Hardy littlewood (#995)

* maximal inequality

CHANGELOG_UNRELEASED.md

@@ -29,8 +29,35 @@
 	`nondecreasing_cvge`, `nondecreasing_is_cvge`,
 	`nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
 	`nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
+- in `ereal.v`:
+  + lemmas `ereal_sup_le`, `ereal_inf_le`
+
+- in `normedtype.v`:
+  + definition `lower_semicontinuous`
+  + lemma `lower_semicontinuousP`
+
+- in `numfun.v`:
+  + lemma `patch_indic`
+
+- in `lebesgue_measure.v`
+  + lemma `lower_semicontinuous_measurable`
+
+- in `lebesgue_integral.v`:
+  + definition `locally_integrable`
+  + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`,
+    `locally_integrableB`
+  + definition `iavg`
+  + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD`
+  + definitions `HL_maximal`
+  + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`,
+    `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`,
+    `maximal_inequality`
 
 ### Changed
+
+- in `normedtype.v`:
+  + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns
+    duplicate-free lists of indices
 
 ### Renamed
 
@@ -39,6 +66,9 @@
 
 ### Generalized
 
+- in `lebesgue_integral.v`
+  + `ge0_integral_bigsetU` generalized from `nat` to `eqType`
+
 ### Deprecated
 
 ### Removed

theories/charge.v

@@ -1136,17 +1136,19 @@ Let E m j := is_max_approxRN mu nu m j.
 
 Let int_F_nu m A (mA : measurable A) : \int[mu]_(x in A) F m x <= nu A.
 Proof.
-rewrite [leLHS](_ : _ = \sum_(j < m.+1) \int[mu]_(x in (A `&` E m j)) F m x);
-    last first.
+rewrite [leLHS](_ : _ =
+    \sum_(j < m.+1) \int[mu]_(x in (A `&` E m j)) F m x); last first.
   rewrite -[in LHS](setIT A) -(bigsetU_is_max_approxRN mu nu m) big_distrr/=.
-  rewrite (@ge0_integral_bigsetU _ _ _ _ (fun n => A `&` E m n))//.
+  rewrite -(@big_mkord _ _ _ m.+1 xpredT (fun i => A `&` is_max_approxRN mu nu m i)).
+  rewrite ge0_integral_bigsetU ?big_mkord//.
   - by move=> n; apply: measurableI => //; exact: measurable_is_max_approxRN.
-  - by apply: measurable_funTS => //; exact: measurable_max_approxRN_seq.
-  - by move=> ? ?; exact: max_approxRN_seq_ge0.
+  - exact: iota_uniq.
   - apply: trivIset_setIl; apply: (@sub_trivIset _ _ _ setT (E m)) => //.
     exact: trivIset_is_max_approxRN.
-rewrite [leLHS](_ : _ = \sum_(j < m.+1) (\int[mu]_(x in (A `&` (E m j))) g j x));
-    last first.
+  - by apply: measurable_funTS => //; exact: measurable_max_approxRN_seq.
+  - by move=> ? ?; exact: max_approxRN_seq_ge0.
+rewrite [leLHS](_ : _ =
+    \sum_(j < m.+1) (\int[mu]_(x in (A `&` (E m j))) g j x)); last first.
   apply: eq_bigr => i _; apply:eq_integral => x; rewrite inE => -[?] [] Fmgi h.
   by apply/eqP; rewrite eq_le; rewrite /F Fmgi lexx.
 rewrite [leRHS](_ : _ = \sum_(j < m.+1) (nu (A `&` E m j))); last first.
@@ -1582,16 +1584,15 @@ End radon_nikodym.
 Notation "'d nu '/d mu" := (Radon_Nikodym mu nu) : charge_scope.
 
 Section radon_nikodym_lemmas.
+Context d (T : measurableType d) (R : realType).
 
-Lemma dominates_cscale d (T : measurableType d) (R : realType)
-  (mu : {sigma_finite_measure set T -> \bar R})
-  (nu : {charge set T -> \bar R})
-  (c : R) : nu `<< mu -> cscale c nu `<< mu.
+Lemma dominates_cscale (mu : {sigma_finite_measure set T -> \bar R})
+    (nu : {charge set T -> \bar R}) (c : R) :
+  nu `<< mu -> cscale c nu `<< mu.
 Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed.
 
-Lemma Radon_Nikodym_cscale d (T : measurableType d) (R : realType)
-  (mu : {sigma_finite_measure set T -> \bar R})
-  (nu : {charge set T -> \bar R}) (c : R) :
+Lemma Radon_Nikodym_cscale (mu : {sigma_finite_measure set T -> \bar R})
+    (nu : {charge set T -> \bar R}) (c : R) :
   nu `<< mu ->
   ae_eq mu [set: T] ('d [the charge _ _ of cscale c nu] '/d mu)
                     (fun x => c%:E * 'd nu '/d mu x).
@@ -1606,17 +1607,14 @@ move=> numu; apply: integral_ae_eq => [//| | |E mE].
   by rewrite -Radon_Nikodym_integral.
 Qed.
 
-Lemma dominates_caddl d (T : measurableType d)
-  (R : realType) (mu : {sigma_finite_measure set T -> \bar R})
-  (nu0 nu1 : {charge set T -> \bar R}) :
-  nu0 `<< mu -> nu1 `<< mu ->
-  cadd nu0 nu1 `<< mu.
+Lemma dominates_caddl (mu : {sigma_finite_measure set T -> \bar R})
+    (nu0 nu1 : {charge set T -> \bar R}) :
+  nu0 `<< mu -> nu1 `<< mu -> cadd nu0 nu1 `<< mu.
 Proof.
 by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0.
 Qed.
 
-Lemma Radon_Nikodym_cadd d (T : measurableType d) (R : realType)
-    (mu : {sigma_finite_measure set T -> \bar R})
+Lemma Radon_Nikodym_cadd (mu : {sigma_finite_measure set T -> \bar R})
     (nu0 nu1 : {charge set T -> \bar R}) :
   nu0 `<< mu -> nu1 `<< mu ->
   ae_eq mu [set: T] ('d [the charge _ _ of cadd nu0 nu1] '/d mu)

theories/ereal.v

@@ -506,6 +506,9 @@ case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS.
 by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0).
 Qed.
 
+Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
+Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed.
+
 Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo].
 Proof.
 split.
@@ -518,14 +521,17 @@ Proof.
 by move=> x Sx; rewrite /ereal_inf lee_oppl; apply ereal_sup_ub; exists x.
 Qed.
 
+Lemma ereal_inf_le S x : (exists2 y, S y & y <= x) -> ereal_inf S <= x.
+Proof. by move=> [y Sy]; apply: le_trans; exact: ereal_inf_lb. Qed.
+
 Lemma ereal_inf_pinfty S : ereal_inf S = +oo <-> S `<=` [set +oo].
 Proof. rewrite eqe_oppLRP oppe_subset image_set1; exact: ereal_sup_ninfty. Qed.
 
 Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A <= B}.
-Proof. by move=> A B AB; apply ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
+Proof. by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
 
 Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B <= A}.
-Proof. by move=> A B AB; apply lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
+Proof. by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
 
 Lemma hasNub_ereal_sup (A : set (\bar R)) : ~ has_ubound A ->
   A !=set0 -> ereal_sup A = +oo%E.