doc, changelog

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

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.

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.

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.