feat: The convolution of a locally integrable function f with a seque…

…nce of bump functions converges ae to f (#6102)

Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

@@ -5,11 +5,14 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Analysis.Convolution
 import Mathlib.Analysis.Calculus.BumpFunction.Normed
+import Mathlib.MeasureTheory.Integral.Average
+import Mathlib.MeasureTheory.Covering.Differentiation
+import Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
 
 #align_import analysis.convolution from "leanprover-community/mathlib"@"8905e5ed90859939681a725b00f6063e65096d95"
 
 /-!
-# Convolution of a bump function
+# Convolution with a bump function
 
 In this file we prove lemmas about convolutions `(φ.normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀`,
 where `φ : ContDiffBump 0` is a smooth bump function.
@@ -25,6 +28,9 @@ We also provide estimates in the case if `g x` is close to `g x₀` on this ball
   If `(φ i).rOut` tends to zero along a filter `l`,
   then `((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀` tends to `g x₀` along the same filter.
 - `ContDiffBump.convolution_tendsto_right`: generalization of the above lemma.
+- `ContDiffBump.ae_convolution_tendsto_right_of_locally_integrable`: let `g` be a locally
+  integrable function. Then the convolution of `g` with a family of bump functions with
+  support tending to `0` converges almost everywhere to `g`.
 
 ## Keywords
 
@@ -33,7 +39,7 @@ convolution, smooth function, bump function
 
 universe uG uE'
 
-open ContinuousLinearMap Metric MeasureTheory Filter Function
+open ContinuousLinearMap Metric MeasureTheory Filter Function Measure Set
 open scoped Convolution Topology
 
 namespace ContDiffBump
@@ -83,7 +89,7 @@ nonrec theorem convolution_tendsto_right {ι} {φ : ι → ContDiffBump (0 : G)}
     {k : ι → G} {x₀ : G} {z₀ : E'} {l : Filter ι} (hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0))
     (hig : ∀ᶠ i in l, AEStronglyMeasurable (g i) μ) (hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀))
     (hk : Tendsto k l (𝓝 x₀)) :
-    Tendsto (fun i => ((fun x => (φ i).normed μ x) ⋆[lsmul ℝ ℝ, μ] g i : G → E') (k i)) l (𝓝 z₀) :=
+    Tendsto (fun i => ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀) :=
   convolution_tendsto_right (eventually_of_forall fun i => (φ i).nonneg_normed)
     (eventually_of_forall fun i => (φ i).integral_normed) (tendsto_support_normed_smallSets hφ) hig
     hcg hk
@@ -93,9 +99,46 @@ nonrec theorem convolution_tendsto_right {ι} {φ : ι → ContDiffBump (0 : G)}
   and the limit is taken only in the first function. -/
 theorem convolution_tendsto_right_of_continuous {ι} {φ : ι → ContDiffBump (0 : G)} {l : Filter ι}
     (hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)) (hg : Continuous g) (x₀ : G) :
-    Tendsto (fun i => ((fun x => (φ i).normed μ x) ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀) l (𝓝 (g x₀)) :=
+    Tendsto (fun i => ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀)) :=
   convolution_tendsto_right hφ (eventually_of_forall fun _ => hg.aestronglyMeasurable)
     ((hg.tendsto x₀).comp tendsto_snd) tendsto_const_nhds
 #align cont_diff_bump.convolution_tendsto_right_of_continuous ContDiffBump.convolution_tendsto_right_of_continuous
 
+local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y) -- Porting note: See issue #2220
+
+/-- If a function `g` is locally integrable, then the convolution `φ i * g` converges almost
+everywhere to `g` if `φ i` is a sequence of bump functions with support tending to `0`, provided
+that the ratio between the inner and outer radii of `φ i` remains bounded. -/
+theorem ae_convolution_tendsto_right_of_locally_integrable
+    {ι} {φ : ι → ContDiffBump (0 : G)} {l : Filter ι} {K : ℝ}
+    (hφ : Tendsto (fun i ↦ (φ i).rOut) l (𝓝 0))
+    (h'φ : ∀ᶠ i in l, (φ i).rOut ≤ K * (φ i).rIn) (hg : LocallyIntegrable g μ) : ∀ᵐ x₀ ∂μ,
+    Tendsto (fun i ↦ ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀)) := by
+  have : IsAddHaarMeasure μ := ⟨⟩
+  -- By Lebesgue differentiation theorem, the average of `g` on a small ball converges
+  -- almost everywhere to the value of `g` as the radius shrinks to zero.
+  -- We will see that this set of points satisfies the desired conclusion.
+  filter_upwards [(Besicovitch.vitaliFamily μ).ae_tendsto_average_norm_sub hg] with x₀ h₀
+  simp only [convolution_eq_swap, lsmul_apply]
+  have hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0) :=
+    tendsto_nhdsWithin_iff.2 ⟨hφ, eventually_of_forall (fun i ↦ (φ i).rOut_pos)⟩
+  have := (h₀.comp (Besicovitch.tendsto_filterAt μ x₀)).comp hφ'
+  simp only [Function.comp] at this
+  apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (FiniteDimensional.finrank ℝ G)) this
+  · apply eventually_of_forall (fun i ↦ ?_)
+    apply hg.integrableOn_isCompact
+    exact isCompact_closedBall _ _
+  · apply tendsto_const_nhds.congr (fun i ↦ ?_)
+    rw [← integral_neg_eq_self]
+    simp only [sub_neg_eq_add, integral_add_left_eq_self, integral_normed]
+  · apply eventually_of_forall (fun i ↦ ?_)
+    change support ((ContDiffBump.normed (φ i) μ) ∘ (fun y ↦ x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
+    simp only [support_comp_eq_preimage, support_normed_eq]
+    intro x hx
+    simp only [mem_preimage, mem_ball, dist_zero_right] at hx
+    simpa [dist_eq_norm_sub'] using hx.le
+  · filter_upwards [h'φ] with i hi x
+    rw [abs_of_nonneg (nonneg_normed _ _), addHaar_closedBall_center]
+    exact (φ i).normed_le_div_measure_closedBall_rOut _ _ hi _
+
 end ContDiffBump

Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

@@ -5,6 +5,7 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Analysis.Calculus.BumpFunction.Basic
 import Mathlib.MeasureTheory.Integral.SetIntegral
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 
 #align_import analysis.calculus.bump_function_inner from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
 
@@ -17,7 +18,7 @@ In this file we define `ContDiffBump.normed f μ` to be the bump function `f` no
 
 noncomputable section
 
-open Function Filter Set Metric MeasureTheory
+open Function Filter Set Metric MeasureTheory FiniteDimensional Measure
 open scoped Topology
 
 namespace ContDiffBump
@@ -107,4 +108,58 @@ theorem integral_normed_smul {X} [NormedAddCommGroup X] [NormedSpace ℝ X]
   simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]
 #align cont_diff_bump.integral_normed_smul ContDiffBump.integral_normed_smul
 
+theorem measure_closedBall_le_integral : (μ (closedBall c f.rIn)).toReal ≤ ∫ x, f x ∂μ := by calc
+  (μ (closedBall c f.rIn)).toReal = ∫ x in closedBall c f.rIn, 1 ∂μ := by simp
+  _ = ∫ x in closedBall c f.rIn, f x ∂μ := set_integral_congr (measurableSet_closedBall)
+        (fun x hx ↦ (one_of_mem_closedBall f hx).symm)
+  _ ≤ ∫ x, f x ∂μ := set_integral_le_integral f.integrable (eventually_of_forall (fun x ↦ f.nonneg))
+
+theorem normed_le_div_measure_closedBall_rIn (x : E) :
+    f.normed μ x ≤ 1 / (μ (closedBall c f.rIn)).toReal := by
+  rw [normed_def]
+  gcongr
+  · exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rIn_pos).ne' measure_closedBall_lt_top.ne
+  · exact f.le_one
+  · exact f.measure_closedBall_le_integral μ
+
+theorem integral_le_measure_closedBall : ∫ x, f x ∂μ ≤ (μ (closedBall c f.rOut)).toReal := by calc
+  ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ := by
+    apply (set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
+    apply f.zero_of_le_dist (le_of_lt _)
+    simpa using hx
+  _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ := by
+    apply set_integral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
+    simp [measure_closedBall_lt_top]
+  _ = (μ (closedBall c f.rOut)).toReal := by simp
+
+local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y) -- Porting note: See Lean 4 issue #2220
+
+theorem measure_closedBall_div_le_integral [IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn) :
+    (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ x, f x ∂μ := by
+  have K_pos : 0 < K := by
+    simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
+  apply le_trans _ (f.measure_closedBall_le_integral μ)
+  rw [div_le_iff (pow_pos K_pos _), addHaar_closedBall' _ _ f.rIn_pos.le,
+    addHaar_closedBall' _ _ f.rOut_pos.le, ENNReal.toReal_mul, ENNReal.toReal_mul,
+    ENNReal.toReal_ofReal (pow_nonneg f.rOut_pos.le _),
+    ENNReal.toReal_ofReal (pow_nonneg f.rIn_pos.le _), mul_assoc, mul_comm _ (K ^ _), ← mul_assoc,
+    ← mul_pow, mul_comm _ K]
+  gcongr
+  exact f.rOut_pos.le
+
+theorem normed_le_div_measure_closedBall_rOut [IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn)
+    (x : E) :
+    f.normed μ x ≤ K ^ finrank ℝ E / (μ (closedBall c f.rOut)).toReal := by
+  have K_pos : 0 < K := by
+    simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
+  have : f x / ∫ y, f y ∂μ ≤ 1 / ∫ y, f y ∂μ := by
+    gcongr
+    · exact f.integral_pos.le
+    · exact f.le_one
+  apply this.trans
+  rw [div_le_div_iff f.integral_pos, one_mul, ← div_le_iff' (pow_pos K_pos _)]
+  · exact f.measure_closedBall_div_le_integral μ K h
+  · exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rOut_pos).ne'
+      measure_closedBall_lt_top.ne
+
 end ContDiffBump

Mathlib/MeasureTheory/Covering/DensityTheorem.lean

@@ -153,7 +153,7 @@ theorem ae_tendsto_measure_inter_div (S : Set α) (K : ℝ) : ∀ᵐ x ∂μ.res
 
 /-- A version of **Lebesgue differentiation theorem** for a sequence of closed balls whose
 centers are not required to be fixed. -/
-theorem ae_tendsto_average_norm_sub {f : α → E} (hf : Integrable f μ) (K : ℝ) : ∀ᵐ x ∂μ,
+theorem ae_tendsto_average_norm_sub {f : α → E} (hf : LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ x ∂μ,
     ∀ {ι : Type _} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (δlim : Tendsto δ l (𝓝[>] 0))
       (xmem : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)),
       Tendsto (fun j => ⨍ y in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0) := by
@@ -163,8 +163,8 @@ theorem ae_tendsto_average_norm_sub {f : α → E} (hf : Integrable f μ) (K : 
 
 /-- A version of **Lebesgue differentiation theorem** for a sequence of closed balls whose
 centers are not required to be fixed. -/
-theorem ae_tendsto_average [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : Integrable f μ)
-    (K : ℝ) : ∀ᵐ x ∂μ,
+theorem ae_tendsto_average [NormedSpace ℝ E] [CompleteSpace E]
+    {f : α → E} (hf : LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ x ∂μ,
       ∀ {ι : Type _} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (δlim : Tendsto δ l (𝓝[>] 0))
         (xmem : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)),
         Tendsto (fun j => ⨍ y in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x)) := by

Mathlib/MeasureTheory/Covering/Differentiation.lean

@@ -772,7 +772,6 @@ theorem ae_tendsto_measure_inter_div (s : Set α) :
 
 /-! ### Lebesgue differentiation theorem -/
 
-
 theorem ae_tendsto_lintegral_div' {f : α → ℝ≥0∞} (hf : Measurable f) (h'f : (∫⁻ y, f y ∂μ) ≠ ∞) :
     ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x)) := by
   let ρ := μ.withDensity f
@@ -799,7 +798,7 @@ theorem ae_tendsto_lintegral_div {f : α → ℝ≥0∞} (hf : AEMeasurable f μ
   exact ae_restrict_of_ae hf.ae_eq_mk
 #align vitali_family.ae_tendsto_lintegral_div VitaliFamily.ae_tendsto_lintegral_div
 
-theorem ae_tendsto_lintegral_nnnorm_sub_div' {f : α → E} (hf : Integrable f μ)
+theorem ae_tendsto_lintegral_nnnorm_sub_div'_of_integrable {f : α → E} (hf : Integrable f μ)
     (h'f : StronglyMeasurable f) :
     ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0) := by
   /- For every `c`, then `(∫⁻ y in a, ‖f y - c‖₊ ∂μ) / μ a` tends almost everywhere to `‖f x - c‖`.
@@ -873,12 +872,12 @@ theorem ae_tendsto_lintegral_nnnorm_sub_div' {f : α → E} (hf : Integrable f 
       · simp only [lintegral_const, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
         exact mul_le_mul_right' xc.le _
     _ = ε * μ a := by rw [← add_mul, ENNReal.add_halves]
-#align vitali_family.ae_tendsto_lintegral_nnnorm_sub_div' VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'
+#align vitali_family.ae_tendsto_lintegral_nnnorm_sub_div' VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'_of_integrable
 
-theorem ae_tendsto_lintegral_nnnorm_sub_div {f : α → E} (hf : Integrable f μ) :
+theorem ae_tendsto_lintegral_nnnorm_sub_div_of_integrable {f : α → E} (hf : Integrable f μ) :
     ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0) := by
   have I : Integrable (hf.1.mk f) μ := hf.congr hf.1.ae_eq_mk
-  filter_upwards [v.ae_tendsto_lintegral_nnnorm_sub_div' I hf.1.stronglyMeasurable_mk,
+  filter_upwards [v.ae_tendsto_lintegral_nnnorm_sub_div'_of_integrable I hf.1.stronglyMeasurable_mk,
     hf.1.ae_eq_mk] with x hx h'x
   apply hx.congr _
   intro a
@@ -887,45 +886,69 @@ theorem ae_tendsto_lintegral_nnnorm_sub_div {f : α → E} (hf : Integrable f μ
   apply ae_restrict_of_ae
   filter_upwards [hf.1.ae_eq_mk] with y hy
   rw [hy, h'x]
-#align vitali_family.ae_tendsto_lintegral_nnnorm_sub_div VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div
+#align vitali_family.ae_tendsto_lintegral_nnnorm_sub_div VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div_of_integrable
+
+theorem ae_tendsto_lintegral_nnnorm_sub_div {f : α → E} (hf : LocallyIntegrable f μ) :
+    ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0) := by
+  rcases hf.exists_nat_integrableOn with ⟨u, u_open, u_univ, hu⟩
+  have : ∀ n, ∀ᵐ x ∂μ,
+      Tendsto (fun a => (∫⁻ y in a, ‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a)
+      (v.filterAt x) (𝓝 0) := by
+    intro n
+    apply ae_tendsto_lintegral_nnnorm_sub_div_of_integrable
+    exact (integrable_indicator_iff (u_open n).measurableSet).2 (hu n)
+  filter_upwards [ae_all_iff.2 this] with x hx
+  obtain ⟨n, hn⟩ : ∃ n, x ∈ u n := by simpa only [← u_univ, mem_iUnion] using mem_univ x
+  apply Tendsto.congr' _ (hx n)
+  filter_upwards [v.eventually_filterAt_subset_of_nhds ((u_open n).mem_nhds hn),
+    v.eventually_filterAt_measurableSet x] with a ha h'a
+  congr 1
+  refine' set_lintegral_congr_fun h'a (eventually_of_forall (fun y hy ↦ _))
+  rw [indicator_of_mem (ha hy) f, indicator_of_mem hn f]
+
+theorem eventually_filterAt_integrableOn (x : α) {f : α → E} (hf : LocallyIntegrable f μ) :
+    ∀ᶠ a in v.filterAt x, IntegrableOn f a μ := by
+  rcases hf x with ⟨w, w_nhds, hw⟩
+  filter_upwards [v.eventually_filterAt_subset_of_nhds w_nhds] with a ha
+  exact hw.mono_set ha
 
 /-- *Lebesgue differentiation theorem*: for almost every point `x`, the
 average of `‖f y - f x‖` on `a` tends to `0` as `a` shrinks to `x` along a Vitali family.-/
-theorem ae_tendsto_average_norm_sub {f : α → E} (hf : Integrable f μ) :
+theorem ae_tendsto_average_norm_sub {f : α → E} (hf : LocallyIntegrable f μ) :
     ∀ᵐ x ∂μ, Tendsto (fun a => ⨍ y in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0) := by
-  filter_upwards [v.ae_tendsto_lintegral_nnnorm_sub_div hf, v.ae_eventually_measure_pos] with x hx
-    h'x
+  filter_upwards [v.ae_tendsto_lintegral_nnnorm_sub_div hf] with x hx
   have := (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hx
   simp only [ENNReal.zero_toReal] at this
   apply Tendsto.congr' _ this
-  filter_upwards [h'x, v.eventually_measure_lt_top x] with a _ h'a
+  filter_upwards [v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf]
+    with a h'a h''a
   simp only [Function.comp_apply, ENNReal.toReal_div, setAverage_eq, div_eq_inv_mul]
   have A : IntegrableOn (fun y => (‖f y - f x‖₊ : ℝ)) a μ := by
     simp_rw [coe_nnnorm]
-    exact (hf.integrableOn.sub (integrableOn_const.2 (Or.inr h'a))).norm
+    exact (h''a.sub (integrableOn_const.2 (Or.inr h'a))).norm
   rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal]
   · simp_rw [coe_nnnorm]
     rfl
   · apply integral_nonneg
     intro x
     exact NNReal.coe_nonneg _
-#align vitali_family.ae_tendsto_average_norm_sub VitaliFamily.ae_tendsto_average_norm_sub
 
 /-- *Lebesgue differentiation theorem*: for almost every point `x`, the
 average of `f` on `a` tends to `f x` as `a` shrinks to `x` along a Vitali family.-/
-theorem ae_tendsto_average [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : Integrable f μ) :
+theorem ae_tendsto_average [NormedSpace ℝ E] [CompleteSpace E] {f : α → E}
+    (hf : LocallyIntegrable f μ) :
     ∀ᵐ x ∂μ, Tendsto (fun a => ⨍ y in a, f y ∂μ) (v.filterAt x) (𝓝 (f x)) := by
   filter_upwards [v.ae_tendsto_average_norm_sub hf, v.ae_eventually_measure_pos] with x hx h'x
   rw [tendsto_iff_norm_tendsto_zero]
   refine' squeeze_zero' (eventually_of_forall fun a => norm_nonneg _) _ hx
-  filter_upwards [h'x, v.eventually_measure_lt_top x] with a ha h'a
+  filter_upwards [h'x, v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf]
+    with a ha h'a h''a
   nth_rw 1 [← setAverage_const ha.ne' h'a.ne (f x)]
   simp_rw [setAverage_eq']
   rw [← integral_sub]
   · exact norm_integral_le_integral_norm _
-  · exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 hf.integrableOn
+  · exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 h''a
   · exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 (integrableOn_const.2 (Or.inr h'a))
-#align vitali_family.ae_tendsto_average VitaliFamily.ae_tendsto_average
 
 end