English
Under general non-atomic and measurability hypotheses, the convolution (φ i.normed μ) ⋆ g_i tends to g_i pointwise along k_i → x0, uniformly in a limit sense.
Русский
При общих гипотезах с мерами и измеримостью конволюция стремится к соответствующим значениям.
LaTeX
$$$\\text{tendsto right: }\\ (φ_i.normed μ ⋆ g_i)(k_i) \\to g(x_0) \\text{ as } i\\to l$$$
Lean4
/-- `(φ i ⋆ g i) (k i)` tends to `z₀` as `i` tends to some filter `l` if
* `φ` is a sequence of normed bump functions
such that `(φ i).rOut` tends to `0` as `i` tends to `l`;
* `g i` is `μ`-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₀`. -/
nonrec theorem convolution_tendsto_right {ι} {φ : ι → ContDiffBump (0 : G)} {g : ι → G → E'} {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 => ((φ 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
