fix, mv 1 lemma, marginally shorter scripts

CHANGELOG_UNRELEASED.md

@@ -42,8 +42,10 @@
 
 - in file `lebesgue_integral.v`,
   + new lemmas `simple_bounded`, `measurable_bounded_integrable`, 
-    `compact_finite_measure`, `approximation_continuous_integrable`, and
-    `cvge_harmonic`.
+    `compact_finite_measure`, `approximation_continuous_integrable`
+
+- in `sequences.v`:
+  + lemma `cvge_harmonic`
 
 - in `mathcomp_extra.v`:
   + lemmas `le_bigmax_seq`, `bigmax_sup_seq`
@@ -64,9 +66,12 @@
 - removed dependency in `Rstruct.v` on `normedtype.v`:
 - added dependency in `normedtype.v` on `Rstruct.v`:
 
-- in `cardinality.f`:
+- in `cardinality.v`:
   + implicits of `fimfunP`
 
+- in `lebesgue_integral.v`:
+  + implicits of `integral_le_bound`
+
 ### Renamed
 
 - in `normedtype.v`: 

theories/lebesgue_integral.v

@@ -403,7 +403,7 @@ Qed.
 Section simple_bounded.
 Context d (T : measurableType d) (R : realType).
 
-Lemma simple_bounded {f : {sfun T >-> R}} :
+Lemma simple_bounded (f : {sfun T >-> R}) :
   bounded_fun (f : T -> [normedModType R of R^o]).
 Proof.
 have /finite_seqP[r fr] := fimfunP f.
@@ -1757,7 +1757,6 @@ apply: le_lt_trans.
 by rewrite [_ eps]splitr EFinD lte_add.
 Qed.
 
-
 End lusin.
 
 Section emeasurable_fun.
@@ -4283,6 +4282,7 @@ by apply: ae_ge0_le_integral => //; exact: measurableT_comp.
 Qed.
 
 End integral_bounded.
+Arguments integral_le_bound {d T R mu D f} M.
 
 Section integral_ae_eq.
 Local Open Scope ereal_scope.
@@ -4760,21 +4760,19 @@ Section simple_density_L1.
 Context d (T : measurableType d) (R : realType).
 Variables (mu : {measure set T -> \bar R}) (E : set T) (mE : measurable E).
 
+Local Open Scope ereal_scope.
+
 Lemma measurable_bounded_integrable (f : T -> R^o)  :
-  (mu E < +oo)%E -> measurable_fun E f ->
+  mu E < +oo -> measurable_fun E f ->
   [bounded f x | x in E] -> mu.-integrable E (EFin \o f).
 Proof.
-move=> Afin mfA bdA; apply/integrableP; split.
-  exact/EFin_measurable_fun.
+move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun.
 have [M [_ mrt]] := bdA; apply: le_lt_trans.
-  apply (@integral_le_bound _ _ _ _ _ _ (`|M| + 1)%:E) => //.
-    by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun.
-  by apply: aeW => z Az; rewrite lee_fin mrt // ltr_spaddr// ler_norm.
+  apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp.
+  by apply: aeW => z Az; rewrite lee_fin mrt// ltr_spaddr// ler_norm.
 by rewrite lte_mul_pinfty.
 Qed.
 
-Local Open Scope ereal_scope.
-
 Let sfun_dense_L1_pos (f : T -> \bar R) :
   mu.-integrable E f -> (forall x, E x -> 0 <= f x) ->
   exists g_ : {sfun T >-> R}^nat,
@@ -4857,17 +4855,15 @@ Section continuous_density_L1.
 Context (rT : realType).
 Let mu := [the measure _ _ of @lebesgue_measure rT].
 Let R  := [the measurableType _ of measurableTypeR rT].
+Local Open Scope ereal_scope.
 
-Lemma compact_finite_measure (A : set R^o) :
-  compact A -> (mu A < +oo)%E.
+Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.
 Proof.
-move => /[dup]/compact_measurable => ?; case/compact_bounded => N [_ N1x].
-have AN1 : A `<=` `[- (`|N| + 1), `|N| + 1].
+move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]].
+have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R.
   by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm.
-apply: le_lt_trans; first apply: (le_measure _ _ _ AN1); first exact /mem_set.
-  by apply/mem_set; exact: measurable_itv.
-rewrite /= lebesgue_measure_itv hlength_itv /= -fun_if.
-by case E : (_%:E < _%:E)%E => //=; rewrite ltry.
+rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=.
+by rewrite lebesgue_measure_itv hlength_itv/= lte_fin gtr_opp// EFinD ltry.
 Qed.
 
 Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) :
@@ -4877,113 +4873,100 @@ move=> cptA ctsfA; apply: measurable_bounded_integrable.
 - exact: compact_measurable.
 - exact: compact_finite_measure.
 - by apply: subspace_continuous_measurable_fun => //; exact: compact_measurable.
-- have /compact_bounded [M [_ mrt]] := continuous_compact ctsfA cptA.
+- have /compact_bounded[M [_ mrt]] := continuous_compact ctsfA cptA.
   by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt.
 Qed.
 
-Lemma cvge_harmonic : (EFin \o (@harmonic rT)) @ \oo --> 0%E.
-Proof. by apply: cvg_EFin; [exact: nearW | exact: cvg_harmonic]. Qed.
-
-Local Open Scope ereal_scope.
 Local Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o):
   measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) ->
   exists g_ : (rT -> rT)^nat,
-    [/\ forall n, continuous (g_ n : R -> R),
+    [/\ forall n, continuous (g_ n),
         forall n, mu.-integrable E (EFin \o g_ n) &
         (fun n => \int[mu]_(z in E) `|(f z - g_ n z)%:E|) --> 0].
 Proof.
 move=> mE Efin intf.
-have mf : measurable_fun E f by case/integrableP:intf => /EFin_measurable_fun.
-suff apxf eps : exists (h : rT -> rT), (eps > 0)%R ->
+have mf : measurable_fun E f by case/integrableP : intf => /EFin_measurable_fun.
+suff apxf eps : exists h : rT -> rT, (eps > 0)%R ->
     [/\ continuous h,
         mu.-integrable E (EFin \o h) &
         \int[mu]_(z in E) `|(f z - h z)%:E| < eps%:E].
-  pose g_ (n : nat) := projT1 (cid (apxf (n.+1%:R^-1))); exists g_; split.
-  - by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //.
-  - by move=> n; have [] := projT2 (cid (apxf (n.+1%:R^-1))) => //.
+  pose g_ n := projT1 (cid (apxf n.+1%:R^-1)); exists g_; split.
+  - by move=> n; have [] := projT2 (cid (apxf n.+1%:R^-1)).
+  - by move=> n; have [] := projT2 (cid (apxf n.+1%:R^-1)).
   apply/cvg_ballP => eps epspos.
-  have /cvg_ballP/(_ eps epspos) [N _ Nball] := cvge_harmonic.
+  have /cvg_ballP/(_ eps epspos)[N _ Nball] := @cvge_harmonic rT.
   exists N => //; apply: (subset_trans Nball) => n.
-  rewrite /ball /= /ereal_ball contract0 ?mul0r ?sub0r ?normrN.
-  move/(lt_trans _); apply; rewrite ?ger0_norm; first last.
-  - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0 integral_ge0.
-  - by rewrite -le_expandLR //; rewrite ?inE ?normr0 // expand0.
-  have [] := projT2 (cid (apxf (n.+1%:R^-1))) => // ? ? ?.
-  by rewrite -lt_expandRL // ?contractK // inE contract_le1.
-case epspos: (0 < eps)%R; last by exists point.
-move: eps epspos => _/posnumP[eps].
-have [g [gfe2 ?]] : exists (g : {sfun R >-> rT}),
-    \int[mu]_(z in E) `|(f z - g z)%:E| < (eps%:num/2)%:E /\
+  rewrite /ball /= /ereal_ball contract0 !sub0r !normrN => /(lt_trans _); apply.
+  rewrite ?ger0_norm; first last.
+  - by rewrite -le_expandLR // ?inE ?normr0// expand0 integral_ge0.
+  - by rewrite -le_expandLR // ?inE ?normr0// expand0.
+  have [] := projT2 (cid (apxf n.+1%:R^-1)) => // _ _ ipaxfn.
+  by rewrite -lt_expandRL ?contractK// inE contract_le1.
+have [|] := ltP 0%R eps; last by exists point.
+move: eps => _/posnumP[eps].
+have [g [gfe2 ig]] : exists g : {sfun R >-> rT},
+    \int[mu]_(z in E) `|(f z - g z)%:E| < (eps%:num / 2)%:E /\
     mu.-integrable E (EFin \o g).
   have [g_ [intG ?]] := approximation_sfun_integrable mE intf.
-  case/fine_fcvg/cvg_ballP/(_ (eps%:num/2)) => // n _ Nb; exists (g_ n).
-  have ? : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num.
-    apply: integral_fune_fin_num => //; apply: integrable_abse.
-    under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //.
-    exact: intG.
-  split; last by exact: intG.
-  have /= := Nb _ (leqnn n); rewrite /ball /= sub0r normrN -fine_abse //.
-  rewrite -?lte_fin fineK ?abse_fin_num // => /(le_lt_trans _); apply.
-  by rewrite lee_abs.
-have mg : measurable_fun E (g : {mfun R >-> rT}(*NB(rei): shouldn't need this constraint, should we?*)).
+  move/fine_fcvg/cvg_ballP/(_ (eps%:num / 2)) => -[] // n _ Nb; exists (g_ n).
+  have fg_fin_num : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num.
+    rewrite integral_fune_fin_num// integrable_abse//.
+    by under eq_fun do rewrite EFinB; apply: integrableB => //; exact: intG.
+  split; last exact: intG.
+  have /= := Nb _ (leqnn n); rewrite /ball/= sub0r normrN -fine_abse// -lte_fin.
+  by rewrite fineK ?abse_fin_num// => /le_lt_trans; apply; exact: lee_abs.
+have mg : measurable_fun E g.
   by apply: (measurable_funS measurableT) => //; exact: measurable_funP.
-have [M [Mpos Mbd]] : (exists M, 0 < M /\ forall x, `|g x| <= M)%R.
-  case: (@simple_bounded _ _ _ g) => M [_ /= bdM].
-  exists (`|M| + 1)%R; split; first exact: ltr_spaddr.
-  by move=> x; apply: bdM => //; apply: ltr_spaddr; rewrite // ler_norm.
-have [] // := @measurable_almost_continuous rT E mE _ g (eps%:num/2/(M *+ 2)).
-  by apply: divr_gt0 => //; apply: mulrn_wgt0.
+have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R.
+  have [M [_ /= bdM]] := simple_bounded g.
+  exists (`|M| + 1)%R; first exact: ltr_spaddr.
+  by move=> x; rewrite bdM// ltr_spaddr// ler_norm.
+have [] // := @measurable_almost_continuous _ _ mE _ g (eps%:num / 2 / (M *+ 2)).
+  by rewrite divr_gt0// mulrn_wgt0.
 move=> A [cptA AE /= muAE ctsAF].
 have [] := continuous_bounded_extension _ _ Mpos ctsAF.
 - exact: pseudometric_normal.
-- by apply: compact_closed => //; exact: Rhausdorff .
+- by apply: compact_closed => //; exact: Rhausdorff.
 - by move=> ? ?; exact: Mbd.
-have mA : measurable A by exact: compact_measurable.
+have mA : measurable A := compact_measurable cptA.
 move=> h [gh ctsh hbdM]; have mh : measurable_fun E h.
-  apply: subspace_continuous_measurable_fun => //.
-  exact: continuous_subspaceT.
+  by apply: subspace_continuous_measurable_fun=> //; exact: continuous_subspaceT.
 have intg : mu.-integrable E (EFin \o h).
   apply: measurable_bounded_integrable => //.
-  exists M; split; rewrite ?num_real // => ? sx ? ? /=.
-  by apply: ltW; apply: (le_lt_trans _ sx); apply: hbdM.
+  exists M; split; rewrite ?num_real // => x Mx y _ /=.
+  by rewrite (le_trans _ (ltW Mx)).
 exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
-pose fgh x := (`|(f x - g x)%:E| + `|(g x - h x)%:E|).
-  apply (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //.
-  - apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)).
+  pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|.
+  apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //.
+  - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //.
     exact: measurable_funB.
   - by move=> z _; rewrite /fgh.
-  - rewrite /fgh; apply: measurableT_comp => //.
-    by apply: measurable_funD => //;
+  - apply: measurableT_comp => //; apply: measurable_funD => //;
       apply: (measurable_funS mE) => //; (apply: measurableT_comp => //);
       exact: measurable_funB.
-  - move=> x _; rewrite (_ : f x - h x = (f x - g x) + (g x - h x))%R.
-      rewrite lee_fin ler_norm_add //.
-    by rewrite -addrA [(- _ + _)%R]addrA [(-_ + _)%R]addrC subrr sub0r.
-rewrite integralD //; first last.
-- apply: integrable_abse.
-  by under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //.
-- apply: integrable_abse.
-  by under eq_fun => ? do rewrite ?EFinB; apply: integrableB => //.
-rewrite EFinD; apply: lte_add => //.
-rewrite -(setDKU AE) integral_setU => //; first last.
+  - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin.
+    by rewrite ler_norm_add.
+rewrite integralD//; first last.
+- by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB.
+- by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB.
+rewrite EFinD lte_add// -(setDKU AE) integral_setU => //; first last.
 - by rewrite /disj_set setDKI.
-- rewrite setDKU //; (do 2 (apply: measurableT_comp => //)).
+- rewrite setDKU //; do 2 apply: measurableT_comp => //.
   exact: measurable_funB.
 - exact: measurableD.
-rewrite (@ae_eq_integral _ _ _ mu A (fun=> 0)) //; first last.
-- by apply: aeW => z Az; rewrite (gh z) ?inE // subrr abse0.
-- apply: (measurable_funS mE) => //; (do 2 (apply: measurableT_comp => //)).
+rewrite (@ae_eq_integral _ _ _ mu A (cst 0)) //; first last.
+- by apply: aeW => z Az; rewrite (gh z) ?inE// subrr abse0.
+- apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //.
   exact: measurable_funB.
 rewrite integral0 adde0.
-apply: le_lt_trans; first apply: (@integral_le_bound _ _ _ _ _ _ (M *+ 2)%:E).
+apply: (le_lt_trans (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //.
 - exact: measurableD.
-- apply: (measurable_funS mE) => //; (apply: measurableT_comp => //).
+- apply: (measurable_funS mE) => //; apply: measurableT_comp => //.
   exact: measurable_funB.
-- by rewrite lee_fin mulrn_wge0 //; apply: ltW.
+- by rewrite lee_fin mulrn_wge0// ltW.
 - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n.
-  apply: le_trans; first exact: ler_norm_sub.
-  by apply: ler_add; [exact: Mbd | exact: hbdM].
-by rewrite -lte_pdivl_mull ? mulrn_wgt0 // muleC -EFinM.
+  by rewrite (le_trans (ler_norm_sub _ _))// ler_add.
+by rewrite -lte_pdivl_mull ?mulrn_wgt0// muleC -EFinM.
 Qed.
 
 End continuous_density_L1.
@@ -5624,16 +5607,16 @@ suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <=
   move=> intfeps; apply: le_trans.
     apply: (ler_pmul r20 _ (le_refl _)); first exact: fine_ge0.
     apply: fine_le; last apply: le_abse_integral => //.
-    - by rewrite abse_fin_num; exact: integral_fune_fin_num.
-    - by apply: integral_fune_fin_num => //; exact: integrable_abse.
-    - by case/integrableP: int_fx.
+    - by rewrite abse_fin_num integral_fune_fin_num.
+    - by rewrite integral_fune_fin_num// integrable_abse.
+    - by case/integrableP : int_fx.
   rewrite div1r ler_pdivr_mull ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)).
-  by rewrite fine_le // ?integral_fune_fin_num // ?integrable_abse.
+  by rewrite fine_le// integral_fune_fin_num// integrable_abse.
 apply: le_trans.
-  apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //.
-  - by case/integrableP: int_fx.
-  - exact: ltW.
-  - by apply: aeW => ? ?; rewrite /= lee_fin distrC; apply: feps.
+- apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //.
+  + by case/integrableP: int_fx.
+  + exact: ltW.
+  + by apply: aeW => ? ?; rewrite /= lee_fin distrC feps.
 by rewrite ritv //= -EFinM lee_fin mulrC.
 Unshelve. all: by end_near. Qed.
 

theories/sequences.v

@@ -771,6 +771,9 @@ rewrite (le_trans (ltW (archi_boundP _)))// ler_nat -add1n -leq_subLR.
 by near: i; apply: nbhs_infty_ge.
 Unshelve. all: by end_near. Qed.
 
+Lemma cvge_harmonic {R : archiFieldType} : (EFin \o @harmonic R) @ \oo --> 0%E.
+Proof. by apply: cvg_EFin; [exact: nearW | exact: cvg_harmonic]. Qed.
+
 Lemma dvg_harmonic (R : numFieldType) : ~ cvg (series (@harmonic R)).
 Proof.
 have ge_half n : (0 < n)%N -> 2^-1 <= \sum_(n <= i < n.*2) harmonic i.