English
If the indicators of measurable sets A_i converge almost everywhere to the indicator of A, and A_i ⊆ B eventually for some finite-measure B, then μ(A_i) tends to μ(A).
Русский
Если индикаторы подмножеств A_i сходятся почти повсюду к индикатору A, и A_i ⊆ B для некоторых множества B с конечной мерой, то меры μ(A_i) сходятся к μ(A).
LaTeX
$$$ \mathrm{Tendsto}\ i \mapsto \mu(A_i) \; L \; (\mathcal{N})\ \to\mu(A) \quad\text{under appropriate hypotheses on }A_i, A, B$$$
Lean4
/-- If the indicators of measurable sets `Aᵢ` tend pointwise almost everywhere to the indicator
of a measurable set `A` and we eventually have `Aᵢ ⊆ B` for some set `B` of finite measure, then
the measures of `Aᵢ` tend to the measure of `A`. -/
theorem tendsto_measure_of_ae_tendsto_indicator {μ : Measure α} (A_mble : MeasurableSet A)
(As_mble : ∀ i, MeasurableSet (As i)) {B : Set α} (B_mble : MeasurableSet B) (B_finmeas : μ B ≠ ∞)
(As_le_B : ∀ᶠ i in L, As i ⊆ B) (h_lim : ∀ᵐ x ∂μ, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) :
Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A)) :=
by
simp_rw [← MeasureTheory.lintegral_indicator_one A_mble, ← MeasureTheory.lintegral_indicator_one (As_mble _)]
refine
tendsto_lintegral_filter_of_dominated_convergence (B.indicator (1 : α → ℝ≥0∞)) (Eventually.of_forall ?_) ?_ ?_ ?_
· exact fun i ↦ Measurable.indicator measurable_const (As_mble i)
· filter_upwards [As_le_B] with i hi
exact Eventually.of_forall (fun x ↦ indicator_le_indicator_of_subset hi (by simp) x)
· rwa [← lintegral_indicator_one B_mble] at B_finmeas
· simpa only [Pi.one_def, tendsto_indicator_const_apply_iff_eventually] using h_lim
