Continuous functions are dense in L1 (#1015)

* simple functions are bounded

* continuous functions dense in simple

* updating changelog

* proving full theorem instead

* changelog

* shorter simple_bouned with bigmax lemmas

* fix, mv 1 lemma, marginally shorter scripts

* making lemma non-local

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -40,6 +40,19 @@
   + new definition `regular_space`.
   + new lemma `ent_closure`.
 
+- in file `lebesgue_integral.v`,
+  + new lemmas `simple_bounded`, `measurable_bounded_integrable`, 
+    `compact_finite_measure`, `approximation_continuous_integrable`
+
+- in `sequences.v`:
+  + lemma `cvge_harmonic`
+
+- in `mathcomp_extra.v`:
+  + lemmas `le_bigmax_seq`, `bigmax_sup_seq`
+
+- in `constructive_ereal.v`:
+  + lemma `bigmaxe_fin_num`
+
 ### Changed
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized
@@ -53,6 +66,12 @@
 - removed dependency in `Rstruct.v` on `normedtype.v`:
 - added dependency in `normedtype.v` on `Rstruct.v`:
 
+- in `cardinality.v`:
+  + implicits of `fimfunP`
+
+- in `lebesgue_integral.v`:
+  + implicits of `integral_le_bound`
+
 ### Renamed
 
 - in `normedtype.v`: 

classical/cardinality.v

@@ -1231,13 +1231,15 @@ HB.mixin Record FiniteImage aT rT (f : aT -> rT) := {
 }.
 HB.structure Definition FImFun aT rT := {f of @FiniteImage aT rT f}.
 
+Arguments fimfunP {aT rT} _.
+#[global] Hint Resolve fimfunP : core.
+
 Reserved Notation "{ 'fimfun' aT >-> T }"
   (at level 0, format "{ 'fimfun'  aT  >->  T }").
 Reserved Notation "[ 'fimfun' 'of' f ]"
   (at level 0, format "[ 'fimfun'  'of'  f ]").
 Notation "{ 'fimfun' aT >-> T }" := (@FImFun.type aT T) : form_scope.
 Notation "[ 'fimfun' 'of' f ]" := [the {fimfun _ >-> _} of f] : form_scope.
-#[global] Hint Resolve fimfunP : core.
 
 Lemma fimfun_inP {aT rT} (f : {fimfun aT >-> rT}) (D : set aT) :
   finite_set (f @` D).

classical/mathcomp_extra.v

@@ -869,3 +869,25 @@ Qed.
 End max_min.
 
 Notation trivial := (ltac:(done)).
+
+Section bigmax_seq.
+Context d {T : orderType d} {x : T} {I : eqType}.
+Variables (r : seq I) (i0 : I) (P : pred I).
+
+(* NB: as of [2023-08-28], bigop.leq_bigmax_seq already exists for nat *)
+Lemma le_bigmax_seq F :
+  i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- r | P i) F i)%O.
+Proof.
+move=> + Pi0; elim: r => // h t ih; rewrite inE big_cons.
+move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_maxr// lexx.
+by case: ifPn => Ph; [rewrite le_maxr ih// orbT|rewrite ih].
+Qed.
+
+(* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat *)
+Lemma bigmax_sup_seq (m : T) (F : I -> T) :
+  i0 \in r -> P i0 -> (m <= F i0)%O ->
+  (m <= \big[Order.max/x]_(i <- r | P i) F i)%O.
+Proof. by move=> i0r Pi0 ?; apply: le_trans (le_bigmax_seq _ _ _). Qed.
+
+End bigmax_seq.
+Arguments le_bigmax_seq {d T} x {I r} i0 P.

theories/constructive_ereal.v

@@ -2441,6 +2441,16 @@ Lemma mineMl z x y : z \is a fin_num -> 0 < z ->
   mine x y * z = mine (x * z) (y * z).
 Proof. by move=> zfin z0; rewrite muleC mineMr// !(muleC z). Qed.
 
+Lemma bigmaxe_fin_num (s : seq R) r : r \in s ->
+  \big[maxe/-oo%E]_(i <- s) i%:E \is a fin_num.
+Proof.
+move=> rs; have {rs} : s != [::].
+  by rewrite -size_eq0 -lt0n -has_predT; apply/hasP; exists r.
+elim: s => [[]//|a l]; have [-> _ _|_ /(_ isT) ih _] := eqVneq l [::].
+  by rewrite big_seq1.
+by rewrite big_cons {1}/maxe;  case: (_ < _)%E.
+Qed.
+
 Lemma lee_pemull x y : 0 <= y -> 1 <= x -> y <= x * y.
 Proof.
 move: x y => [x| |] [y| |] //; last by rewrite mulyy.

theories/kernel.v

@@ -1003,7 +1003,7 @@ HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n).
 
 Let fk_2 n : finite_set (range (k_2 n)).
 Proof.
-have := @fimfunP _ _ (k_ n).
+have := fimfunP (k_ n).
 suff : range (k_ n) = range (k_2 n) by move=> <-.
 by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2].
 Qed.

theories/lebesgue_integral.v

@@ -494,6 +494,23 @@ rewrite /preimage /= => [fxfy gzf].
 by rewrite gzf -fxfy addrC subrK.
 Qed.
 
+Section simple_bounded.
+Context d (T : measurableType d) (R : realType).
+
+Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f.
+Proof.
+have /finite_seqP[r fr] := fimfunP f.
+exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)).
+split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx).
+have ? : f z \in r by have := imageT f z; rewrite fr.
+rewrite -[leLHS]/(fine `|f z|%:E) fine_le//.
+  have := @bigmaxe_fin_num _ (map normr r) `|f z|.
+  by rewrite big_map => ->//; apply/mapP; exists (f z).
+by rewrite (bigmax_sup_seq _ _ (lexx _)).
+Qed.
+
+End simple_bounded.
+
 Section nnsfun_functions.
 Context d (T : measurableType d) (R : realType).
 
@@ -1729,7 +1746,7 @@ Let lusin_simple (f : {sfun R >-> rT}) (eps : rT) : (0 < eps)%R ->
   exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E &
   {within K, continuous f}].
 Proof.
-move: eps=> _/posnumP[eps]; have [N /card_fset_set rfN] := @fimfunP _ _ f.
+move: eps=> _/posnumP[eps]; have [N /card_fset_set rfN] := fimfunP f.
 pose Af x : set R := A `&` f @^-1` [set x].
 have mAf x : measurable (Af x) by exact: measurableI.
 have finAf x : mu (Af x) < +oo.
@@ -4363,6 +4380,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.
@@ -4842,6 +4860,17 @@ 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 -> measurable_fun E f ->
+  [bounded f x | x in E] -> mu.-integrable E (EFin \o f).
+Proof.
+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) => //; first exact: measurableT_comp.
+  by apply: aeW => z Az; rewrite lee_fin mrt// ltr_spaddr// ler_norm.
+by rewrite lte_mul_pinfty.
+Qed.
+
 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,
@@ -4920,9 +4949,128 @@ rewrite !ger0_norm ?fine_ge0 ?integral_ge0 ?fine_le//.
   + by move=> ? ?; rewrite fpn; exact: lee_abs_sub.
   + by move=> x Ex; rewrite adde_ge0.
 Unshelve. all: by end_near. Qed.
-
 End simple_density_L1.
 
+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.
+Proof.
+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.
+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) :
+  compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f).
+Proof.
+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.
+  by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt.
+Qed.
+
+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),
+        forall n, mu.-integrable E (EFin \o g_ n) &
+        \int[mu]_(z in E) `|(f z - g_ n z)%:E| @[n --> \oo] --> 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 ->
+    [/\ continuous h,
+        mu.-integrable E (EFin \o h) &
+        \int[mu]_(z in E) `|(f z - h z)%:E| < eps%:E].
+  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 rT.
+  exists N => //; apply: (subset_trans Nball) => n.
+  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.
+  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] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R.
+  have [M [_ /= bdM]] := simple_bounded g.
+  exists (`|M| + 1)%R; first exact: ltr_pwDr.
+  by move=> x; rewrite bdM// ltr_pwDr// 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 move=> ? ?; exact: Mbd.
+have mA : measurable A := compact_measurable cptA.
+move=> h [gh ctsh hbdM]; have mh : measurable_fun E h.
+  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 // => 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 => //.
+    exact: measurable_funB.
+  - by move=> z _; rewrite adde_ge0.
+  - apply: measurableT_comp => //; apply: measurable_funD => //;
+      apply: (measurable_funS mE) => //; (apply: measurableT_comp => //);
+      exact: measurable_funB.
+  - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin.
+    by rewrite ler_normD.
+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 => //.
+  exact: measurable_funB.
+- exact: measurableD.
+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 (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //.
+- exact: measurableD.
+- apply: (measurable_funS mE) => //; apply: measurableT_comp => //.
+  exact: measurable_funB.
+- by rewrite lee_fin mulrn_wge0// ltW.
+- apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n.
+  by rewrite (le_trans (ler_normB _ _))// lerD.
+by rewrite -lte_pdivl_mull ?mulrn_wgt0// muleC -EFinM.
+Qed.
+
+End continuous_density_L1.
+
 Section fubini_functions.
 Local Open Scope ereal_scope.
 Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
@@ -5497,25 +5645,6 @@ Context (rT : realType).
 Let mu := [the measure _ _ of @lebesgue_measure rT].
 Let R  := [the measurableType _ of measurableTypeR rT].
 
-Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) :
-  compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f).
-Proof.
-move=> cptA ctsfA; have mA := compact_measurable cptA; apply/integrableP; split.
-  by apply: measurableT_comp => //; exact: subspace_continuous_measurable_fun.
-have /compact_bounded [M [_ mrt]] := continuous_compact ctsfA cptA.
-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.
-case/compact_bounded : cptA => N [_ N1x].
-have AN1 : A `<=` `[- (`|N| + 1), `|N| + 1].
-  by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm.
-apply: (@le_lt_trans _ _ (_ * _)%E).
-  by rewrite lee_pmul; last by apply: (le_measure _ _ _ AN1); rewrite inE.
-rewrite /= lebesgue_measure_itv hlength_itv /=.
-by case: ifPn => /=; rewrite ?mule0// -EFinM ltry.
-Qed.
-
 Let ballE (x : R) (r : {posnum rT}) :
   ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT.
 Proof.
@@ -5530,8 +5659,8 @@ Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) :
 Proof.
 have ball_itvr r : 0 < r -> `[x - r, x + r] `\` ball x r = [set x + r; x - r].
   move: r => _/posnumP[r].
-  rewrite -setU1itv ?bnd_simp ?ler_subl_addr -?addrA ?ler_paddr//.
-  rewrite -setUitv1 ?bnd_simp ?ltr_subl_addr -?addrA ?ltr_spaddr//.
+  rewrite -setU1itv ?bnd_simp ?lerBlDr -?addrA ?ler_wpDr//.
+  rewrite -setUitv1 ?bnd_simp ?ltrBlDr -?addrA ?ltr_pwDr//.
   rewrite setUA setUC setUA setDUl !ballE setDv setU0 setDidl// -subset0.
   by move=> z /= [[]] ->; rewrite in_itv/= ltxx// andbF.
 have ball_itv2 r : 0 < r -> ball x r = `[x - r, x + r] `\` [set x + r; x - r].
@@ -5540,7 +5669,7 @@ have ball_itv2 r : 0 < r -> ball x r = `[x - r, x + r] `\` [set x + r; x - r].
   by rewrite ballE set_itvcc => ?/=; rewrite in_itv => /andP [/ltW -> /ltW ->].
 have ritv r : 0 < r -> mu `[x - r, x + r]%classic = (r *+ 2)%:E.
   move=> /gt0_cp rE; rewrite /= lebesgue_measure_itv hlength_itv /= lte_fin.
-  rewrite ler_lt_add // ?rE // -EFinD; congr (_ _).
+  rewrite ler_ltD // ?rE // -EFinD; congr (_ _).
   by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r.
 move=> oA intf ctsfx Ax.
 apply: cvg_zero.
@@ -5581,16 +5710,16 @@ suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <=
   move=> intfeps; apply: le_trans.
     apply: (ler_pM 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_pdivrMl ?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

@@ -779,6 +779,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) : ~ cvgn (series (@harmonic R)).
 Proof.
 have ge_half n : (0 < n)%N -> 2^-1 <= \sum_(n <= i < n.*2) harmonic i.