English
A standard tendsto result: as the measure of the symmetric difference tends to 0, the corresponding indicatorConstLp converges to the limit indicatorConstLp.
Русский
При схождении мер симметичной разности к нулю индикаторные функции сходятся.
LaTeX
$$$\text{Tendsto}_{l} indicatorConstLp(p, (ht), (hμt), c) \to indicatorConstLp(p, hs, hμs, c)$ under appropriate hypotheses.$$
Lean4
/-- A family of `indicatorConstLp` functions tends to an `indicatorConstLp`,
if the underlying sets tend to the set in the sense of the measure of the symmetric difference. -/
theorem tendsto_indicatorConstLp_set [hp₁ : Fact (1 ≤ p)] {β : Type*} {l : Filter β} {t : β → Set α}
{ht : ∀ b, MeasurableSet (t b)} {hμt : ∀ b, μ (t b) ≠ ∞} (hp : p ≠ ∞) (h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)) :
Tendsto (fun b ↦ indicatorConstLp p (ht b) (hμt b) c) l (𝓝 (indicatorConstLp p hs hμs c)) :=
by
rw [tendsto_iff_dist_tendsto_zero]
have hp₀ : p ≠ 0 := (one_pos.trans_le hp₁.out).ne'
simp only [dist_indicatorConstLp_eq_norm, norm_indicatorConstLp hp₀ hp]
convert tendsto_const_nhds.mul (((ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h).rpow_const _)
· simp [ENNReal.toReal_eq_zero_iff, hp, hp₀]
· simp
