MeasureTheory.tendsto_lintegral_nn_filter_of_le_const
theorem MeasureTheory.tendsto_lintegral_nn_filter_of_le_const :
∀ {Ω : Type u_1} [inst : TopologicalSpace Ω] [inst_1 : MeasurableSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{ι : Type u_2} {L : Filter ι} [inst_3 : L.IsCountablyGenerated] (μ : MeasureTheory.Measure Ω)
[inst_4 : MeasureTheory.IsFiniteMeasure μ] {fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal},
(∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) →
∀ {f : Ω → NNReal},
(∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun i => (fs i) ω) L (nhds (f ω))) →
Filter.Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂μ))
This theorem, known as a bounded convergence theorem for a finite measure, establishes a condition under which the limit of the integrals of a sequence of functions equals the integral of the limit function. More specifically, given a topological and measurable space along with a finite measure, if we have a sequence of bounded continuous non-negative functions that are uniformly bounded by a constant and converge to a limit, then the integrals of these functions with respect to the measure also converge to the integral of the limit function. The convergence of the functions and their boundedness are assumed to hold almost everywhere, which means for all points except for a set of measure zero. Furthermore, the functions and their integrals are valued in the set of non-negative extended real numbers. The convergence of the functions is considered with respect to a countably generated filter, which intuitively means the sequence's limit is approached along some countable subset of its indices.
More concisely: Given a topological and measurable space with a finite measure, if we have a sequence of bounded, continuous, non-negative functions that converge almost everywhere to a limit function and are uniformly integrable, then their integrals converge to the integral of the limit function.
|
MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed
theorem MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed :
∀ {Ω : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω) [inst_3 : MeasureTheory.IsFiniteMeasure μ] {F : Set Ω},
IsClosed F →
∀ {δs : ℕ → ℝ} (δs_pos : ∀ (n : ℕ), 0 < δs n),
Filter.Tendsto δs Filter.atTop (nhds 0) →
Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) Filter.atTop (nhds (↑↑μ F))
This theorem, `MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed`, states that for a given measurable space `Ω` equipped with a pseudo emetric space structure and an open measurable space structure, a measure `μ` that is finite, and a closed set `F` in the space `Ω`, if we have a sequence of real numbers `δs` such that each `δs(n)` is greater than 0 and this sequence tends to 0 as `n` tends to infinity, then the limit as `n` tends to infinity of the integral with respect to measure `μ` of the thickened indicator function of set `F` is equal to the measure of the set `F`. This essentially means that the integrals of the "thickened" indicators of a closed set against a finite measure converge to the measure of the closed set when the "thickening" radii tend to zero.
More concisely: Given a measurable space with a finite measure and a closed set, the integral of the thickened indicator function's limit as the radius tends to 0 equals the set's measure.
|
HasOuterApproxClosed.measure_le_lintegral
theorem HasOuterApproxClosed.measure_le_lintegral :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F)
[inst_2 : MeasurableSpace X] [inst_3 : OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) (n : ℕ),
↑↑μ F ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ
This theorem states that for any topological space `X`, which has an outer approximation by closed sets, given a closed set `F` in 'X' and a measure `μ` on `X` that is compatible with the topology, the measure of the set `F` (denoted by `μ F`) is less than or equal to the integral of the `n`-th approximation of the characteristic function of `F` (denoted by `(hF.apprSeq n) x`) with respect to the measure `μ`. A characteristic function of a set is a function that takes the value 1 on the points of the set and 0 elsewhere. The `n`-th approximation of this function is part of a decreasing sequence of functions that approximate the characteristic function, hence the name "decreasing approximating sequence". This theorem ties together concepts from topology, measure theory and integration.
More concisely: For any topological space endowed with a compatible measure, the measure of a closed set is less than or equal to the integral of its decreasing approximating sequence of characteristic functions.
|
MeasureTheory.measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure
theorem MeasureTheory.measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : HasOuterApproxClosed Ω]
[inst_3 : OpensMeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} [inst_4 : MeasureTheory.IsFiniteMeasure μ],
(∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν) →
∀ {F : Set Ω}, IsClosed F → ↑↑μ F = ↑↑ν F
This theorem states that for any measurable and topological space `Ω` that also has properties of outer measure approximation by closed sets and open sets measurability, given two finite measures `μ` and `ν` defined on this space, if the integrals of all bounded continuous functions from `Ω` to nonnegative real numbers with respect to the two measures are equal, then the two measures assign the same measure to all closed subsets of `Ω`. In simpler terms, if two measures on a space agree on the integrals of all bounded continuous functions, they also agree on the measure of every closed set in that space.
More concisely: If two finite measures on a measurable and topological space with outer measure approximation agree on the integrals of all bounded continuous functions, they coincide on the measurement of closed sets.
|
MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator
theorem MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [inst_1 : L.IsCountablyGenerated]
[inst_2 : TopologicalSpace Ω] [inst_3 : OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
[inst_4 : MeasureTheory.IsFiniteMeasure μ] {c : NNReal} {E : Set Ω},
MeasurableSet E →
∀ (fs : ι → BoundedContinuousFunction Ω NNReal),
(∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) →
(∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun i => (fs i) ω) L (nhds (E.indicator (fun x => 1) ω))) →
Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) L (nhds (↑↑μ E))
The theorem `MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator` states that if a series of bounded continuous functions, defined on a measurable space, converges towards the indicator function of a measurable set (in an almost everywhere sense), and these functions are uniformly bounded (again, in an almost everywhere sense), then the integrals of these functions with respect to a finite measure also converge, and they converge to the measure of the set.
Here are the detailed assumptions:
1. The functions are defined on a topological space with a compatible measurable structure.
2. The functions converge to the limit along a countably generated filter.
3. The limit is in the almost everywhere sense, that is, the set of points where the limit doesn't hold is of measure zero.
4. The series of functions are uniformly bounded, i.e., there exists some non-negative real number `c` such that for all functions in the series, and for almost all points, the value of the function at that point is less than or equal to `c`.
5. The measure with respect to which the integrals are taken is finite.
The result of the theorem is that the limit of the sequence of integrals of the functions is equal to the measure of the set, with respect to the given finite measure.
More concisely: If a sequence of uniformly bounded, continuous functions on a measurable space, converging almost everywhere to the indicator function of a measurable set with respect to a finite measure, then the integrals of the sequence converge to the measure of the set.
|
MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure
theorem MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : HasOuterApproxClosed Ω]
[inst_3 : BorelSpace Ω] {μ ν : MeasureTheory.Measure Ω} [inst_4 : MeasureTheory.IsFiniteMeasure μ],
(∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν) → μ = ν
This theorem states that, for any type Ω, given that Ω is a measurable space, a topological space, has an outer measure approximating its closed subsets, and is a Borel space, and given two finite Borel measures μ and ν on this space Ω, if the integrals of all bounded continuous functions from Ω to the nonnegative real numbers with respect to both μ and ν are equal, then measures μ and ν themselves must also be equal. In other words, two finite Borel measures on a given space are equal if they give the same result when applied to every bounded continuous function on that space.
More concisely: If two finite Borel measures on a measurable, topological space with an outer measure approximating its closed subsets, and having equal integrals for all bounded continuous functions, are equal on the space.
|
HasOuterApproxClosed.tendsto_lintegral_apprSeq
theorem HasOuterApproxClosed.tendsto_lintegral_apprSeq :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F)
[inst_2 : MeasurableSpace X] [inst_3 : OpensMeasurableSpace X] (μ : MeasureTheory.Measure X)
[inst_4 : MeasureTheory.IsFiniteMeasure μ],
Filter.Tendsto (fun n => ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ) Filter.atTop (nhds (↑↑μ F))
This theorem states that for any topological space `X` with an outer approximation to a closed set, and any closed subset `F` of `X`, if `X` also has a measurable space structure and an open measurable space structure, along with a measure `μ` (that is a finite measure), the sequence of integrals over `X` of the decreasing approximating sequence to the characteristic function (or indicator function) of the closed set `F` tends to the measure of the closed set `F`. This happens as the index of the sequence goes to infinity. More specifically, the sequence of functions `(hF.apprSeq n) x` is an approximation to the characteristic function of the closed set `F`, and `∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ` represents the integral of this sequence. The theorem asserts that the limit of these integrals as the index `n` goes to infinity is the measure of the set `F` under the measure `μ`, denoted by `↑↑μ F`.
More concisely: For any topological space `X` with a measurable structure and a finite measure `μ`, the integral of the sequence of approximating characteristic functions of a closed set `F` converges to the measure of `F` as the index goes to infinity.
|
MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator
theorem MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator :
∀ {Ω : Type u_1} [inst : TopologicalSpace Ω] [inst_1 : MeasurableSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω) [inst_3 : MeasureTheory.IsFiniteMeasure μ] {c : NNReal} {E : Set Ω},
MeasurableSet E →
∀ (fs : ℕ → BoundedContinuousFunction Ω NNReal),
(∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) →
Filter.Tendsto (fun n ω => (fs n) ω) Filter.atTop (nhds (E.indicator fun x => 1)) →
Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) Filter.atTop (nhds (↑↑μ E))
The theorem `MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator` states that given a topological space `Ω` which is also a measurable space (with open sets being measurable), a finite measure `μ` on `Ω`, a nonnegative real number `c`, and a measurable set `E` in `Ω`, if a sequence of bounded continuous functions `fs` from `Ω` to nonnegative real numbers is such that each function in the sequence is bounded by `c` and the sequence converges pointwise to the indicator function of the set `E`, then the sequence of Lebesgue integrals of the functions in `fs` with respect to the measure `μ` converges to the measure of the set `E` under `μ`.
This theorem is saying that under these circumstances, the limit of the sequence of integrals of the bounded continuous functions is the measure of the set whose indicator function the sequence converges to. This is a result in measure theory that connects the behavior of a sequence of functions and their integrals to the measure of a set.
More concisely: If `Ω` is a measurable space with finite measure `μ`, a sequence `fs` of bounded continuous functions converging pointwise to the indicator function of measurable set `E` satisfies ∫ᵢμ(x).fₗ(x)dμ(x) → μ(E) as i → ∞.
|