English
If g is Locally Integrable w.r.t. μ, then for almost every x0, the convolution ((φ i).normed μ) ⋆ g tends to g(x0) as i → l under rOut → 0 with bounded radius ratio.
Русский
Если g локально интегрируема по μ, то почти везде конволюция стремится к g(x0) при i→l.
LaTeX
$$$\\forall^{\\text{ae}} x_0 ∂μ , Tendsto (λ i, (φ_i.normed μ ⋆ g)(x_0)) l (nhds (g(x_0)))$$$
Lean4
/-- 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_locallyIntegrable {ι} {φ : ι → 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
-- 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 at this
apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this
· filter_upwards with i using hg.integrableOn_isCompact (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]
· filter_upwards with 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_real_closedBall_center]
exact (φ i).normed_le_div_measure_closedBall_rOut _ _ hi _
