MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure
theorem MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure :
∀ {α : Type u_1} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι)
[inst_1 : L.IsCountablyGenerated] {As : ι → Set α} [inst_2 : L.NeBot] (μ : MeasureTheory.Measure α)
[inst_3 : MeasureTheory.IsFiniteMeasure μ],
(∀ (i : ι), MeasurableSet (As i)) →
(∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) → Filter.Tendsto (fun i => ↑↑μ (As i)) L (nhds (↑↑μ A))
The theorem `MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure` states that for a given finite measure `μ` and a sequence of measurable sets `Aᵢ` indexed by `ι`, if the indicators of the `Aᵢ`s converge pointwise to the indicator of a set `A`, then the measures `μ Aᵢ` converge to the measure `μ A` in the filter `L`. This convergence is in the sense of the neighborhood filter at `μ A`, denoted `nhds (μ A)`. It is also required that the filter `L` be countably generated and not "bottom" (i.e., not the empty set), and that each set `Aᵢ` is measurable. The condition `(∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A)` expresses that, eventually for each `x` in the filter `L`, `x` belongs to `Aᵢ` if and only if `x` belongs to `A`.
More concisely: Given a finite measure `μ`, a countably generated non-empty filter `L` of subsets of a measurable space, a sequence of measurable sets `Aᵢ` converging pointwise to a measurable set `A`, if for all `x`, `μ`-almost all `i` in `L`, `x` is in `Aᵢ` if and only if `x` is in `A`, then `μ Aᵢ` converges to `μ A` in the `μ`-neighborhood filter `nhds (μ A)`.
|
MeasureTheory.tendsto_measure_of_tendsto_indicator
theorem MeasureTheory.tendsto_measure_of_tendsto_indicator :
∀ {α : Type u_1} [inst : MeasurableSpace α] {A : Set α} {ι : Type u_2} (L : Filter ι)
[inst_1 : L.IsCountablyGenerated] {As : ι → Set α} [inst_2 : L.NeBot] {μ : MeasureTheory.Measure α},
(∀ (i : ι), MeasurableSet (As i)) →
∀ {B : Set α},
MeasurableSet B →
↑↑μ B ≠ ⊤ →
(∀ᶠ (i : ι) in L, As i ⊆ B) →
(∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) →
Filter.Tendsto (fun i => ↑↑μ (As i)) L (nhds (↑↑μ A))
This theorem, `MeasureTheory.tendsto_measure_of_tendsto_indicator`, states that if we have a sequence of measurable sets `Aᵢ` indexed by `ι` and a measurable set `A`, alongside a filter `L` on the index set, under certain conditions the measure of `Aᵢ` tends to the measure of `A`.
The conditions are as follows:
1) The filter `L` is countably generated and not the bottom filter.
2) There exists a measurable set `B` with finite measure such that every set `Aᵢ` is eventually a subset of `B` as per the filter `L`.
3) The indicator functions (which are equal to one on the set and zero outside) of `Aᵢ` converge pointwise to the indicator function of `A` for every point in the space, again eventually according to the filter `L`.
In other words, if you have a sequence of measurable sets that becomes increasingly similar to another set in terms of the points it contains, and these sets are all contained within some finitely measurable set, then the measures of the sets in the sequence will approach the measure of the set they are becoming similar to.
More concisely: If `Aᵢ` is a sequence of measurable sets indexed by `ι`, `L` is a countably generated, non-bottom filter on `ι`, `B` is a measurable set of finite measure, and `Aᵢ` is eventually contained in `B` and has indicator functions converging pointwise to the indicator function of `A` according to `L`, then the measures of `Aᵢ` tend to the measure of `A`.
|