MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto
theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure Ω}
{μ : MeasureTheory.ProbabilityMeasure Ω},
Filter.Tendsto μs F (nhds μ) ↔
∀ (f : BoundedContinuousFunction Ω NNReal),
Filter.Tendsto (fun i => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs i)) F (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
This theorem provides a characterization of the weak convergence of probability measures characterized by the condition that the integrals of every continuous bounded nonnegative function converge to the integral of the function against the limit measure. Specifically, for any measure space `Ω` that possesses a topological structure and a measurable open structure, a filter `F`, a sequence of probability measures `μs` indexed by `γ`, and a probability measure `μ`, it states that the sequence `μs` tends to `μ` with respect to the filter `F` if and only if for all bounded continuous functions `f` from `Ω` to the nonnegative real numbers, the sequence of integrals of `f` with respect to `μs` tends to the integral of `f` with respect to `μ`, again with respect to the filter `F`.
More concisely: A sequence of probability measures `μs` on a measurable space `(Ω, Σ)` converges weakly to a probability measure `μ` with respect to a filter `F` if and only if for all bounded continuous functions `f` from `Ω` to the real numbers, the sequence of integrals `∫(f dμs)` converges to `∫(f dμ)` with respect to `F`.
|
Mathlib.MeasureTheory.Measure.ProbabilityMeasure._auxLemma.2
theorem Mathlib.MeasureTheory.Measure.ProbabilityMeasure._auxLemma.2 : (¬False) = True
This theorem, in the Mathlib's Measure Theory module, asserts a basic logical proposition that the negation of 'False' is 'True'. In other words, it states that if 'False' does not occur (is negated), then the result is 'True'. This is a fundamental principle in classical logic and boolean algebra.
More concisely: The theorem asserts that the negation of False is True. In mathematical notation, ¬False = True.
|
MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure
theorem MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω), μ.toFiniteMeasure.mass = 1
This theorem states that for any given measurable space 'Ω' and a probability measure 'μ' on that space, the total mass of the finite measure, obtained by interpreting the probability measure as a finite measure, is equal to 1. In other words, it ensures that when a probability measure is converted to a finite measure, its total mass (or the measure of the entire space) remains 1, preserving the key property of a probability measure.
More concisely: For any measurable space 'Ω' and probability measure 'μ' on it, the total mass of the induced finite measure equals 1.
|
MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn
theorem MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω),
(fun s => (↑↑↑ν.toFiniteMeasure s).toNNReal) = fun s => (↑↑↑ν s).toNNReal
This theorem states that, for any given probability measure "ν" on a measure space "Ω", the measure of any set "s" under the composition of the function that converts "ν" into a finite measure and the function that converts the measure value into a non-negative real number, is equal to the measure of "s" under the original probability measure "ν" converted into a non-negative real number. In other words, converting a probability measure into a finite measure does not change its measure values when those values are represented as non-negative real numbers.
More concisely: For any probability measure ν and set s in a measurable space, the conversion of ν to a finite measure and then to a non-negative real number equals the conversion of ν directly to a non-negative real number for the measure of s.
|
MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass
theorem MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass :
∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
[inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
{μs : γ → MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize) →
Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass) → Filter.Tendsto μs F (nhds μ)
The theorem, `MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass`, states that if we have a sequence of finite measures (`μs`) which are indexed by a type (`γ`), and if the normalized versions of these finite measures converge to the normalized version of a finite measure (`μ`) in terms of a filter (`F`), and if the total masses of these finite measures also converge to the total mass of `μ` in terms of the same filter, then the sequence of finite measures itself converges to `μ` in terms of the filter. Here, the notion of convergence used is the weak form, which means that as we progress along the sequence, the measures become arbitrarily close to `μ`. Furthermore, the space on which the measures are defined (`Ω`) is assumed to be nonempty, measurable, and endowed with a topological structure which allows it to handle open sets measurably.
More concisely: If a sequence of finite measures on a nonempty, measurable and topologizable space converges weakly to a finite measure and their total masses also converge to the total mass of the limit measure, then the sequence of measures themselves converge to the limit measure in the weak topology.
|
MeasureTheory.FiniteMeasure.average_eq_integral_normalize
theorem MeasureTheory.FiniteMeasure.average_eq_integral_normalize :
∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) {E : Type u_2}
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E],
μ ≠ 0 → ∀ (f : Ω → E), MeasureTheory.average (↑μ) f = ∫ (ω : Ω), f ω ∂↑μ.normalize
The theorem `MeasureTheory.FiniteMeasure.average_eq_integral_normalize` states that for any nonempty measurable space `Ω`, given a finite measure `μ` over this space and assuming that `μ` is not zero, the process of averaging with respect to this finite measure is equivalent to integrating against the normalized version of this measure. This holds true for any function `f` that maps `Ω` to `E`, where `E` is a normed add-commutative group that also forms a normed space over the real numbers.
More concisely: For any nonempty measurable space Ω with finite, non-zero measure μ, and any function f from Ω to a normed add-commutative group E over the real numbers, the average of f is equal to the integral of its normalized version with respect to μ.
|
MeasureTheory.ProbabilityMeasure.continuous_map
theorem MeasureTheory.ProbabilityMeasure.continuous_map :
∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
[inst_2 : TopologicalSpace Ω] [inst_3 : OpensMeasurableSpace Ω] [inst_4 : TopologicalSpace Ω']
[inst_5 : BorelSpace Ω'] {f : Ω → Ω'} (f_cont : Continuous f), Continuous fun ν => ν.map ⋯
The theorem `MeasureTheory.ProbabilityMeasure.continuous_map` states that if you have a continuous function `f` from one measurable space `Ω` to another measurable space `Ω'`, where `Ω'` is equipped with the Borel sigma algebra, then the push-forward of probability measures, that is, the mapping of any probability measure `ν` on `Ω` to the probability measure `f*ν` on `Ω'`, is also a continuous function. This continuity is defined with respect to the topologies of convergence in distribution.
More concisely: Given a continuous function `f` from a measurable space `(Ω, Σ)` to another measurable space `(Ω', Σ')` with `Ω'` being the Borel sets, the push-forward `f*ν` of any probability measure `ν` on `(Ω, Σ)` is a continuous function with respect to the topologies of convergence in distribution.
|
MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure
theorem MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω),
↑((fun s => (↑↑↑ν s).toNNReal) s) = ↑↑↑ν s
This theorem is stating that for any type `Ω` that is equipped with a `MeasurableSpace` structure, any probability measure `ν` on `Ω`, and any set `s` of `Ω`, the real number part of the measure `ν` of the set `s` (obtained by applying three coercions to `ν s` and then taking the nonnegative real part) is equal to the measure `ν` of the set `s` itself. This is equivalent to saying that the measure of any set in a probability space, when considered as a nonnegative real number, is the same as the original measure value.
More concisely: For any probability measure `ν` on a measurable space `(Ω, Σ)`, the real number `ℝ⁺(ν(s))` equal to the measure `ν` of any set `s ∈ Σ`.
|
MeasureTheory.ProbabilityMeasure.map_apply'
theorem MeasureTheory.ProbabilityMeasure.map_apply' :
∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
(ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'},
MeasurableSet A → ↑↑↑(ν.map f_aemble) A = ↑↑↑ν (f ⁻¹' A)
This theorem states that, for any measure spaces `Ω` and `Ω'` and any probability measure `ν` on `Ω`, if a function `f` from `Ω` to `Ω'` is almost everywhere measurable with respect to `ν`, and `A` is a measurable set in `Ω'`, then the measure of `A` under the measure induced by `f` and `ν` will be equal to the measure of the preimage of `A` under `f` with respect to `ν`. This equality is in terms of non-negative extended real numbers (`ℝ≥0∞`). Note that there is also a version of this theorem, `MeasureTheory.ProbabilityMeasure.map_apply`, which expresses the same result in terms of non-negative real numbers (`ℝ≥0`).
More concisely: For any measurable function `f` from a measure space `(Ω, Σ, ν)` to a measurable space `(Ω', Σ', μ)`, and any measurable set `A ∈ Σ'`, the induced measure `μ(f⁁ⁱ(E)) = ν(E)` for every `E ∈ Σ` such that `μ` almost equals `ν` on `f(E)`.
|
MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto
theorem MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto :
∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
[inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
{μs : γ → MeasureTheory.FiniteMeasure Ω},
μ ≠ 0 →
(Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize) ∧
Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass) ↔
Filter.Tendsto μs F (nhds μ))
This theorem states that for any set `Ω`, given a measurable space `m0` over it, a finite measure `μ` on it, a topological space over `Ω`, an open measurable space, another type `γ`, and a filter `F` over `γ`, along with a sequence of finite measures `μs` indexed by `γ`, if the finite measure `μ` is not zero, then the sequences of normalized measures and total masses converging to the normalized measure and total mass of `μ` respectively is equivalent to the sequence of finite measures converging to `μ`. In other words, the weak convergence of finite measures to a nonzero limit can be characterized by the weak convergence of both their normalized versions (probability measures) and their total masses.
More concisely: For a nonzero finite measure `μ` on a measurable space `(Ω, m0)` and an open measurable space over `Ω`, if a sequence of finite measures `μs` on `γ` with filters `F` weakly converges to `μ`, then both the normalized measures and their total masses converge to those of `μ`.
|
MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds
theorem MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{δ : Type u_2} (F : Filter δ) {μs : δ → MeasureTheory.ProbabilityMeasure Ω}
{μ₀ : MeasureTheory.ProbabilityMeasure Ω},
Filter.Tendsto μs F (nhds μ₀) ↔
Filter.Tendsto (MeasureTheory.ProbabilityMeasure.toFiniteMeasure ∘ μs) F (nhds μ₀.toFiniteMeasure)
The theorem states that for any measurable and topological space Ω with the property that any open set in Ω is measurable, any filter F over a type δ, and any sequence of probability measures μs over Ω, the sequence μs tends to a certain probability measure μ₀ under the filter F if and only if the sequence of finite measures associated to μs (obtained by interpreting each probability measure in the sequence as a finite measure) also tends to the finite measure associated to μ₀ under the same filter F. In other words, the convergence of a sequence of probability measures in the neighborhood filter is equivalent to the convergence of the corresponding sequence of finite measures in the same filter.
More concisely: For any measurable and topological space Ω with the property that any open set is measurable, the convergence of a sequence of probability measures on Ω under the neighborhood filter is equivalent to the convergence of the corresponding sequence of finite measures.
|
MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto
theorem MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto :
∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
[inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
{μs : γ → MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto μs F (nhds μ) → μ ≠ 0 → Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize)
This theorem states that if a sequence of finite measures converges to a nonzero limit measure in the weak topology, then the sequence of their normalized versions also converges weakly to the normalized version of the limit measure. Here, a finite measure is a measure that has a finite total mass, and the normalization of a finite measure is obtained by multiplying it by the reciprocal of its total mass. The weak convergence of a sequence of measures is defined in terms of the convergence of the integration of functions against these measures, with respect to a given filter. The filter represents the index set of the sequence, and the theorem asserts that if the original sequence of measures converges weakly, then so does the sequence of their normalized versions.
More concisely: If a sequence of finite measures converges weakly to a nonzero limit measure, then their normalized versions also converge weakly to the normalized limit measure.
|
MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous
theorem MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous :
∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
[inst_2 : TopologicalSpace Ω] [inst_3 : OpensMeasurableSpace Ω] [inst_4 : TopologicalSpace Ω']
[inst_5 : BorelSpace Ω'] {ι : Type u_3} {L : Filter ι} (νs : ι → MeasureTheory.ProbabilityMeasure Ω)
(ν : MeasureTheory.ProbabilityMeasure Ω),
Filter.Tendsto νs L (nhds ν) →
∀ {f : Ω → Ω'} (f_cont : Continuous f), Filter.Tendsto (fun i => (νs i).map ⋯) L (nhds (ν.map ⋯))
This theorem states that if we have a function `f` from `X` to `Y` that is continuous, and if `Y` is equipped with the Borel sigma algebra, then if a sequence of probability measures on `X` converges (in distribution), the sequence of their push-forwards by `f` also converges (in distribution). In other words, if we have a sequence of probability measures on `X` that converges, then applying `f` to each measure in the sequence and taking the push-forward will result in a new sequence of measures that also converges. This holds true for any topological space `X` and `Y` where `Y` is a BorelSpace.
More concisely: If `f: X → Y` is a continuous function between topological spaces `X` and `BorelSpace Y`, and `μ_n` is a sequence of probability measures on `X` that converges in distribution, then the sequence of push-forwards `f_# μ_n` also converges in distribution to some probability measure on `Y`.
|
MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.ProbabilityMeasure Ω}
{μ : MeasureTheory.ProbabilityMeasure Ω},
Filter.Tendsto μs F (nhds μ) ↔
∀ (f : BoundedContinuousFunction Ω ℝ),
Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))
This theorem characterizes the weak convergence of probability measures. Specifically, it states that for any measurable and topological space Ω, any type γ, any filter F on γ, and any sequence of probability measures μs indexed by γ, the sequence μs converges weakly to a probability measure μ (i.e., `Filter.Tendsto μs F (nhds μ)`) if and only if for any bounded continuous function f from Ω to the real numbers ℝ, the sequence of integrals of f with respect to the measures μs converges to the integral of f with respect to the measure μ in the filter F (i.e., `Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))`). In layman's terms, this theorem is stating that a sequence of probability measures converges if integrals of functions with respect to these measures also converge.
More concisely: A sequence of probability measures on a measurable and topological space converges weakly if and only if the integrals of bounded continuous functions with respect to the measures converge in the filter of neighborhoods of the limit measure.
|