English
A specialized distance inequality for convolution with a finite measure and a bounded f supported in a ball.
Русский
Специальное неравенство расстояния для свертки с конечной мерой и ограниченной функцией с опорой внутри шара.
LaTeX
$$dist((f ⋆[lsmul ℝ ℝ, μ] g : G → E') x0) z0 ≤ ε$$
Lean4
/-- `(φ i ⋆ g i) (k i)` tends to `z₀` as `i` tends to some filter `l` if
* `φ` is a sequence of nonnegative functions with integral `1` as `i` tends to `l`;
* The support of `φ` tends to small neighborhoods around `(0 : G)` as `i` tends to `l`;
* `g i` is `mu`-a.e. strongly measurable as `i` tends to `l`;
* `g i x` tends to `z₀` as `(i, x)` tends to `l ×ˢ 𝓝 x₀`;
* `k i` tends to `x₀`.
See also `ContDiffBump.convolution_tendsto_right`.
-/
theorem convolution_tendsto_right {ι} {g : ι → G → E'} {l : Filter ι} {x₀ : G} {z₀ : E'} {φ : ι → G → ℝ} {k : ι → G}
(hnφ : ∀ᶠ i in l, ∀ x, 0 ≤ φ i x)
(hiφ : ∀ᶠ i in l, ∫ x, φ i x ∂μ = 1)
-- todo: we could weaken this to "the integral tends to 1"
(hφ : Tendsto (fun n => support (φ n)) l (𝓝 0).smallSets) (hmg : ∀ᶠ i in l, AEStronglyMeasurable (g i) μ)
(hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)) (hk : Tendsto k l (𝓝 x₀)) :
Tendsto (fun i : ι => (φ i ⋆[lsmul ℝ ℝ, μ] g i : G → E') (k i)) l (𝓝 z₀) :=
by
simp_rw [tendsto_smallSets_iff] at hφ
rw [Metric.tendsto_nhds] at hcg ⊢
simp_rw [Metric.eventually_prod_nhds_iff] at hcg
intro ε hε
have h2ε : 0 < ε / 3 := div_pos hε (by simp)
obtain ⟨p, hp, δ, hδ, hgδ⟩ := hcg _ h2ε
dsimp only [uncurry] at hgδ
have h2k := hk.eventually (ball_mem_nhds x₀ <| half_pos hδ)
have h2φ := hφ (ball (0 : G) _) <| ball_mem_nhds _ (half_pos hδ)
filter_upwards [hp, h2k, h2φ, hnφ, hiφ, hmg] with i hpi hki hφi hnφi hiφi hmgi
have hgi : dist (g i (k i)) z₀ < ε / 3 := hgδ hpi (hki.trans <| half_lt_self hδ)
have h1 : ∀ x' ∈ ball (k i) (δ / 2), dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3 :=
by
intro x' hx'
refine (dist_triangle_right _ _ _).trans (add_le_add (hgδ hpi ?_).le hgi.le)
exact ((dist_triangle _ _ _).trans_lt (add_lt_add hx'.out hki)).trans_eq (add_halves δ)
have := dist_convolution_le (add_pos h2ε h2ε).le hφi hnφi hiφi hmgi h1
refine ((dist_triangle _ _ _).trans_lt (add_lt_add_of_le_of_lt this hgi)).trans_eq ?_
field_simp; ring_nf
