Results about indicator functions, their integrals, and measures

This file has a few measure theoretic or integration-related results on indicator functions.

Implementation notes

This file exists to avoid importing Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable in Mathlib.MeasureTheory.Integral.Lebesgue.

Todo

The result MeasureTheory.tendsto_measure_of_tendsto_indicator here could be proved without integration, if we had convergence of measures results for countably generated filters. Ideally, the present file would then become unnecessary: lemmas such as MeasureTheory.tendsto_measure_of_ae_tendsto_indicator would not need integration so could be moved out of Mathlib.MeasureTheory.Integral.Lebesgue, and the lemmas in this file could be moved to, e.g., Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable.

theorem MeasureTheory.tendsto_measure_of_tendsto_indicator {α : Type u_1} [MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι) [Filter.IsCountablyGenerated L] {As : ι → Set α} [Filter.NeBot L] {μ : MeasureTheory.Measure α} (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) : Filter.Tendsto (fun (i : ι) => ↑↑μ (As i)) L (nhds (↑↑μ A))

If the indicators of measurable sets Aᵢ tend pointwise to the indicator of a 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 MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure {α : Type u_1} [MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι) [Filter.IsCountablyGenerated L] {As : ι → Set α} [Filter.NeBot L] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (As_mble : ∀ (i : ι), MeasurableSet (As i)) (h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) : Filter.Tendsto (fun (i : ι) => ↑↑μ (As i)) L (nhds (↑↑μ A))

If μ is a finite measure and the indicators of measurable sets Aᵢ tend pointwise to the indicator of a set A, then the measures μ Aᵢ tend to the measure μ A.