MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const
theorem MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
(μ : MeasureTheory.FiniteMeasure Ω) {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal},
(∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) →
∀ {f : Ω → NNReal},
(∀ (ω : Ω), Filter.Tendsto (fun n => (fs n) ω) Filter.atTop (nhds (f ω))) →
Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ))
This theorem, known as a bounded convergence theorem for a finite measure, asserts the following: given a measurable space equipped with a finite measure and a topology, if we have a sequence of bounded continuous non-negative functions that are uniformly bounded by a constant, and these functions converge pointwise to a limit, then the integral of each function in this sequence (computed with respect to the finite measure) also converges to the integral of the limit function. This is a specific case of a more general result concerning the convergence of integrals under certain boundedness conditions.
More concisely: Given a measurable space with a finite measure and a topology, if if a sequence of bounded, continuous, non-negative functions converges uniformly to a limit function, then the integrals of the sequence converge to the integral of the limit function.
|
MeasureTheory.FiniteMeasure.ennreal_mass
theorem MeasureTheory.FiniteMeasure.ennreal_mass :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω}, ↑μ.mass = ↑↑↑μ Set.univ
The theorem `MeasureTheory.FiniteMeasure.ennreal_mass` states that for any measurable space `Ω` and any finite measure `μ` on this space, the total mass of `μ`, when converted to the extended nonnegative real number type (`ennreal`), is equal to the measure of the universal set under `μ`. In other words, the total mass of a finite measure is just the measure of the whole space.
More concisely: For any measurable space Ω and finite measure μ, the total mass of μ, when considered as an extended nonnegative real number, equals the measure of Ω under μ.
|
MeasureTheory.FiniteMeasure.mass_zero_iff
theorem MeasureTheory.FiniteMeasure.mass_zero_iff :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω), μ.mass = 0 ↔ μ = 0
This theorem states that for any type `Ω` with a measurable space structure and for any finite measure `μ` on `Ω`, the total mass of `μ` is zero if and only if `μ` is the zero measure. In mathematical terms, the total mass of a measure is the measure of the entire space, written as `μ(univ)`. So, this theorem is expressing the idea that a finite measure is the zero measure if and only if the measure of the entire space is zero.
More concisely: A finite measure `μ` on a measurable space `(Ω, Σ)` is the zero measure if and only if `μ(Ω) = 0`.
|
Filter.Tendsto.mass
theorem Filter.Tendsto.mass :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto μs F (nhds μ) → Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass)
This theorem states that if a sequence of finite measures on a measurable and topological space converges to a finite measure with respect to the neighborhood filter, then the sequence of their total masses also converges to the total mass of the limit measure in the neighborhood filter. In other words, if finite measures converge, their corresponding total masses will also converge. This is applicable to any type of measures, as long as they satisfy the property of being a finite measure.
More concisely: If a sequence of finite measures on a measurable and topological space converges with respect to the neighborhood filter, then their total masses converge to the total mass of the limit measure.
|
MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass
theorem MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto (fun i => (μs i).mass) F (nhds 0) → Filter.Tendsto μs F (nhds 0)
This theorem states that if the total masses (or total measures) of finite measures tend to zero, then the measures themselves also tend to zero. More formally, for any measurable and topological space Ω, equipped with a topology that makes all open sets measurable, given a filter F on some type γ and a sequence of finite measures μs indexed by γ, if the total masses (defined by the function `(μs i).mass`) tend to zero as per the filter F (i.e., for every neighborhood of zero, there's some point in the filter after which all total masses are within that neighborhood), then the finite measures μs themselves also tend to zero under the same filter F.
More concisely: If a filter converges to 0 in the total mass of a sequence of finite measures on a measurable and topological space, then the measures themselves converge to the zero measure under the same filter.
|
MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure
theorem MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.FiniteMeasure Ω) (s : Set Ω),
↑((fun s => (↑↑↑ν s).toNNReal) s) = ↑↑↑ν s
This theorem states that for any measurable space `Ω` and any finite measure `ν` on this space, the measure of any set `s` in `Ω` under `ν`, when converted to a non-negative real number and then lifted back into the extended non-negative real number type, is equivalent to the direct measure of the set `s` under `ν`. In other words, the process of measuring a set, converting this measure to a non-negative real number and then lifting back does not alter the measure value in the context of finite measures.
More concisely: For any measurable space `(Ω, Σ)` and finite measure `ν:` ∀s ∈ Σ, ν(s) = ‛‛ν(s)‛‛ where `ν(s)` is the measure of `s` under `ν` as a real number and `ν(s)` as a non-negative real number under `ν`.
|
MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN
theorem MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : HasOuterApproxClosed Ω]
[inst_3 : BorelSpace Ω], Function.Injective MeasureTheory.FiniteMeasure.toWeakDualBCNN
The theorem `MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN` states that the mapping `toWeakDualBCNN`, which transforms finite Borel measures to elements of the weak dual of the space of bounded, continuous, non-negative real functions (denoted as `Ω →ᵇ ℝ≥0`) on a measurable and topological space `Ω`, is injective. This means that two different finite Borel measures will be mapped to two different elements in the weak dual. This applies specifically when indicator functions of closed sets in `Ω` can be approximated by sequences of continuous functions that are decreasing. In particular, this condition is met when `Ω` is pseudometrizable. This theorem guarantees that we can invert the mapping under these conditions, allowing us to recover the original finite Borel measures from their image in the weak dual.
More concisely: The mapping from finite Borel measures to their weak dual representatives is injective under the condition that indicator functions of closed sets can be approximated by sequences of decreasing continuous functions on pseudometrizable spaces.
|
MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply
theorem MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (f : BoundedContinuousFunction Ω NNReal),
MeasureTheory.FiniteMeasure.testAgainstNN 0 f = 0
The theorem `MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply` states that for any measurable space `Ω` that also has a topological structure and any bounded continuous function `f` from `Ω` to nonnegative real numbers, if we pair the zero measure (a finite measure) with the function `f`, the result will always be zero. This is equivalent to saying that the Lebesgue integral of the function `f` with respect to the zero measure is zero.
More concisely: For any measurable space with a topology and a bounded continuous function, the Lebesgue integral of the function with respect to the zero measure is zero.
|
MeasureTheory.FiniteMeasure.map_apply'
theorem MeasureTheory.FiniteMeasure.map_apply' :
∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
(ν : MeasureTheory.FiniteMeasure Ω) {f : Ω → Ω'},
AEMeasurable f ↑ν → ∀ {A : Set Ω'}, MeasurableSet A → ↑↑↑(ν.map f) A = ↑↑↑ν (f ⁻¹' A)
This theorem states that, for any two types `Ω` and `Ω'` with respective measurable spaces, any finite measure `ν` on `Ω`, and any function `f` from `Ω` to `Ω'` that is almost everywhere measurable with respect to the measure `ν`, for any measurable set `A` in `Ω'`, the measure of the image of `A` under the function `f` is equal to the measure of the preimage of `A` under `f`. Note that this equality holds in the space of extended non-negative real numbers `ℝ≥0∞`. The theorem also refers to a similar result, `MeasureTheory.FiniteMeasure.map_apply`, which gives the same equality in the space of non-negative real numbers `ℝ≥0`.
More concisely: For any finite measure `ν` on measurable spaces `Ω` and `Ω'`, and almost everywhere measurable function `f` from `Ω` to `Ω'`, the measure of `f''(A)` under `ν` is equal to the measure of `f⁻¹(A)` for any measurable set `A` in `Ω'` in the space of extended non-negative real numbers `ℝ≥0∞`.
|
MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_le_const
theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_le_const :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{μ : MeasureTheory.FiniteMeasure Ω} {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal},
(∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) →
∀ {f : BoundedContinuousFunction Ω NNReal},
(∀ (ω : Ω), Filter.Tendsto (fun n => (fs n) ω) Filter.atTop (nhds (f ω))) →
Filter.Tendsto (fun n => μ.testAgainstNN (fs n)) Filter.atTop (nhds (μ.testAgainstNN f))
This theorem is a bounded convergence theorem for a finite measure. It states that given a sequence of bounded continuous non-negative functions defined on a measurable and topological space, if these functions are uniformly bounded by a constant and converge pointwise to a limit, then the integrals of these functions with respect to a finite measure also converge to the integral of the limit function. This theorem is related to other results in measure theory, such as more general assumptions on bounded convergence and using the Lebesgue integral for integration.
More concisely: Let $(X, \Sigma, \mu)$ be a finite measure space, and let $f\_n : X \to \mathbb{R}$ be a sequence of bounded, continuous, non-negative functions such that $\sup\_{x \in X} \lvert f\_n(x) \rvert \leq M$ for some constant $M$. If $f\_n$ converges pointwise to $f : X \to \mathbb{R}$, then $\int\_X f\_n d\mu$ converges to $\int\_X f d\mu$.
|
MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto
theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto μs F (nhds μ) ↔
∀ (f : BoundedContinuousFunction Ω NNReal),
Filter.Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (nhds (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
The theorem `MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto` provides a characterization of weak convergence in measure theory. Specifically, it states that for any measurable and topological space `Ω` (that is also an opens measurable space), and any type `γ`, if `F` is a filter on `γ`, `μs` is a function from `γ` to the finite measures on `Ω`, and `μ` is a finite measure on `Ω`, then `μs` converges to `μ` in the neighborhood filter if and only if for every bounded continuous function `f` from `Ω` to the nonnegative real numbers, the Lebesgue integral of the function `f` with respect to the measure `μs i` converges in the filter `F` to the Lebesgue integral of the function `f` with respect to the measure `μ`.
More concisely: A sequence of finite measures on a measurable and topological space converges in the neighborhood filter if and only if the Lebesgue integrals of every bounded continuous function converge with respect to the sequence of measures.
|
MeasureTheory.FiniteMeasure.continuous_mass
theorem MeasureTheory.FiniteMeasure.continuous_mass :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
Continuous fun μ => μ.mass
This theorem states that the total mass (or the total measure) of a finite measure is a continuous function with respect to the measure. Here, Ω denotes the underlying set. The set Ω is equipped with a measurable space structure, a topological space structure, and the measurable structure is compatible with the topology (i.e., every open set is measurable). Given these structures, the theorem asserts that as you vary the measure, the total measure changes continuously.
More concisely: The total measure is a continuous function with respect to variations in the measure on the measurable space Ω, where Ω is a set equipped with a compatible measurable and topological structure.
|
MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const
theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{ι : Type u_2} {L : Filter ι} [inst_3 : L.IsCountablyGenerated] {μ : MeasureTheory.FiniteMeasure Ω}
{fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal},
(∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c) →
∀ {f : BoundedContinuousFunction Ω NNReal},
(∀ᵐ (ω : Ω) ∂↑μ, Filter.Tendsto (fun i => (fs i) ω) L (nhds (f ω))) →
Filter.Tendsto (fun i => μ.testAgainstNN (fs i)) L (nhds (μ.testAgainstNN f))
This theorem, named "MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const", states a bounded convergence result for a finite measure. It asserts that if a series of bounded, continuous, non-negative functions are uniformly bounded by a constant and converge to a limit, then the integrals of these functions with respect to the finite measure also tend to the integral of the limit function. The theorem makes several assumptions: the functions converge to the limit along a countably generated filter; the convergence to the limit is almost everywhere; the boundedness of the functions holds almost everywhere; and the integration is the pairing against non-negative, continuous test functions (`MeasureTheory.FiniteMeasure.testAgainstNN`). The theorem also refers to a related result using `MeasureTheory.lintegral` for integration, named `MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const`.
More concisely: If a sequence of bounded, continuous, non-negative functions converges uniformly to a limit function almost everywhere with respect to a finite measure, then the integrals of the sequence converge to the integral of the limit function with respect to the measure.
|
MeasureTheory.FiniteMeasure.continuous_map
theorem MeasureTheory.FiniteMeasure.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 : Ω → Ω'}, Continuous f → Continuous fun ν => ν.map f
This theorem states that if we have a continuous function `f` mapping from a type `Ω` to another type `Ω'`, and if `Ω'` is equipped with the Borel sigma algebra, then the push-forward of finite measures (denoted as `f*`) from `Ω` to `Ω'` is continuous. Here, continuity is defined in the context of the topologies of weak convergence of measures. This means the measures on `Ω'` obtained by "pushing forward" the measures on `Ω` via `f` will vary continuously as the measures on `Ω` vary, given the measures are converging weakly.
More concisely: If `f` is a continuous function from a measurable space `(Ω, Σ)` to a measurable space `(Ω', Σ')` where `Σ'` is the Borel sigma algebra, then `f` induces a continuous map from the space of Borel probability measures on `Ω` to the space of Borel probability measures on `Ω'`, under the weak topology.
|
MeasureTheory.FiniteMeasure.toMeasure_smul
theorem MeasureTheory.FiniteMeasure.toMeasure_smul :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
[inst_3 : IsScalarTower R NNReal ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal] (c : R)
(μ : MeasureTheory.FiniteMeasure Ω), ↑(c • μ) = c • ↑μ
This theorem, `MeasureTheory.FiniteMeasure.toMeasure_smul`, states that for any measure space Ω and any scalar `c` of a type `R` that can perform scalar multiplication on nonnegative real numbers (`NNReal`) and extended nonnegative real numbers (`ENNReal`), and where `R`, `NNReal`, and `ENNReal` form two scalar towers (meaning scalar multiplication respects associative law across these types), the scalar multiplication of `c` and a finite measure `μ` on Ω gets lifted to the finite measure space, and is equal to the scalar multiplication of `c` and the embedding of `μ` into an extended nonnegative real number (abbreviated as `c • ↑μ` in Lean). In other words, scalar multiplication commutes with the embedding of finite measures into the extended nonnegative real numbers.
More concisely: For any measure space Ω, scalar `c` of type `R` with scalar multiplication on nonnegative and extended nonnegative real numbers, and finite measure `μ` on Ω, `c • μ` equals `c • ↑μ`, where `↑μ` is the embedding of `μ` into an extended nonnegative real number.
|
MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq
theorem MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ ν : MeasureTheory.FiniteMeasure Ω),
(∀ (s : Set Ω), MeasurableSet s → ↑↑↑μ s = ↑↑↑ν s) → μ = ν
The theorem `MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq` states that for any type `Ω` with a `MeasurableSpace` instance and any two finite measures `μ` and `ν` on `Ω`, if for every measurable set `s`, the measure of `s` under `μ` equals the measure of `s` under `ν`, then `μ` must be equal to `ν`. In other words, two finite measures on a measurable space are considered equal if they assign the same measure to every measurable set within the space.
More concisely: If two finite measures assign equal measures to every measurable set in a measurable space, then they are equal.
|
MeasureTheory.FiniteMeasure.mass_nonzero_iff
theorem MeasureTheory.FiniteMeasure.mass_nonzero_iff :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω), μ.mass ≠ 0 ↔ μ ≠ 0
This theorem states that for any type Ω equipped with a measurable space structure and any finite measure μ on Ω, the mass of the finite measure μ is non-zero if and only if μ is not the zero measure. In other words, a finite measure on a measurable space has a non-zero mass exactly when it is not the zero measure.
More concisely: A finite measure on a measurable space is non-zero if and only if it is not the zero measure.
|
MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto
theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto μs F (nhds μ) ↔
∀ (f : BoundedContinuousFunction Ω ℝ),
Filter.Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (nhds (∫ (x : Ω), f x ∂↑μ))
This theorem provides a characterization of weak convergence in terms of integrals of bounded continuous real-valued functions. It states that for any measurable and topological space Ω that is also an open measurable space, any filter γ, any sequence of finite measures μs on Ω indexed by γ, and any finite measure μ on Ω, the sequence of measures μs converges to the measure μ 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 other words, the weak convergence of a sequence of finite measures is equivalent to the pointwise convergence of the integrals of all bounded continuous functions.
More concisely: A sequence of finite measures on a measurable and open space Ω converges weakly to a measure μ if and only if for all bounded continuous functions f from Ω to the real numbers, the integrals of f with respect to the measures μs converge to the integral of f with respect to μ.
|
MeasureTheory.FiniteMeasure.tendsto_map_of_tendsto_of_continuous
theorem MeasureTheory.FiniteMeasure.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.FiniteMeasure Ω)
(ν : MeasureTheory.FiniteMeasure Ω),
Filter.Tendsto νs L (nhds ν) →
∀ {f : Ω → Ω'}, Continuous f → Filter.Tendsto (fun i => (νs i).map f) L (nhds (ν.map f))
This theorem states that if we have a continuous function `f` which maps from a topological space `X` (designated as `Ω`) to another topological space `Y` (designated as `Ω'`) equipped with the Borel sigma algebra, and a sequence of finite measures (denoted `νs`) on `X` that converge to a finite measure `ν` (in the weak sense), then the sequence of push-forwards of these measures by `f` also converges (weakly) to the push-forward of `ν` by `f`. In other words, the convergence of finite measures is preserved under the mapping by a continuous function when the target space is equipped with the Borel sigma algebra. This property is crucial in various limit theorems in probability theory and measure theory.
More concisely: If `f` is a continuous function from a topological space `X` to a Borel space `Y`, and `νs` is a sequence of finite measures on `X` converging weakly to a finite measure `ν`, then `f_*\nu_s` converges weakly to `f_*\nu` on `Y`.
|
MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq
theorem MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω}
{f : BoundedContinuousFunction Ω NNReal}, ↑(μ.testAgainstNN f) = ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ
The theorem `MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq` states that for any given finite measure space 'Ω', any finite measure 'μ' on that space, and any bounded continuous function 'f' from 'Ω' to the nonnegative real numbers, the pairing of the finite measure 'μ' with the function 'f' (obtained by integrating the function against the measure) is equal to the Lebesgue integral of the function 'f' against the measure 'μ'. In simpler terms, the measure-theoretic integration of the function with respect to the finite measure is accurately represented by the `testAgainstNN` function.
More concisely: For any finite measure space 'Ω', finite measure 'μ' on 'Ω', and bounded continuous function 'f' from 'Ω' to the nonnegative real numbers, the integral of 'f' with respect to 'μ' (as a measure-theoretic integral) equals the Lebesgue integral of 'f' against 'μ'.
|
Mathlib.MeasureTheory.Measure.FiniteMeasure._auxLemma.5
theorem Mathlib.MeasureTheory.Measure.FiniteMeasure._auxLemma.5 : ∀ {p q : NNReal}, (p = q) = (↑p = ↑q)
This theorem states that for any two nonnegative real numbers `p` and `q`, `p` is equal to `q` if and only if the real number part of `p` (denoted as `↑p`) is equal to the real number part of `q` (denoted as `↑q`). This is essentially saying that two nonnegative real numbers are equal if their underlying real numbers are equal.
More concisely: For any nonnegative real numbers `p` and `q`, `p = q` if and only if `↑p = ↑q`.
|
MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq
theorem MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : HasOuterApproxClosed Ω]
[inst_3 : BorelSpace Ω] {μ ν : MeasureTheory.FiniteMeasure Ω},
(∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν) → μ = ν
This theorem states that for any topological measurable space Ω with a Borel σ-algebra, given two finite Borel measures `μ` and `ν` on Ω, if for every bounded continuous function `f` from Ω to the nonnegative real numbers, the integral of `f` with respect to `μ` is equal to the integral of `f` with respect to `ν`, then we can conclude that the two measures `μ` and `ν` are equal.
More concisely: If two finite Borel measures on a topological measurable space with a Borel σ-algebra have equal integrals for every bounded continuous function, then they are equal.
|
MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass
theorem MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto (fun i => (μs i).mass) F (nhds 0) →
∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (nhds 0)
This theorem, `MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass`, states that for any measurable and topological space Ω, with Ω also being an opens measurable space, and any type γ, if a sequence of finite measures μs (from γ to Ω) has total masses that tend towards zero (in the filter F), then for any bounded continuous nonnegative test function on Ω, the functional of these measures against the test function also tends to zero in the same filter. In other words, if the total weight (mass) of the measures is decreasing towards zero, then the measures themselves are "vanishing" when tested against bounded continuous nonnegative functions. This theorem is related to the weak convergence of measures.
More concisely: If a sequence of finite measures on an Open Measurable Space with total masses tending to zero in a filter converges, then the functional of these measures against any bounded continuous nonnegative test function tends to zero in the same filter.
|
MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
{γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
Filter.Tendsto μs F (nhds μ) ↔
∀ (f : BoundedContinuousFunction Ω NNReal),
Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (nhds (μ.testAgainstNN f))
This theorem states that for any given measurable and topological space with the open sets also being measurable, a filter and a sequence of finite measures defined on the space, and a finite measure, the sequence of finite measures converges to the given finite measure if and only if for every bounded continuous function from the space to the non-negative real numbers, the sequence of results obtained by integrating the function against the measures (i.e., testing the function against the measures) also converges to the result obtained by integrating the function against the given finite measure. This is with respect to the respective neighborhood filters of the measure and the integrals.
More concisely: A sequence of measurable finite measures on a measurable and topological space converges to a given finite measure if and only if the sequence of integrals of every bounded continuous function against the measures converges to the integral of that function against the given measure.
|
MeasureTheory.FiniteMeasure.coeFn_smul_apply
theorem MeasureTheory.FiniteMeasure.coeFn_smul_apply :
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
[inst_3 : IsScalarTower R NNReal ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal]
[inst_5 : IsScalarTower R NNReal NNReal] (c : R) (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω),
(fun s => (↑↑↑(c • μ) s).toNNReal) s = c • (fun s => (↑↑↑μ s).toNNReal) s
The theorem `MeasureTheory.FiniteMeasure.coeFn_smul_apply` states that for any measurable space `Ω`, any type `R` that can multiply nonnegative real numbers and extended nonnegative real numbers, and which forms scalar towers with these types, any scalar `c` of type `R`, any finite measure `μ` on `Ω`, and any set `s` in `Ω`, the measure of the set `s` under the measure obtained by scaling `μ` by `c` (when converted to a nonnegative real number) is the same as the scalar `c` multiplied by the measure of `s` under `μ` (when converted to a nonnegative real number).
In other words, scaling a finite measure and then measuring a set is the same as first measuring the set and then scaling the result. This illustrates a fundamental property of measures known as homogeneity.
More concisely: For any measurable space Ω, any scalar c of type R that can multiply nonnegative real numbers and extended nonnegative real numbers, and forms scalar towers with these types, and for any finite measure μ on Ω and measurable set s in Ω, the measure of s under the scaled measure μ' = μ * c is equal to the measure of s under μ multiplied by c as real numbers, i.e., μ'(s) = μ(s) * c.
|