diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 515f5c8a16..8530c546e0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -51,6 +51,13 @@ + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` + lemma `hoelder` +- in `ereal.v`: + + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`, + `ereal_infT` + +- in `measure.v`: + + definition `ess_sup`, lemma `ess_sup_ge0` + ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized diff --git a/theories/ereal.v b/theories/ereal.v index e6be994cb8..d1d8185f9e 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -127,6 +127,9 @@ Section ERealArithTh_numDomainType. Context {R : numDomainType}. Implicit Types (x y z : \bar R) (r : R). +Lemma range_oppe : range -%E = [set: \bar R]%classic. +Proof. by apply/seteqP; split => [//|x] _; exists (- x); rewrite ?oppeK. Qed. + Lemma oppe_subset (A B : set (\bar R)) : ((A `<=` B) <-> (-%E @` A `<=` -%E @` B))%classic. Proof. @@ -336,11 +339,19 @@ Export ConstructiveDualAddTheory. Export DualAddTheoryNumDomain. End DualAddTheory. +Canonical ereal_pointed (R : numDomainType) := PointedType (extended R) 0%E. + Section ereal_supremum. Variable R : realFieldType. Local Open Scope classical_set_scope. Implicit Types (S : set (\bar R)) (x y : \bar R). +Lemma uboundT : ubound [set: \bar R] = [set +oo]. +Proof. +apply/seteqP; split => /= [x Tx|x -> ?]; last by rewrite leey. +by apply/eqP; rewrite eq_le leey /= Tx. +Qed. + Lemma ereal_ub_pinfty S : ubound S +oo. Proof. by apply/ubP=> x _; rewrite leey. Qed. @@ -352,9 +363,21 @@ right; rewrite predeqE => y; split => [/Snoo|->{y}]. by have := Snoo _ Sx; rewrite leeNy_eq => /eqP <-. Qed. +Lemma supremumsT : supremums [set: \bar R] = [set +oo]. +Proof. +rewrite /supremums uboundT. +by apply/seteqP; split=> [x []//|x -> /=]; split => // y ->. +Qed. + Lemma ereal_supremums_set0_ninfty : supremums (@set0 (\bar R)) -oo. Proof. by split; [exact/ubP | apply/lbP=> y _; rewrite leNye]. Qed. +Lemma supremumT : supremum -oo [set: \bar R] = +oo. +Proof. +rewrite /supremum (negbTE setT0) supremumsT. +by case: xgetP => // /(_ +oo)/= /eqP; rewrite eqxx. +Qed. + Lemma supremum_pinfty S x0 : S +oo -> supremum x0 S = +oo. Proof. move=> Spoo; rewrite /supremum ifF; last by apply/eqP => S0; rewrite S0 in Spoo. @@ -372,11 +395,17 @@ Definition ereal_inf S := - ereal_sup (-%E @` S). Lemma ereal_sup0 : ereal_sup set0 = -oo. Proof. exact: supremum0. Qed. +Lemma ereal_supT : ereal_sup [set: \bar R] = +oo. +Proof. by rewrite /ereal_sup/= supremumT. Qed. + Lemma ereal_sup1 x : ereal_sup [set x] = x. Proof. exact: supremum1. Qed. Lemma ereal_inf0 : ereal_inf set0 = +oo. Proof. by rewrite /ereal_inf image_set0 ereal_sup0. Qed. +Lemma ereal_infT : ereal_inf [set: \bar R] = -oo. +Proof. by rewrite /ereal_inf range_oppe/= ereal_supT. Qed. + Lemma ereal_inf1 x : ereal_inf [set x] = x. Proof. by rewrite /ereal_inf image_set1 ereal_sup1 oppeK. Qed. @@ -533,8 +562,6 @@ Qed. End ereal_supremum_realType. -Canonical ereal_pointed (R : numDomainType) := PointedType (extended R) 0%E. - Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) : (abse \o f) \_ D = abse \o (f \_ D). Proof. diff --git a/theories/hoelder.v b/theories/hoelder.v index 2d4d94f253..8a7d5378cb 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -36,61 +36,11 @@ Declare Scope Lnorm_scope. Local Open Scope ereal_scope. -(* TODO: move this elsewhere *) -Lemma ubound_setT {R : realFieldType} : ubound [set: \bar R] = [set +oo]. -Proof. -apply/seteqP; split => /= [x Tx|x -> ?]; last by rewrite leey. -by apply/eqP; rewrite eq_le leey /= Tx. -Qed. - -Lemma supremums_setT {R : realFieldType} : supremums [set: \bar R] = [set +oo]. -Proof. -rewrite /supremums ubound_setT. -by apply/seteqP; split=> [x []//|x -> /=]; split => // y ->. -Qed. - -Lemma supremum_setT {R : realFieldType} : supremum -oo [set: \bar R] = +oo. -Proof. -rewrite /supremum (negbTE setT0) supremums_setT. -by case: xgetP => // /(_ +oo)/= /eqP; rewrite eqxx. -Qed. - -Lemma ereal_sup_setT {R : realFieldType} : ereal_sup [set: \bar R] = +oo. -Proof. by rewrite /ereal_sup/= supremum_setT. Qed. - -Lemma range_oppe {R : realFieldType} : range -%E = [set: \bar R]. -Proof. -by apply/seteqP; split => [//|x] _; exists (- x) => //; rewrite oppeK. -Qed. - -Lemma ereal_inf_setT {R : realFieldType} : ereal_inf [set: \bar R] = -oo. -Proof. by rewrite /ereal_inf range_oppe/= ereal_sup_setT. Qed. - -Section essential_supremum. -Context d {T : measurableType 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 [set t | f t > r]%R = 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 rf <-]. -rewrite leNgt; apply/negP => r0. -move/eqP: rf; apply/negP; rewrite gt_eqF//. -rewrite [X in mu X](_ : _ = setT) //. -by apply/seteqP; split => // x _ /=; rewrite (lt_le_trans _ (f0 x)). -Qed. - -End essential_supremum. - Section Lnorm. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. Local Open Scope ereal_scope. -Implicit Types (p : \bar R) (f g : T -> R). +Implicit Types (p : \bar R) (f g : T -> R) (r : R). Definition Lnorm p f := match p with @@ -117,13 +67,12 @@ Qed. Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g]. Proof. by move=> fg; congr Lnorm; exact/funext. Qed. -(* TODO: generalize p *) -Lemma Lnorm_eq0_eq0 (p : R) f : measurable_fun setT f -> 'N_p%:E[f] = 0 -> - ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). +Lemma Lnorm_eq0_eq0 r f : measurable_fun setT f -> 'N_r%:E[f] = 0 -> + ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0). Proof. move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. apply: measurableT_comp => //. - apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. exact: measurableT_comp. under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0. diff --git a/theories/measure.v b/theories/measure.v index 4ba0cdb98c..42ce88b82d 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -228,6 +228,8 @@ From HB Require Import structures. (* measurableType's with resp. display d1 and d2 *) (* *) (* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1 *) +(* ess_sup f == essential supremum of the function f : T -> R where T is a *) +(* measurableType and R is a realType *) (* *) (******************************************************************************) @@ -4367,3 +4369,21 @@ Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed. End absolute_continuity. Notation "m1 `<< m2" := (measure_dominates m1 m2). + +Section essential_supremum. +Context d {T : measurableType 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.