From 401a7e8f68f3a3b2381f751ef7a98dc52784df67 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 30 Apr 2025 22:35:01 +0900 Subject: [PATCH 1/4] theory of essential supremum Co-authored-by: Reynald Affeldt Co-authored-by: Cyril Cohen Co-authored-by: Pierre Roux Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 23 +++ _CoqProject | 1 + theories/ess_sup_inf.v | 343 ++++++++++++++++++++++++++++++++++++++++ theories/hoelder.v | 6 +- theories/measure.v | 18 --- 5 files changed, 370 insertions(+), 21 deletions(-) create mode 100644 theories/ess_sup_inf.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c9debd831..697e29672 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -17,6 +17,25 @@ + lemma `ae_foralln` + lemma `ae_eqe_mul2l` +- new file `ess_sup_inf.v`: + + lemma `measure0_ae` + + definition `ess_esup` + + lemmas `ess_supEae`, `ae_le_measureP`, `ess_supEmu0`, `ess_sup_ge`, + `ess_supP`, `le_ess_sup`, `eq_ess_sup`, `ess_sup_cst`, `ess_sup_ae_cst`, + `ess_sup_gee`, `abs_sup_eq0_ae_eq`, `abs_ess_sup_eq0`, `ess_sup_pZl`, + `ess_supZl`, `ess_sup_eqNyP`, `ess_supD`, `ess_sup_absD` + + notation `ess_supr` + + lemmas `ess_supr_bounded`, `ess_sup_eqr0_ae_eq`, `ess_suprZl`, + `ess_sup_ger`, `ess_sup_ler`, `ess_sup_cstr`, `ess_suprD`, `ess_sup_normD` + + definition `ess_inf` + + lemmas `ess_infEae`, `ess_infEN`, `ess_supEN`, `ess_infN`, `ess_supN`, + `ess_infP`, `ess_inf_le`, `le_ess_inf`, `eq_ess_inf`, `ess_inf_cst`, + `ess_inf_ae_cst`, `ess_inf_gee`, `ess_inf_pZl`, `ess_infZl`, `ess_inf_eqyP`, + `ess_infD` + + notation `ess_infr` + + lemmas `ess_infr_bounded`, `ess_infrZl`, `ess_inf_ger`, `ess_inf_ler`, + `ess_inf_cstr` + ### Changed - in `measure.v`: @@ -26,6 +45,9 @@ ### Renamed +- in `measure.v` + + definition `ess_sup` moved to `ess_sup_inf.v` + ### Generalized ### Deprecated @@ -34,6 +56,7 @@ - in `measure.v`: + definition `almost_everywhere_notation` + + lemma `ess_sup_ge0` ### Infrastructure diff --git a/_CoqProject b/_CoqProject index 29135cf9d..4bd2a3f29 100644 --- a/_CoqProject +++ b/_CoqProject @@ -69,6 +69,7 @@ theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v theories/homotopy_theory/continuous_path.v +theories/ess_sup_inf.v theories/function_spaces.v theories/ereal.v theories/cantor.v diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v new file mode 100644 index 000000000..2312636ef --- /dev/null +++ b/theories/ess_sup_inf.v @@ -0,0 +1,343 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. +From mathcomp Require Import topology normedtype sequences esum numfun. +From mathcomp Require Import measure lebesgue_measure. + +(**md**************************************************************************) +(* ``` *) +(* ess_sup f == essential supremum of the function f : T -> R where T is a *) +(* semiRingOfSetsType and R is a realType *) +(* ess_inf f == essential infimum *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Section essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types (f g : T -> \bar R) (h k : T -> R). + +(* TODO: move *) +Lemma measure0_ae (P : set T) : mu [set: T] = 0 -> \forall x \ae mu, P x. +Proof. by move=> x; exists setT; split. Qed. + +Definition ess_sup f := ereal_inf [set y | \forall x \ae mu, f x <= y]. + +Lemma ess_supEae (f : T -> \bar R) : + ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y]. +Proof. by []. Qed. + +Lemma ae_le_measureP f y : measurable_fun setT f -> + (\forall x \ae mu, f x <= y) <-> (mu (f @^-1` `]y, +oo[) = 0). +Proof. +move=> f_meas; have fVroo_meas : d.-measurable (f @^-1` `]y, +oo[). + by rewrite -[_ @^-1` _]setTI; apply/f_meas=> //; exact/emeasurable_itv. +have setCfVroo : (f @^-1` `]y, +oo[) = ~` [set x | f x <= y]. + by apply: setC_inj; rewrite preimage_setC setCitv/= set_itvxx setU0 setCK. +split. + move=> [N [dN muN0 inN]]; rewrite (subset_measure0 _ dN)// => x. + by rewrite setCfVroo; apply: inN. +set N := (X in mu X) => muN0; exists N; rewrite -setCfVroo. +by split => //; exact: fVroo_meas. +Qed. + +Lemma ess_supEmu0 (f : T -> \bar R) : measurable_fun setT f -> + ess_sup f = ereal_inf [set y | mu (f @^-1` `]y, +oo[) = 0]. +Proof. +by move=> ?; congr (ereal_inf _); apply/predeqP => r; exact: ae_le_measureP. +Qed. + +Lemma ess_sup_ge f : \forall x \ae mu, f x <= ess_sup f. +Proof. +rewrite ess_supEae//; set I := (X in ereal_inf X). +have [->|IN0] := eqVneq I set0. + by rewrite ereal_inf0; apply: nearW => ?; rewrite leey. +have [u uI uinf] := ereal_inf_seq IN0. +rewrite -(cvg_lim _ uinf)//; near=> x. +rewrite lime_ge//; first by apply/cvgP: uinf. +by apply: nearW; near: x; apply/ae_foralln => n; apply: uI. +Unshelve. all: by end_near. Qed. + +Lemma ess_supP f a : reflect (\forall x \ae mu, f x <= a) (ess_sup f <= a). +Proof. +apply: (iffP (ereal_inf_leP _)) => /=; last 2 first. +- by move=> [y fy ya]; near do apply: le_trans ya. +- by move=> fa; exists a. +by rewrite -ess_supEae//; exact: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma le_ess_sup f g : (\forall x \ae mu, f x <= g x) -> ess_sup f <= ess_sup g. +Proof. +move=> fg; apply/ess_supP => //. +near do rewrite (le_trans (near fg _ _))//=. +exact: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma eq_ess_sup f g : (\forall x \ae mu, f x = g x) -> ess_sup f = ess_sup g. +Proof. +move=> fg; apply/eqP; rewrite eq_le !le_ess_sup//=; + by apply: filterS fg => x ->. +Qed. + +Lemma ess_sup_cst r : 0 < mu [set: T] -> ess_sup (cst r) = r. +Proof. +move=> muT_gt0; apply/eqP; rewrite eq_le; apply/andP; split. + by apply/ess_supP => //; apply: nearW. +have ae_proper := ae_properfilter_algebraOfSetsType muT_gt0. +by near (almost_everywhere mu) => x; near: x; apply: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_ae_cst f r : 0 < mu [set: T] -> + (\forall x \ae mu, f x = r) -> ess_sup f = r. +Proof. by move=> muT_gt0 /= /eq_ess_sup->; rewrite ess_sup_cst. Qed. + +Lemma ess_sup_gee f y : 0 < mu [set: T] -> + (\forall x \ae mu, y <= f x)%E -> y <= ess_sup f. +Proof. by move=> *; rewrite -(ess_sup_cst y)//; apply: le_ess_sup. Qed. + +Lemma abs_sup_eq0_ae_eq f : ess_sup (abse \o f) = 0 -> f = \0 %[ae mu]. +Proof. +move=> ess_sup_f_eq0; near=> x => _ /=; apply/eqP. +rewrite -abse_eq0 eq_le abse_ge0 andbT; near: x. +by apply/ess_supP; rewrite ess_sup_f_eq0. +Unshelve. all: by end_near. Qed. + +Lemma abs_ess_sup_eq0 f : mu [set: T] > 0 -> + f = \0 %[ae mu] -> ess_sup (abse \o f) = 0. +Proof. +move=> muT_gt0 f0; apply/eqP; rewrite eq_le; apply/andP; split. + by apply/ess_supP => /=; near do rewrite (near f0 _ _)//= normr0//. +by rewrite -[0]ess_sup_cst// le_ess_sup//=; near=> x; rewrite abse_ge0. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_pZl f (a : R) : (0 < a)%R -> + ess_sup (cst a%:E \* f) = a%:E * ess_sup f. +Proof. +move=> /[dup] /ltW a_ge0 a_gt0. +gen have esc_le : a f a_ge0 a_gt0 / + (ess_sup (cst a%:E \* f) <= a%:E * ess_sup f)%E. + by apply/ess_supP; near do rewrite /cst/= lee_pmul2l//; apply/ess_supP. +apply/eqP; rewrite eq_le esc_le// -lee_pdivlMl//=. +apply: le_trans (esc_le _ _ _ _); rewrite ?invr_gt0 ?invr_ge0//. +by under eq_fun do rewrite muleA -EFinM mulVf ?mul1e ?gt_eqF//. +Unshelve. all: by end_near. Qed. + +Lemma ess_supZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> + ess_sup (cst a%:E \* f) = a%:E * ess_sup f. +Proof. +move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_sup_pZl. +by under eq_fun do rewrite mul0e; rewrite mul0e ess_sup_cst. +Qed. + +Lemma ess_sup_eqNyP f : ess_sup f = -oo <-> \forall x \ae mu, f x = -oo. +Proof. +rewrite (rwP eqP) -leeNy_eq (eq_near (fun=> rwP eqP)). +by under eq_near do rewrite -leeNy_eq; apply/(rwP2 idP (ess_supP _ _)). +Qed. + +Lemma ess_supD f g : ess_sup (f \+ g) <= ess_sup f + ess_sup g. +Proof. +by apply/ess_supP; near do rewrite lee_add//; apply/ess_supP. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_absD f g : + ess_sup (abse \o (f \+ g)) <= ess_sup (abse \o f) + ess_sup (abse \o g). +Proof. +rewrite (le_trans _ (ess_supD _ _))// le_ess_sup//. +by apply/nearW => x; apply/lee_abs_add. +Qed. + +End essential_supremum. +Arguments ess_sup_ae_cst {d T R mu f}. +Arguments ess_supP {d T R mu f a}. + +Section real_essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Notation ess_supr f := (ess_sup mu (EFin \o f)). + +Lemma ess_supr_bounded f : ess_supr f < +oo -> + exists M, \forall x \ae mu, (f x <= M)%R. +Proof. +set g := EFin \o f => ltfy; have [|supfNy] := eqVneq (ess_sup mu g) -oo. + by move=> /ess_sup_eqNyP fNy; exists 0%:R; apply: filterS fNy. +have supf_fin : ess_supr f \is a fin_num by case: ess_sup ltfy supfNy. +by exists (fine (ess_supr f)); near do rewrite -lee_fin fineK//; apply/ess_supP. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_eqr0_ae_eq f : ess_supr (normr \o f) = 0 -> f = 0%R %[ae mu]. +Proof. +under [X in ess_sup _ X]eq_fun do rewrite /= -abse_EFin. +move=> /abs_sup_eq0_ae_eq; apply: filterS => x /= /(_ _)/eqP. +by rewrite eqe => /(_ _)/eqP. +Qed. + +Lemma ess_suprZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> + ess_supr (cst y \* f)%R = y%:E * ess_supr f. +Proof. by move=> muT_gt0 r_ge0; rewrite -ess_supZl. Qed. + +Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> + x <= ess_supr f. +Proof. by move=> muT f0; apply/ess_sup_gee => //=; apply: nearW. Qed. + +Lemma ess_sup_ler f y : (forall t, (f t)%:E <= y) -> ess_supr f <= y. +Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed. + +Lemma ess_sup_cstr y : (0 < mu setT)%E -> (ess_supr (cst y) = y%:E)%E. +Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed. + +Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g. +Proof. by rewrite (le_trans _ (ess_supD _ _ _)). Qed. + +Lemma ess_sup_normD f g : + ess_supr (normr \o (f \+ g)) <= ess_supr (normr \o f) + ess_supr (normr \o g). +Proof. +rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//. +by apply/nearW => x; apply/ler_normD. +Qed. + +End real_essential_supremum. +Notation ess_supr mu f := (ess_sup mu (EFin \o f)). + +Section essential_infimum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> \bar R. + +Definition ess_inf f := ereal_sup [set y | \forall x \ae mu, y <= f x]. +Notation ess_sup := (ess_sup mu). + +Lemma ess_infEae (f : T -> \bar R) : + ess_inf f = ereal_sup [set y | \forall x \ae mu, y <= f x]. +Proof. by []. Qed. + +Lemma ess_infEN (f : T -> \bar R) : ess_inf f = - ess_sup (\- f). +Proof. +rewrite ess_supEae ess_infEae ereal_infEN oppeK; congr (ereal_sup _). +apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]]. + by exists (- y); rewrite ?oppeK//=; apply: filterS y_le => x; rewrite leeN2. +by apply: filterS y_ge => x; rewrite leeNl. +Qed. + +Lemma ess_supEN (f : T -> \bar R) : ess_sup f = - ess_inf (\- f). +Proof. +by rewrite ess_infEN oppeK; apply/eq_ess_sup/nearW => ?; rewrite oppeK. +Qed. + +Lemma ess_infN (f : T -> \bar R) : ess_inf (\- f) = - ess_sup f. +Proof. by rewrite ess_supEN oppeK. Qed. + +Lemma ess_supN (f : T -> \bar R) : ess_sup (\- f) = - ess_inf f. +Proof. by rewrite ess_infEN oppeK. Qed. + +Lemma ess_infP f a : reflect (\forall x \ae mu, a <= f x) (a <= ess_inf f). +Proof. +by rewrite ess_infEN leeNr; apply: (iffP ess_supP); + apply: filterS => x; rewrite leeN2. +Qed. + +Lemma ess_inf_le f : \forall x \ae mu, ess_inf f <= f x. +Proof. exact/ess_infP. Qed. + +Lemma le_ess_inf f g : (\forall x \ae mu, f x <= g x) -> ess_inf f <= ess_inf g. +Proof. +move=> fg; apply/ess_infP => //. +near do rewrite (le_trans _ (near fg _ _))//=. +exact: ess_inf_le. +Unshelve. all: by end_near. Qed. + +Lemma eq_ess_inf f g : (\forall x \ae mu, f x = g x) -> ess_inf f = ess_inf g. +Proof. +move=> fg; apply/eqP; rewrite eq_le !le_ess_inf//=; + by apply: filterS fg => x ->. +Qed. + +Lemma ess_inf_cst r : 0 < mu [set: T] -> ess_inf (cst r) = r. +Proof. +by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- r)) ?oppeK//=; apply: nearW. +Qed. + +Lemma ess_inf_ae_cst f r : 0 < mu [set: T] -> + (\forall x \ae mu, f x = r) -> ess_inf f = r. +Proof. by move=> muT_gt0 /= /eq_ess_inf->; rewrite ess_inf_cst. Qed. + +Lemma ess_inf_gee f y : 0 < mu [set: T] -> + (\forall x \ae mu, y <= f x)%E -> y <= ess_inf f. +Proof. by move=> *; rewrite -(ess_inf_cst y)//; apply: le_ess_inf. Qed. + +Lemma ess_inf_pZl f (a : R) : (0 < a)%R -> + (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Proof. +move=> a_gt0; rewrite !ess_infEN muleN; congr (- _)%E. +by under eq_fun do rewrite -muleN; rewrite ess_sup_pZl. +Qed. + +Lemma ess_infZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> + (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Proof. +move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_inf_pZl. +by under eq_fun do rewrite mul0e; rewrite mul0e ess_inf_cst. +Qed. + +Lemma ess_inf_eqyP f : ess_inf f = +oo <-> \forall x \ae mu, f x = +oo. +Proof. +rewrite (rwP eqP) -leye_eq (eq_near (fun=> rwP eqP)). +by under eq_near do rewrite -leye_eq; apply/(rwP2 idP (ess_infP _ _)). +Qed. + +Lemma ess_infD f g : ess_inf (f \+ g) >= ess_inf f + ess_inf g. +Proof. +by apply/ess_infP; near do rewrite lee_add//; apply/ess_infP. +Unshelve. all: by end_near. Qed. + +End essential_infimum. +Arguments ess_inf_ae_cst {d T R mu f}. +Arguments ess_infP {d T R mu f a}. + +Section real_essential_infimum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Notation ess_infr f := (ess_inf mu (EFin \o f)). + +Lemma ess_infr_bounded f : ess_infr f > -oo -> + exists M, \forall x \ae mu, (f x >= M)%R. +Proof. +set g := EFin \o f => ltfy; have [|inffNy] := eqVneq (ess_inf mu g) +oo. + by move=> /ess_inf_eqyP fNy; exists 0%:R; apply: filterS fNy. +have inff_fin : ess_infr f \is a fin_num by case: ess_inf ltfy inffNy. +by exists (fine (ess_infr f)); near do rewrite -lee_fin fineK//; apply/ess_infP. +Unshelve. all: by end_near. Qed. + +Lemma ess_infrZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> + ess_infr (cst y \* f)%R = y%:E * ess_infr f. +Proof. by move=> muT_gt0 r_ge0; rewrite -ess_infZl. Qed. + +Lemma ess_inf_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> + x <= ess_infr f. +Proof. by move=> muT f0; apply/ess_inf_gee => //=; apply: nearW. Qed. + +Lemma ess_inf_ler f y : (forall t, y <= (f t)%:E) -> y <= ess_infr f. +Proof. by move=> ?; apply/ess_infP; apply: nearW. Qed. + +Lemma ess_inf_cstr y : (0 < mu setT)%E -> (ess_infr (cst y) = y%:E)%E. +Proof. by move=> muN0; rewrite (ess_inf_ae_cst y%:E)//=; apply: nearW. Qed. + +End real_essential_infimum. +Notation ess_infr mu f := (ess_inf mu (EFin \o f)). diff --git a/theories/hoelder.v b/theories/hoelder.v index 06385c4ac..d5dca2a07 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop reals ereal. From mathcomp Require Import topology normedtype sequences real_interval. From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral. -From mathcomp Require Import numfun exp convex interval_inference. +From mathcomp Require Import numfun exp convex interval_inference ess_sup_inf. (**md**************************************************************************) (* # Hoelder's Inequality *) @@ -43,7 +43,7 @@ HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType} mu (f @^-1` (setT `\ 0%R)) else (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E - | +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E + | +oo%E => (if mu [set: T] > 0 then ess_supr mu (normr \o f) else 0)%E | -oo%E => 0%E end. Canonical locked_Lnorm := Unlockable Lnorm.unlock. @@ -68,7 +68,7 @@ Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. rewrite unlock; move: p => [r/=|/=|//]. by case: ifPn => // r0; exact: poweR_ge0. -by case: ifPn => // /ess_sup_ge0; apply => t/=. +by case: ifPn => // /ess_sup_ger; apply => t/=. Qed. Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g]. diff --git a/theories/measure.v b/theories/measure.v index 836009a40..7830028b4 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5421,21 +5421,3 @@ Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E -> Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed. End absolute_continuity_lemmas. - -Section essential_supremum. -Context d {T : semiRingOfSetsType d} {R : realType}. -Variable mu : {measure set T -> \bar R}. -Implicit Types f : T -> R. - -Definition ess_sup f := - ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). - -Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> - 0 <= ess_sup f. -Proof. -move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP rf <-]; rewrite leNgt. -apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//. -by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)). -Qed. - -End essential_supremum. From 8a4c5702e8083e0727acf8254ec7a204f5665e7a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 12 May 2025 19:02:36 +0900 Subject: [PATCH 2/4] nitpicking --- theories/ess_sup_inf.v | 135 ++++++++++++++++++++++++----------------- theories/measure.v | 15 +++-- 2 files changed, 90 insertions(+), 60 deletions(-) diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v index 2312636ef..26ade094a 100644 --- a/theories/ess_sup_inf.v +++ b/theories/ess_sup_inf.v @@ -6,6 +6,8 @@ From mathcomp Require Import topology normedtype sequences esum numfun. From mathcomp Require Import measure lebesgue_measure. (**md**************************************************************************) +(* # Essential infimum and essential supremum *) +(* *) (* ``` *) (* ess_sup f == essential supremum of the function f : T -> R where T is a *) (* semiRingOfSetsType and R is a realType *) @@ -26,26 +28,29 @@ Local Open Scope ring_scope. Local Open Scope ereal_scope. Section essential_supremum. -Context d {T : measurableType d} {R : realType}. +Context d {T : semiRingOfSetsType d} {R : realType}. Variable mu : {measure set T -> \bar R}. Implicit Types (f g : T -> \bar R) (h k : T -> R). -(* TODO: move *) -Lemma measure0_ae (P : set T) : mu [set: T] = 0 -> \forall x \ae mu, P x. -Proof. by move=> x; exists setT; split. Qed. - Definition ess_sup f := ereal_inf [set y | \forall x \ae mu, f x <= y]. Lemma ess_supEae (f : T -> \bar R) : ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y]. Proof. by []. Qed. -Lemma ae_le_measureP f y : measurable_fun setT f -> - (\forall x \ae mu, f x <= y) <-> (mu (f @^-1` `]y, +oo[) = 0). +End essential_supremum. + +Section essential_supremum_lemmas. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types (f g : T -> \bar R) (h k : T -> R) (x y : \bar R) (r : R). + +Lemma ae_le_measureP f y : measurable_fun [set: T] f -> + (\forall x \ae mu, f x <= y) <-> mu (f @^-1` `]y, +oo[) = 0. Proof. move=> f_meas; have fVroo_meas : d.-measurable (f @^-1` `]y, +oo[). by rewrite -[_ @^-1` _]setTI; apply/f_meas=> //; exact/emeasurable_itv. -have setCfVroo : (f @^-1` `]y, +oo[) = ~` [set x | f x <= y]. +have setCfVroo : f @^-1` `]y, +oo[ = ~` [set x | f x <= y]. by apply: setC_inj; rewrite preimage_setC setCitv/= set_itvxx setU0 setCK. split. move=> [N [dN muN0 inN]]; rewrite (subset_measure0 _ dN)// => x. @@ -54,7 +59,9 @@ set N := (X in mu X) => muN0; exists N; rewrite -setCfVroo. by split => //; exact: fVroo_meas. Qed. -Lemma ess_supEmu0 (f : T -> \bar R) : measurable_fun setT f -> +Local Notation ess_sup := (ess_sup mu). + +Lemma ess_supEmu0 f : measurable_fun [set: T] f -> ess_sup f = ereal_inf [set y | mu (f @^-1` `]y, +oo[) = 0]. Proof. by move=> ?; congr (ereal_inf _); apply/predeqP => r; exact: ae_le_measureP. @@ -92,21 +99,21 @@ move=> fg; apply/eqP; rewrite eq_le !le_ess_sup//=; by apply: filterS fg => x ->. Qed. -Lemma ess_sup_cst r : 0 < mu [set: T] -> ess_sup (cst r) = r. +Lemma ess_sup_cst x : 0 < mu [set: T] -> ess_sup (cst x) = x. Proof. move=> muT_gt0; apply/eqP; rewrite eq_le; apply/andP; split. by apply/ess_supP => //; apply: nearW. have ae_proper := ae_properfilter_algebraOfSetsType muT_gt0. -by near (almost_everywhere mu) => x; near: x; apply: ess_sup_ge. +by near (almost_everywhere mu) => y; near: y; apply: ess_sup_ge. Unshelve. all: by end_near. Qed. -Lemma ess_sup_ae_cst f r : 0 < mu [set: T] -> - (\forall x \ae mu, f x = r) -> ess_sup f = r. +Lemma ess_sup_ae_cst f y : 0 < mu [set: T] -> + (\forall x \ae mu, f x = y) -> ess_sup f = y. Proof. by move=> muT_gt0 /= /eq_ess_sup->; rewrite ess_sup_cst. Qed. -Lemma ess_sup_gee f y : 0 < mu [set: T] -> - (\forall x \ae mu, y <= f x)%E -> y <= ess_sup f. -Proof. by move=> *; rewrite -(ess_sup_cst y)//; apply: le_ess_sup. Qed. +Lemma ess_sup_gee f a : 0 < mu [set: T] -> + (\forall x \ae mu, a <= f x) -> a <= ess_sup f. +Proof. by move=> *; rewrite -(ess_sup_cst a)//; apply: le_ess_sup. Qed. Lemma abs_sup_eq0_ae_eq f : ess_sup (abse \o f) = 0 -> f = \0 %[ae mu]. Proof. @@ -123,22 +130,22 @@ move=> muT_gt0 f0; apply/eqP; rewrite eq_le; apply/andP; split. by rewrite -[0]ess_sup_cst// le_ess_sup//=; near=> x; rewrite abse_ge0. Unshelve. all: by end_near. Qed. -Lemma ess_sup_pZl f (a : R) : (0 < a)%R -> - ess_sup (cst a%:E \* f) = a%:E * ess_sup f. +Lemma ess_sup_pZl f r : (0 < r)%R -> + ess_sup (cst r%:E \* f) = r%:E * ess_sup f. Proof. -move=> /[dup] /ltW a_ge0 a_gt0. -gen have esc_le : a f a_ge0 a_gt0 / - (ess_sup (cst a%:E \* f) <= a%:E * ess_sup f)%E. +move=> /[dup] /ltW r_ge0 r_gt0. +gen have esc_le : r f r_ge0 r_gt0 / + ess_sup (cst r%:E \* f) <= r%:E * ess_sup f. by apply/ess_supP; near do rewrite /cst/= lee_pmul2l//; apply/ess_supP. apply/eqP; rewrite eq_le esc_le// -lee_pdivlMl//=. apply: le_trans (esc_le _ _ _ _); rewrite ?invr_gt0 ?invr_ge0//. by under eq_fun do rewrite muleA -EFinM mulVf ?mul1e ?gt_eqF//. Unshelve. all: by end_near. Qed. -Lemma ess_supZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> - ess_sup (cst a%:E \* f) = a%:E * ess_sup f. +Lemma ess_supZl f r : mu [set: T] > 0 -> (0 <= r)%R -> + ess_sup (cst r%:E \* f) = r%:E * ess_sup f. Proof. -move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_sup_pZl. +move=> muTN0; case: ltgtP => // [r_gt0|<-] _; first exact: ess_sup_pZl. by under eq_fun do rewrite mul0e; rewrite mul0e ess_sup_cst. Qed. @@ -150,7 +157,7 @@ Qed. Lemma ess_supD f g : ess_sup (f \+ g) <= ess_sup f + ess_sup g. Proof. -by apply/ess_supP; near do rewrite lee_add//; apply/ess_supP. +by apply/ess_supP; near do rewrite leeD//; apply/ess_supP. Unshelve. all: by end_near. Qed. Lemma ess_sup_absD f g : @@ -160,11 +167,20 @@ rewrite (le_trans _ (ess_supD _ _))// le_ess_sup//. by apply/nearW => x; apply/lee_abs_add. Qed. -End essential_supremum. +End essential_supremum_lemmas. Arguments ess_sup_ae_cst {d T R mu f}. Arguments ess_supP {d T R mu f a}. Section real_essential_supremum. +Context d {T : semiRingOfSetsType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Notation ess_supr f := (ess_sup mu (EFin \o f)). + +End real_essential_supremum. + +Section real_essential_supremum_lemmas. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. Implicit Types f : T -> R. @@ -198,7 +214,7 @@ Proof. by move=> muT f0; apply/ess_sup_gee => //=; apply: nearW. Qed. Lemma ess_sup_ler f y : (forall t, (f t)%:E <= y) -> ess_supr f <= y. Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed. -Lemma ess_sup_cstr y : (0 < mu setT)%E -> (ess_supr (cst y) = y%:E)%E. +Lemma ess_sup_cstr y : 0 < mu [set: T] -> ess_supr (cst y) = y%:E. Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed. Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g. @@ -211,22 +227,30 @@ rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//. by apply/nearW => x; apply/ler_normD. Qed. -End real_essential_supremum. +End real_essential_supremum_lemmas. Notation ess_supr mu f := (ess_sup mu (EFin \o f)). Section essential_infimum. -Context d {T : measurableType d} {R : realType}. +Context d {T : semiRingOfSetsType d} {R : realType}. Variable mu : {measure set T -> \bar R}. Implicit Types f : T -> \bar R. Definition ess_inf f := ereal_sup [set y | \forall x \ae mu, y <= f x]. -Notation ess_sup := (ess_sup mu). -Lemma ess_infEae (f : T -> \bar R) : - ess_inf f = ereal_sup [set y | \forall x \ae mu, y <= f x]. +Lemma ess_infEae f : ess_inf f = ereal_sup [set y | \forall x \ae mu, y <= f x]. Proof. by []. Qed. -Lemma ess_infEN (f : T -> \bar R) : ess_inf f = - ess_sup (\- f). +End essential_infimum. + +Section essential_infimum_lemmas. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types (f : T -> \bar R) (x y : \bar R) (r : R). + +Local Notation ess_inf := (ess_inf mu). +Local Notation ess_sup := (ess_sup mu). + +Lemma ess_infEN f : ess_inf f = - ess_sup (\- f). Proof. rewrite ess_supEae ess_infEae ereal_infEN oppeK; congr (ereal_sup _). apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]]. @@ -234,18 +258,18 @@ apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]]. by apply: filterS y_ge => x; rewrite leeNl. Qed. -Lemma ess_supEN (f : T -> \bar R) : ess_sup f = - ess_inf (\- f). +Lemma ess_supEN f : ess_sup f = - ess_inf (\- f). Proof. by rewrite ess_infEN oppeK; apply/eq_ess_sup/nearW => ?; rewrite oppeK. Qed. -Lemma ess_infN (f : T -> \bar R) : ess_inf (\- f) = - ess_sup f. +Lemma ess_infN f : ess_inf (\- f) = - ess_sup f. Proof. by rewrite ess_supEN oppeK. Qed. -Lemma ess_supN (f : T -> \bar R) : ess_sup (\- f) = - ess_inf f. +Lemma ess_supN f : ess_sup (\- f) = - ess_inf f. Proof. by rewrite ess_infEN oppeK. Qed. -Lemma ess_infP f a : reflect (\forall x \ae mu, a <= f x) (a <= ess_inf f). +Lemma ess_infP f y : reflect (\forall x \ae mu, y <= f x) (y <= ess_inf f). Proof. by rewrite ess_infEN leeNr; apply: (iffP ess_supP); apply: filterS => x; rewrite leeN2. @@ -267,28 +291,27 @@ move=> fg; apply/eqP; rewrite eq_le !le_ess_inf//=; by apply: filterS fg => x ->. Qed. -Lemma ess_inf_cst r : 0 < mu [set: T] -> ess_inf (cst r) = r. +Lemma ess_inf_cst x : 0 < mu [set: T] -> ess_inf (cst x) = x. Proof. -by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- r)) ?oppeK//=; apply: nearW. +by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- x)) ?oppeK//=; apply: nearW. Qed. -Lemma ess_inf_ae_cst f r : 0 < mu [set: T] -> - (\forall x \ae mu, f x = r) -> ess_inf f = r. +Lemma ess_inf_ae_cst f y : 0 < mu [set: T] -> + (\forall x \ae mu, f x = y) -> ess_inf f = y. Proof. by move=> muT_gt0 /= /eq_ess_inf->; rewrite ess_inf_cst. Qed. Lemma ess_inf_gee f y : 0 < mu [set: T] -> - (\forall x \ae mu, y <= f x)%E -> y <= ess_inf f. + (\forall x \ae mu, y <= f x) -> y <= ess_inf f. Proof. by move=> *; rewrite -(ess_inf_cst y)//; apply: le_ess_inf. Qed. -Lemma ess_inf_pZl f (a : R) : (0 < a)%R -> - (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Lemma ess_inf_pZl f r : (0 < r)%R -> ess_inf (cst r%:E \* f) = r%:E * ess_inf f. Proof. -move=> a_gt0; rewrite !ess_infEN muleN; congr (- _)%E. +move=> r_gt0; rewrite !ess_infEN muleN; congr (- _). by under eq_fun do rewrite -muleN; rewrite ess_sup_pZl. Qed. -Lemma ess_infZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> - (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Lemma ess_infZl f r : mu [set: T] > 0 -> (0 <= r)%R -> + ess_inf (cst r%:E \* f) = r%:E * ess_inf f. Proof. move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_inf_pZl. by under eq_fun do rewrite mul0e; rewrite mul0e ess_inf_cst. @@ -302,17 +325,17 @@ Qed. Lemma ess_infD f g : ess_inf (f \+ g) >= ess_inf f + ess_inf g. Proof. -by apply/ess_infP; near do rewrite lee_add//; apply/ess_infP. +by apply/ess_infP; near do rewrite leeD//; apply/ess_infP. Unshelve. all: by end_near. Qed. -End essential_infimum. +End essential_infimum_lemmas. Arguments ess_inf_ae_cst {d T R mu f}. -Arguments ess_infP {d T R mu f a}. +Arguments ess_infP {d T R mu f y}. Section real_essential_infimum. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. -Implicit Types f : T -> R. +Implicit Types (f : T -> R) (x : \bar R) (r : R). Notation ess_infr f := (ess_inf mu (EFin \o f)). @@ -325,19 +348,19 @@ have inff_fin : ess_infr f \is a fin_num by case: ess_inf ltfy inffNy. by exists (fine (ess_infr f)); near do rewrite -lee_fin fineK//; apply/ess_infP. Unshelve. all: by end_near. Qed. -Lemma ess_infrZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> - ess_infr (cst y \* f)%R = y%:E * ess_infr f. +Lemma ess_infrZl f r : mu [set: T] > 0 -> (0 <= r)%R -> + ess_infr (cst r \* f)%R = r%:E * ess_infr f. Proof. by move=> muT_gt0 r_ge0; rewrite -ess_infZl. Qed. Lemma ess_inf_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> x <= ess_infr f. Proof. by move=> muT f0; apply/ess_inf_gee => //=; apply: nearW. Qed. -Lemma ess_inf_ler f y : (forall t, y <= (f t)%:E) -> y <= ess_infr f. +Lemma ess_inf_ler f x : (forall t, x <= (f t)%:E) -> x <= ess_infr f. Proof. by move=> ?; apply/ess_infP; apply: nearW. Qed. -Lemma ess_inf_cstr y : (0 < mu setT)%E -> (ess_infr (cst y) = y%:E)%E. -Proof. by move=> muN0; rewrite (ess_inf_ae_cst y%:E)//=; apply: nearW. Qed. +Lemma ess_inf_cstr r : 0 < mu [set: T] -> ess_infr (cst r) = r%:E. +Proof. by move=> muN0; rewrite (ess_inf_ae_cst r%:E)//=; apply: nearW. Qed. End real_essential_infimum. Notation ess_infr mu f := (ess_inf mu (EFin \o f)). diff --git a/theories/measure.v b/theories/measure.v index 7830028b4..f1aaa5ccf 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4160,14 +4160,21 @@ Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope. Notation "\forall x \ae mu , P" := (\forall x \near almost_everywhere mu, P) (format "\forall x \ae mu , P", x name, P at level 200, at level 200): type_scope. -Definition ae_eq d (T : semiRingOfSetsType d) (R : realType) (mu : {measure set T -> \bar R}) - (V : T -> Type) D (f g : forall x, V x) := (\forall x \ae mu, D x -> f x = g x). +Definition ae_eq d (T : semiRingOfSetsType d) (R : realType) + (mu : {measure set T -> \bar R}) (V : T -> Type) D (f g : forall x, V x) := + \forall x \ae mu, D x -> f x = g x. Notation "f = g %[ae mu 'in' D ]" := (\forall x \ae mu, D x -> f x = g x) - (format "f = g '%[ae' mu 'in' D ]", g at next level, D at level 200, at level 70). + (format "f = g '%[ae' mu 'in' D ]", + g at next level, D at level 200, at level 70). Notation "f = g %[ae mu ]" := (f = g %[ae mu in setT ]) (format "f = g '%[ae' mu ]", g at next level, at level 70). -Lemma aeW {d} {T : ringOfSetsType d} {R : realFieldType} +Lemma measure0_ae d {T : algebraOfSetsType d} {R : realType} + (mu : {measure set T -> \bar R}) (P : set T) : + mu [set: T] = 0 -> \forall x \ae mu, P x. +Proof. by move=> x; exists setT. Qed. + +Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType} (mu : {measure set _ -> \bar R}) (P : T -> Prop) : (forall x, P x) -> \forall x \ae mu, P x. Proof. From 9587c95672d0e8f6cb8ba5c6eb32fb49eea6cd8f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 13 May 2025 15:01:45 +0900 Subject: [PATCH 3/4] memo --- theories/ess_sup_inf.v | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v index 26ade094a..b477a35ae 100644 --- a/theories/ess_sup_inf.v +++ b/theories/ess_sup_inf.v @@ -30,12 +30,11 @@ Local Open Scope ereal_scope. Section essential_supremum. Context d {T : semiRingOfSetsType d} {R : realType}. Variable mu : {measure set T -> \bar R}. -Implicit Types (f g : T -> \bar R) (h k : T -> R). +Implicit Type f : T -> \bar R. Definition ess_sup f := ereal_inf [set y | \forall x \ae mu, f x <= y]. -Lemma ess_supEae (f : T -> \bar R) : - ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y]. +Lemma ess_supEae f : ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y]. Proof. by []. Qed. End essential_supremum. @@ -45,6 +44,8 @@ Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. Implicit Types (f g : T -> \bar R) (h k : T -> R) (x y : \bar R) (r : R). +(* NB: note that this lemma does not depends on the new definitions introduced + in this file and might be move earlier in the file hierarchy later *) Lemma ae_le_measureP f y : measurable_fun [set: T] f -> (\forall x \ae mu, f x <= y) <-> mu (f @^-1` `]y, +oo[) = 0. Proof. @@ -78,11 +79,11 @@ rewrite lime_ge//; first by apply/cvgP: uinf. by apply: nearW; near: x; apply/ae_foralln => n; apply: uI. Unshelve. all: by end_near. Qed. -Lemma ess_supP f a : reflect (\forall x \ae mu, f x <= a) (ess_sup f <= a). +Lemma ess_supP f y : reflect (\forall x \ae mu, f x <= y) (ess_sup f <= y). Proof. apply: (iffP (ereal_inf_leP _)) => /=; last 2 first. -- by move=> [y fy ya]; near do apply: le_trans ya. -- by move=> fa; exists a. +- by move=> [z fz zy]; near do apply: le_trans zy. +- by move=> fy; exists y. by rewrite -ess_supEae//; exact: ess_sup_ge. Unshelve. all: by end_near. Qed. @@ -169,7 +170,7 @@ Qed. End essential_supremum_lemmas. Arguments ess_sup_ae_cst {d T R mu f}. -Arguments ess_supP {d T R mu f a}. +Arguments ess_supP {d T R mu f y}. Section real_essential_supremum. Context d {T : semiRingOfSetsType d} {R : realType}. @@ -183,7 +184,7 @@ End real_essential_supremum. Section real_essential_supremum_lemmas. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. -Implicit Types f : T -> R. +Implicit Types (f : T -> R) (r : R). Notation ess_supr f := (ess_sup mu (EFin \o f)). @@ -203,8 +204,8 @@ move=> /abs_sup_eq0_ae_eq; apply: filterS => x /= /(_ _)/eqP. by rewrite eqe => /(_ _)/eqP. Qed. -Lemma ess_suprZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> - ess_supr (cst y \* f)%R = y%:E * ess_supr f. +Lemma ess_suprZl f r : mu [set: T] > 0 -> (0 <= r)%R -> + ess_supr (cst r \* f)%R = r%:E * ess_supr f. Proof. by move=> muT_gt0 r_ge0; rewrite -ess_supZl. Qed. Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> From 64a040d9a4e0945a64a0d51be019d42bf0615baf Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 14 May 2025 10:16:39 +0900 Subject: [PATCH 4/4] fix --- theories/Make | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/Make b/theories/Make index 31a7ae13f..c9088359b 100644 --- a/theories/Make +++ b/theories/Make @@ -35,6 +35,7 @@ homotopy_theory/homotopy.v homotopy_theory/wedge_sigT.v homotopy_theory/continuous_path.v +ess_sup_inf.v function_spaces.v cantor.v tvs.v