Lebesgue differentiation for continuous functions (#972)

* interval topology facts

* weakening continuity

* minor improvements

- minor gen. of integral_le_bound
- move lemmas to more appropriate locations
- rebase on master to use measurable_compact

* using ball instead of intervals in the statement

* using natmul notation

---------

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

CHANGELOG_UNRELEASED.md

@@ -23,12 +23,25 @@
 - in `exp.v`:
   + lemmas `concave_ln`, `conjugate_powR`
 
+- in file `lebesgue_integral.v`,
+  + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and 
+    `lebesgue_differentiation_continuous`.
+
+- in `normedtype.v`:
+  + lemmas `open_itvoo_subset`, `open_itvcc_subset`
+
+- in `lebesgue_measure.v`:
+  + lemma `measurable_ball`
+
 ### Changed
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized
 - in `constructive_ereal.v`:
   + `lee_adde` renamed to `lee_addgt0Pr` and turned into a reflect
   + `lee_dadde` renamed to `lee_daddgt0Pr` and turned into a reflect
+- in `lebesgue_integral.v`
+  + rewrote `negligible_integral` to replace the positivity condition
+    with an integrability condition, and added `ge0_negligible_integral`.
 
 ### Renamed
 

theories/lebesgue_integral.v

@@ -3634,7 +3634,7 @@ have h2 : mu.-integrable (D `\` N) f <->
 by apply: (iff_trans h1); exact: iff_sym.
 Qed.
 
-Lemma negligible_integral (D N : set T) (f : T -> \bar R) :
+Lemma ge0_negligible_integral (D N : set T) (f : T -> \bar R) :
   measurable N -> measurable D -> measurable_fun D f ->
   (forall x, D x -> 0 <= f x) ->
   mu N = 0 -> \int[mu]_(x in D) f x = \int[mu]_(x in D `\` N) f x.
@@ -3663,10 +3663,10 @@ Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) :
 Proof.
 move=> mD mf mg f0 g0 [N [mN N0 subN]].
 rewrite integralEindic// [RHS]integralEindic//.
-rewrite (negligible_integral mN)//; last 2 first.
+rewrite (ge0_negligible_integral mN)//; last 2 first.
   - by apply: emeasurable_funM => //; exact/EFin_measurable_fun.
   - by move=> x Dx; apply: mule_ge0 => //; [exact: f0|rewrite lee_fin].
-rewrite [RHS](negligible_integral mN)//; last 2 first.
+rewrite [RHS](ge0_negligible_integral mN)//; last 2 first.
   - by apply: emeasurable_funM => //; exact/EFin_measurable_fun.
   - by move=> x Dx; apply: mule_ge0 => //; [exact: g0|rewrite lee_fin].
 - apply: eq_integral => x;rewrite in_setD => /andP[_ xN].
@@ -3839,6 +3839,31 @@ Qed.
 
 End integralB.
 
+Section negligible_integral.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType)
+        (mu : {measure set T -> \bar R}).
+
+Lemma negligible_integral (D N : set T) (f : T -> \bar R) :
+  measurable N -> measurable D -> mu.-integrable D f ->
+  mu N = 0 -> \int[mu]_(x in D) f x = \int[mu]_(x in D `\` N) f x.
+Proof.
+move=> mN mD mf muN0; rewrite [f]funeposneg ?integralB //; first last.
+- exact: integrable_funeneg.
+- exact: integrable_funepos.
+- apply: (integrableS mD) => //; first exact: measurableD.
+  exact: integrable_funeneg.
+- apply: (integrableS mD) => //; first exact: measurableD.
+  exact: integrable_funepos.
+- exact: measurableD.
+congr (_ - _); apply: ge0_negligible_integral => //; apply: measurable_int.
+  exact: (integrable_funepos mD mf).
+exact: (integrable_funeneg mD mf).
+Qed.
+
+End negligible_integral.
+Add Search Blacklist "ge0_negligible_integral".
+
 Section integrable_fune.
 Context d (T : measurableType d) (R : realType).
 Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
@@ -3863,6 +3888,7 @@ Qed.
 
 End integrable_fune.
 
+
 Section integral_counting.
 Local Open Scope ereal_scope.
 Variable R : realType.
@@ -4211,8 +4237,8 @@ Hypothesis mf2 : measurable_fun D f2.
 Lemma ae_ge0_le_integral : {ae mu, forall x, D x -> f1 x <= f2 x} ->
   \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x.
 Proof.
-move=> [N [mN muN f1f2N]]; rewrite (negligible_integral _ _ _ _ muN)//.
-rewrite [leRHS](negligible_integral _ _ _ _ muN)//.
+move=> [N [mN muN f1f2N]]; rewrite (ge0_negligible_integral _ _ _ _ muN)//.
+rewrite [leRHS](ge0_negligible_integral _ _ _ _ muN)//.
 apply: ge0_le_integral; first exact: measurableD.
 - by move=> t [Dt _]; exact: f10.
 - exact: measurable_funS mf1.
@@ -4223,6 +4249,22 @@ Qed.
 
 End ae_ge0_le_integral.
 
+Section integral_bounded.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Local Open Scope ereal_scope.
+
+Lemma integral_le_bound (D : set T) (f : T -> \bar R) (M : \bar R) :
+  measurable D -> measurable_fun D f -> 0 <= M ->
+  {ae mu, forall x, D x -> `|f x| <= M} ->
+  \int[mu]_(x in D) `|f x| <= M * mu D.
+Proof.
+move=> mD mf M0 dfx; rewrite -integral_cst => //.
+by apply: ae_ge0_le_integral => //; exact: measurableT_comp.
+Qed.
+
+End integral_bounded.
+
 Section integral_ae_eq.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}).
@@ -5345,3 +5387,106 @@ Qed.
 
 End sfinite_fubini.
 Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
+
+Section lebesgue_differentiation.
+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.
+by rewrite /= lebesgue_measure_itv hlength_itv /= -fun_if -EFinM ltry.
+Qed.
+
+Let ballE (x : R) (r : {posnum rT}) :
+  ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT.
+Proof.
+rewrite -(@ball_normE rT [normedModType rT of R^o]) /ball_ set_itvoo.
+by under eq_set => ? do rewrite ltr_distlC.
+Qed.
+
+Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) :
+  open A -> mu.-integrable A (EFin \o f) -> {for x, continuous f} -> A x ->
+  (fun r => 1 / (r *+ 2) * \int[mu]_(z in ball x r) f z) @ 0^'+ -->
+  (f x : R^o).
+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 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].
+  move: r => _/posnumP[r].
+  rewrite -ball_itvr // setDD setIC; apply/esym/setIidPl.
+  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 (_ _).
+  by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r.
+move=> oA intf ctsfx Ax.
+apply: (@cvg_zero rT [normedModType R of rT^o]).
+apply/cvgrPdist_le => eps epos; apply: filter_app (@nbhs_right_gt rT 0).
+have ? : Filter (nbhs (0 : R)^'+) := at_right_proper_filter 0.
+move/cvgrPdist_le/(_ eps epos)/at_right_in_segment : ctsfx; apply: filter_app.
+apply: filter_app (open_itvcc_subset oA Ax).
+have mA : measurable A := open_measurable oA.
+near=> r => xrA; rewrite addrfctE opprfctE => feps rp.
+have cptxr : compact `[x - r, x + r] := @segment_compact _ _ _.
+rewrite distrC subr0.
+have -> : \int[mu]_(z in ball x r) f z = \int[mu]_(z in `[x - r, x + r]) f z.
+  rewrite ball_itv2 //; congr (fine _); rewrite -negligible_integral //.
+  - by apply/measurableU; exact: measurable_set1.
+  - exact: (integrableS mA).
+  - by rewrite measureU0//; exact: lebesgue_measure_set1.
+have r20 : 0 <= 1 / (r *+ 2) by rewrite ?divr_ge0 // mulrn_wge0.
+have -> : f x = 1 / (r *+ 2) * \int[mu]_(z in `[x - r, x + r]) cst (f x) z.
+  rewrite /Rintegral /= integral_cst /= ?ritv // mulrC mul1r.
+  by rewrite -mulrA divff ?mulr1//; apply: lt0r_neq0; rewrite mulrn_wgt0.
+have intRf : mu.-integrable `[x - r, x + r] (EFin \o f).
+  exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf).
+rewrite /= -mulrBr -fineB; first last.
+- rewrite integral_fune_fin_num// continuous_compact_integrable// => ?.
+  exact: cvg_cst.
+- by rewrite integral_fune_fin_num.
+rewrite -integralB_EFin //; first last.
+  by apply: continuous_compact_integrable => // ?; exact: cvg_cst.
+under [fun _ => adde _ _ ]eq_fun => ? do rewrite -EFinD.
+have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E).
+  under [fun z => (f z - _)%:E]eq_fun => ? do rewrite EFinB.
+  rewrite integrableB// continuous_compact_integrable// => ?.
+  exact: cvg_cst.
+rewrite normrM [ `|_/_| ]ger0_norm // -fine_abse //; first last.
+  by rewrite integral_fune_fin_num.
+suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <=
+    (r *+ 2 * eps)%:E)%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.
+  rewrite div1r ler_pdivr_mull ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)).
+  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.
+by rewrite ritv //= -EFinM lee_fin mulrC.
+Unshelve. all: by end_near. Qed.
+
+End lebesgue_differentiation.

theories/lebesgue_measure.v

@@ -1424,6 +1424,12 @@ move=> q; case: ifPn => // qfab; apply: is_interval_measurable => //.
 exact: is_interval_bigcup_ointsub.
 Qed.
 
+Lemma measurable_ball (r x : R) : 0 < r -> measurable (ball x r).
+Proof.
+move=> ?; apply: open_measurable.
+exact: (@ball_open _ [normedModType R of R^o]).
+Qed.
+
 Lemma open_measurable_subspace (D : set R) (U : set (subspace D)) :
   measurable D -> open U -> measurable (D `&` U).
 Proof.

theories/normedtype.v

@@ -1951,6 +1951,33 @@ End at_left_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.
 Notation "x ^'+" := (at_right x) : classical_set_scope.
 
+Section open_itv_subset.
+Context {R : realType}.
+Variables (A : set R) (x : R).
+
+Lemma open_itvoo_subset :
+  open A -> A x -> \forall r \near 0^'+, `]x - r, x + r[ `<=` A.
+Proof.
+move=> /[apply] -[] _/posnumP[r] /subset_ball_prop_in_itv xrA.
+exists r%:num => //= k; rewrite /= distrC subr0 set_itvoo => /ltr_normlW kr k0.
+by apply/(subset_trans _ xrA)/subset_itvW;
+  [rewrite ler_sub//; exact: ltW | rewrite ler_add//; exact: ltW].
+Qed.
+
+Lemma open_itvcc_subset :
+  open A -> A x -> \forall r \near 0^'+, `[x - r, x + r] `<=` A.
+Proof.
+move=> /[apply] -[] _/posnumP[r].
+have -> : r%:num = 2 * (r%:num / 2) by rewrite mulrCA divff// mulr1.
+move/subset_ball_prop_in_itvcc => /= xrA; exists (r%:num / 2) => //= k.
+rewrite /= distrC subr0 set_itvcc => /ltr_normlW kr k0.
+move=> z /andP [xkz zxk]; apply: xrA => //; rewrite in_itv/=; apply/andP; split.
+  by rewrite (le_trans _ xkz)// ler_sub// ltW.
+by rewrite (le_trans zxk)// ler_add// ltW.
+Qed.
+
+End open_itv_subset.
+
 Section at_left_right_topologicalType.
 Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R).