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.lean in Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean.

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/Basic.lean, and the lemmas in this file could be moved to, e.g., Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean.

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

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 MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure {α : Type u_1} [MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι) [L.IsCountablyGenerated] {As : ι → Set α} {μ : Measure α} [IsFiniteMeasure μ] (A_mble : MeasurableSet A) (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 almost everywhere to the indicator of a measurable set A, then the measures μ Aᵢ tend to the measure μ A.

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