English
If a sequence of bounded continuous nonnegative functions converges to the indicator of a measurable set and is uniformly bounded, then their integrals against a finite measure converge to the measure of the set.
Русский
Если последовательность ограниченных непрерывных неотрицательных функций сходится по мере к индиикатору измеримого множества и ограничена сверху, то интегралы по мере сходятся к мере множества.
LaTeX
$$$\\forall \\mu \\text{ finite}, \\forall E \\text{ measurable}, \\\\text{if } f_n \\to 1_E \\text{ a.e. and } |f_n| \\le c, \\\\Rightarrow \\int f_n d\\mu \\to \\mu(E)$$
Lean4
/-- If bounded continuous functions tend to the indicator of a measurable set and are
uniformly bounded, then their integrals against a finite measure tend to the measure of the set.
This formulation assumes:
* the functions tend to a limit along a countably generated filter;
* the limit is in the almost everywhere sense;
* boundedness holds almost everywhere.
-/
theorem measure_of_cont_bdd_of_tendsto_filter_indicator {ι : Type*} {L : Filter ι} [L.IsCountablyGenerated]
(μ : Measure Ω) [IsFiniteMeasure μ] {c : ℝ≥0} {E : Set Ω} (E_mble : MeasurableSet E) (fs : ι → Ω →ᵇ ℝ≥0)
(fs_bdd : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂μ, fs i ω ≤ c)
(fs_lim : ∀ᵐ ω ∂μ, Tendsto (fun i ↦ fs i ω) L (𝓝 (indicator E (fun _ ↦ (1 : ℝ≥0)) ω))) :
Tendsto (fun n ↦ lintegral μ fun ω ↦ fs n ω) L (𝓝 (μ E)) :=
by
convert tendsto_lintegral_nn_filter_of_le_const μ fs_bdd fs_lim
have aux : ∀ ω, indicator E (fun _ ↦ (1 : ℝ≥0∞)) ω = ↑(indicator E (fun _ ↦ (1 : ℝ≥0)) ω) := fun ω ↦ by
simp only [ENNReal.coe_indicator, ENNReal.coe_one]
simp_rw [← aux, lintegral_indicator E_mble]
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
