Probability measures

This file defines the type of probability measures on a given measurable space. When the underlying space has a topology and the measurable space structure (sigma algebra) is finer than the Borel sigma algebra, then the type of probability measures is equipped with the topology of convergence in distribution (weak convergence of measures). The topology of convergence in distribution is the coarsest topology w.r.t. which for every bounded continuous ℝ≥0-valued random variable X, the expected value of X depends continuously on the choice of probability measure. This is a special case of the topology of weak convergence of finite measures.

Main definitions

The main definitions are

• the type MeasureTheory.ProbabilityMeasure Ω with the topology of convergence in distribution (a.k.a. convergence in law, weak convergence of measures);
• MeasureTheory.ProbabilityMeasure.toFiniteMeasure: Interpret a probability measure as a finite measure;
• MeasureTheory.FiniteMeasure.normalize: Normalize a finite measure to a probability measure (returns junk for the zero measure).
• MeasureTheory.ProbabilityMeasure.map: The push-forward f* μ of a probability measure μ on Ω along a measurable function f : Ω → Ω'.

Main results

• MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto: Convergence of probability measures is characterized by the convergence of expected values of all bounded continuous random variables. This shows that the chosen definition of topology coincides with the common textbook definition of convergence in distribution, i.e., weak convergence of measures. A similar characterization by the convergence of expected values (in the MeasureTheory.lintegral sense) of all bounded continuous nonnegative random variables is MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto.
• MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto: The convergence of finite measures to a nonzero limit is characterized by the convergence of the probability-normalized versions and of the total masses.
• MeasureTheory.ProbabilityMeasure.continuous_map: For a continuous function f : Ω → Ω', the push-forward of probability measures f* : ProbabilityMeasure Ω → ProbabilityMeasure Ω' is continuous.
• MeasureTheory.ProbabilityMeasure.t2Space: The topology of convergence in distribution is Hausdorff on Borel spaces where indicators of closed sets have continuous decreasing approximating sequences (in particular on any pseudo-metrizable spaces).

TODO:

• Probability measures form a convex space.

Implementation notes

The topology of convergence in distribution on MeasureTheory.ProbabilityMeasure Ω is inherited weak convergence of finite measures via the mapping MeasureTheory.ProbabilityMeasure.toFiniteMeasure.

Like MeasureTheory.FiniteMeasure Ω, the implementation of MeasureTheory.ProbabilityMeasure Ω is directly as a subtype of MeasureTheory.Measure Ω, and the coercion to a function is the composition ENNReal.toNNReal and the coercion to function of MeasureTheory.Measure Ω.

References

• Billingsley, Convergence of probability measures

Tags

convergence in distribution, convergence in law, weak convergence of measures, probability measure

Probability measures

In this section we define the type of probability measures on a measurable space Ω, denoted by MeasureTheory.ProbabilityMeasure Ω.

If Ω is moreover a topological space and the sigma algebra on Ω is finer than the Borel sigma algebra (i.e. [OpensMeasurableSpace Ω]), then MeasureTheory.ProbabilityMeasure Ω is equipped with the topology of weak convergence of measures. Since every probability measure is a finite measure, this is implemented as the induced topology from the mapping MeasureTheory.ProbabilityMeasure.toFiniteMeasure.

def MeasureTheory.ProbabilityMeasure (Ω : Type u_1) [MeasurableSpace Ω] : Type u_1

Probability measures are defined as the subtype of measures that have the property of being probability measures (i.e., their total mass is one).

Equations

• MeasureTheory.ProbabilityMeasure Ω = { μ : MeasureTheory.Measure Ω // MeasureTheory.IsProbabilityMeasure μ }

instance MeasureTheory.ProbabilityMeasure.instInhabited {Ω : Type u_1} [MeasurableSpace Ω] [Inhabited Ω] : Inhabited (MeasureTheory.ProbabilityMeasure Ω)

Equations

• MeasureTheory.ProbabilityMeasure.instInhabited = { default := ⟨MeasureTheory.Measure.dirac default, ⋯⟩ }

def MeasureTheory.ProbabilityMeasure.toMeasure {Ω : Type u_1} [MeasurableSpace Ω] : MeasureTheory.ProbabilityMeasure Ω → MeasureTheory.Measure Ω

Coercion from MeasureTheory.ProbabilityMeasure Ω to MeasureTheory.Measure Ω.

Equations

• MeasureTheory.ProbabilityMeasure.toMeasure = Subtype.val

instance MeasureTheory.ProbabilityMeasure.instCoeMeasure {Ω : Type u_1} [MeasurableSpace Ω] : Coe (MeasureTheory.ProbabilityMeasure Ω) (MeasureTheory.Measure Ω)

A probability measure can be interpreted as a measure.

Equations

• MeasureTheory.ProbabilityMeasure.instCoeMeasure = { coe := MeasureTheory.ProbabilityMeasure.toMeasure }

instance MeasureTheory.ProbabilityMeasure.instIsProbabilityMeasureToMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : MeasureTheory.IsProbabilityMeasure ↑μ

Equations

• ⋯ = ⋯

@[simp]

theorem MeasureTheory.ProbabilityMeasure.coe_mk {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ) : ↑⟨μ, hμ⟩ = μ

@[simp]

theorem MeasureTheory.ProbabilityMeasure.val_eq_to_measure {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) : ↑ν = ↑ν

theorem MeasureTheory.ProbabilityMeasure.toMeasure_injective {Ω : Type u_1} [MeasurableSpace Ω] : Function.Injective MeasureTheory.ProbabilityMeasure.toMeasure

instance MeasureTheory.ProbabilityMeasure.instFunLike {Ω : Type u_1} [MeasurableSpace Ω] : FunLike (MeasureTheory.ProbabilityMeasure Ω) (Set Ω) NNReal

Equations

• MeasureTheory.ProbabilityMeasure.instFunLike = { coe := fun (μ : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω) => (↑μ s).toNNReal, coe_injective' := ⋯ }

theorem MeasureTheory.ProbabilityMeasure.coeFn_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : ⇑μ = fun (s : Set Ω) => (↑μ s).toNNReal

theorem MeasureTheory.ProbabilityMeasure.coeFn_mk {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ) : ⇑⟨μ, hμ⟩ = fun (s : Set Ω) => (μ s).toNNReal

@[simp]

theorem MeasureTheory.ProbabilityMeasure.mk_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ) (s : Set Ω) : ⟨μ, hμ⟩ s = (μ s).toNNReal

@[simp]

theorem MeasureTheory.ProbabilityMeasure.coeFn_univ {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) : ν Set.univ = 1

theorem MeasureTheory.ProbabilityMeasure.coeFn_univ_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) : ν Set.univ ≠ 0

def MeasureTheory.ProbabilityMeasure.toFiniteMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : MeasureTheory.FiniteMeasure Ω

A probability measure can be interpreted as a finite measure.

Equations

• μ.toFiniteMeasure = ⟨↑μ, ⋯⟩

@[simp]

theorem MeasureTheory.ProbabilityMeasure.coeFn_toFiniteMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : ⇑μ.toFiniteMeasure = ⇑μ

theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω) : μ.toFiniteMeasure s = μ s

@[simp]

theorem MeasureTheory.ProbabilityMeasure.toMeasure_comp_toFiniteMeasure_eq_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) : ↑ν.toFiniteMeasure = ↑ν

@[simp]

theorem MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) : ⇑ν.toFiniteMeasure = ⇑ν

@[simp]

theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply_eq_apply {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω) : ν.toFiniteMeasure s = ν s

@[simp]

theorem MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω) : ↑(ν s) = ↑ν s

@[simp]

theorem MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω) : ν s = 0 ↔ ↑ν s = 0

theorem MeasureTheory.ProbabilityMeasure.apply_mono {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {s₁ s₂ : Set Ω} (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂

@[simp]

theorem MeasureTheory.ProbabilityMeasure.apply_le_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω) : μ s ≤ 1

theorem MeasureTheory.ProbabilityMeasure.nonempty {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : Nonempty Ω

theorem MeasureTheory.ProbabilityMeasure.eq_of_forall_toMeasure_apply_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s) : μ = ν

theorem MeasureTheory.ProbabilityMeasure.eq_of_forall_apply_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω) (h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s) : μ = ν

@[simp]

theorem MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : μ.toFiniteMeasure.mass = 1

theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_nonzero {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : μ.toFiniteMeasure ≠ 0

theorem MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : LipschitzWith 1 fun (f : BoundedContinuousFunction Ω NNReal) => μ.toFiniteMeasure.testAgainstNN f

instance MeasureTheory.ProbabilityMeasure.instTopologicalSpace {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : TopologicalSpace (MeasureTheory.ProbabilityMeasure Ω)

The topology of weak convergence on MeasureTheory.ProbabilityMeasure Ω. This is inherited (induced) from the topology of weak convergence of finite measures via the inclusion MeasureTheory.ProbabilityMeasure.toFiniteMeasure.

Equations

• MeasureTheory.ProbabilityMeasure.instTopologicalSpace = TopologicalSpace.induced MeasureTheory.ProbabilityMeasure.toFiniteMeasure inferInstance

theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_continuous {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : Continuous MeasureTheory.ProbabilityMeasure.toFiniteMeasure

def MeasureTheory.ProbabilityMeasure.toWeakDualBCNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : MeasureTheory.ProbabilityMeasure Ω → WeakDual NNReal (BoundedContinuousFunction Ω NNReal)

Probability measures yield elements of the WeakDual of bounded continuous nonnegative functions via MeasureTheory.FiniteMeasure.testAgainstNN, i.e., integration.

Equations

• MeasureTheory.ProbabilityMeasure.toWeakDualBCNN = MeasureTheory.FiniteMeasure.toWeakDualBCNN ∘ MeasureTheory.ProbabilityMeasure.toFiniteMeasure

@[simp]

theorem MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) : ⇑μ.toWeakDualBCNN = μ.toFiniteMeasure.testAgainstNN

@[simp]

theorem MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) : μ.toWeakDualBCNN f = (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ).toNNReal

theorem MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : Continuous fun (μ : MeasureTheory.ProbabilityMeasure Ω) => μ.toWeakDualBCNN

theorem MeasureTheory.ProbabilityMeasure.continuous_testAgainstNN_eval {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (f : BoundedContinuousFunction Ω NNReal) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure Ω) => μ.toFiniteMeasure.testAgainstNN f

theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding (Ω : Type u_2) [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : Topology.IsEmbedding MeasureTheory.ProbabilityMeasure.toFiniteMeasure

@[deprecated MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding]

theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_embedding (Ω : Type u_2) [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : Topology.IsEmbedding MeasureTheory.ProbabilityMeasure.toFiniteMeasure

Alias of MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding.

theorem MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [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)

theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [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 ω) ∂↑μ))

A characterization of weak convergence of probability measures by the condition that the integrals of every continuous bounded nonnegative function converge to the integral of the function against the limit measure.

theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [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 ω ∂↑μ))

The characterization of weak convergence of probability measures by the usual (defining) condition that the integrals of every continuous bounded function converge to the integral of the function against the limit measure.

theorem MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunction {α : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (f : BoundedContinuousFunction α ℝ) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure α) => ∫ (x : α), f x ∂↑μ

instance MeasureTheory.ProbabilityMeasure.t2Space (Ω : Type u_1) [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] : T2Space (MeasureTheory.ProbabilityMeasure Ω)

On topological spaces where indicators of closed sets have decreasing approximating sequences of continuous functions (HasOuterApproxClosed), the topology of convergence in distribution of Borel probability measures is Hausdorff (T2Space).

Equations

• ⋯ = ⋯

Normalization of finite measures to probability measures

This section is about normalizing finite measures to probability measures.

The weak convergence of finite measures to nonzero limit measures is characterized by the convergence of the total mass and the convergence of the normalized probability measures.

def MeasureTheory.FiniteMeasure.normalize {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) : MeasureTheory.ProbabilityMeasure Ω

Normalize a finite measure so that it becomes a probability measure, i.e., divide by the total mass.

Equations

• μ.normalize = if zero : μ.mass = 0 then ⟨MeasureTheory.Measure.dirac inst.some, ⋯⟩ else ⟨↑(μ.mass⁻¹ • μ), ⋯⟩

@[simp]

theorem MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) : μ s = μ.mass * μ.normalize s

theorem MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) : μ = μ.mass • μ.normalize.toFiniteMeasure

theorem MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (nonzero : μ ≠ 0) (s : Set Ω) : μ.normalize s = μ.mass⁻¹ * μ s

theorem MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (nonzero : μ ≠ 0) : μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ

theorem MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (nonzero : μ ≠ 0) : ↑μ.normalize = μ.mass⁻¹ • ↑μ

@[simp]

theorem ProbabilityMeasure.toFiniteMeasure_normalize_eq_self {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.ProbabilityMeasure Ω) : μ.toFiniteMeasure.normalize = μ

theorem MeasureTheory.FiniteMeasure.average_eq_integral_normalize {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (nonzero : μ ≠ 0) (f : Ω → E) : MeasureTheory.average (↑μ) f = ∫ (ω : Ω), f ω ∂↑μ.normalize

Averaging with respect to a finite measure is the same as integrating against MeasureTheory.FiniteMeasure.normalize.

theorem MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) [TopologicalSpace Ω] (f : BoundedContinuousFunction Ω NNReal) : μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

theorem MeasureTheory.FiniteMeasure.normalize_testAgainstNN {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) [TopologicalSpace Ω] (nonzero : μ ≠ 0) (f : BoundedContinuousFunction Ω NNReal) : μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f

theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto (fun (i : γ) => (μs i).normalize) F (nhds μ.normalize)) (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds μ.mass)) (f : BoundedContinuousFunction Ω NNReal) : Filter.Tendsto (fun (i : γ) => (μs i).testAgainstNN f) F (nhds (μ.testAgainstNN f))

theorem MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto μs F (nhds μ)) (nonzero : μ ≠ 0) (f : BoundedContinuousFunction Ω NNReal) : Filter.Tendsto (fun (i : γ) => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (nhds (μ.normalize.toFiniteMeasure.testAgainstNN f))

theorem MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto (fun (i : γ) => (μs i).normalize) F (nhds μ.normalize)) (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds μ.mass)) : Filter.Tendsto μs F (nhds μ)

If the normalized versions of finite measures converge weakly and their total masses also converge, then the finite measures themselves converge weakly.

theorem MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto μs F (nhds μ)) (nonzero : μ ≠ 0) : Filter.Tendsto (fun (i : γ) => (μs i).normalize) F (nhds μ.normalize)

If finite measures themselves converge weakly to a nonzero limit measure, then their normalized versions also converge weakly.

theorem MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} (nonzero : μ ≠ 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 μ)

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.

noncomputable def MeasureTheory.ProbabilityMeasure.map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) : MeasureTheory.ProbabilityMeasure Ω'

The push-forward of a probability measure by a measurable function.

Equations

• ν.map f_aemble = ⟨MeasureTheory.Measure.map f ↑ν, ⋯⟩

@[simp]

theorem MeasureTheory.ProbabilityMeasure.toMeasure_map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (hf : AEMeasurable f ↑ν) : ↑(ν.map hf) = MeasureTheory.Measure.map f ↑ν

theorem MeasureTheory.ProbabilityMeasure.map_apply' {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'} (A_mble : MeasurableSet A) : ↑(ν.map f_aemble) A = ↑ν (f ⁻¹' A)

Note that this is an equality of elements of ℝ≥0∞. See also MeasureTheory.ProbabilityMeasure.map_apply for the corresponding equality as elements of ℝ≥0.

theorem MeasureTheory.ProbabilityMeasure.map_apply_of_aemeasurable {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'} (A_mble : MeasurableSet A) : (ν.map f_aemble) A = ν (f ⁻¹' A)

theorem MeasureTheory.ProbabilityMeasure.map_apply {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'} (A_mble : MeasurableSet A) : (ν.map f_aemble) A = ν (f ⁻¹' A)

theorem MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω'] {ι : Type u_3} {L : Filter ι} (νs : ι → MeasureTheory.ProbabilityMeasure Ω) (ν : MeasureTheory.ProbabilityMeasure Ω) (lim : Filter.Tendsto νs L (nhds ν)) {f : Ω → Ω'} (f_cont : Continuous f) : Filter.Tendsto (fun (i : ι) => (νs i).map ⋯) L (nhds (ν.map ⋯))

If f : X → Y is continuous and Y is equipped with the Borel sigma algebra, then convergence (in distribution) of ProbabilityMeasures on X implies convergence (in distribution) of the push-forwards of these measures by f.

theorem MeasureTheory.ProbabilityMeasure.continuous_map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω'] {f : Ω → Ω'} (f_cont : Continuous f) : Continuous fun (ν : MeasureTheory.ProbabilityMeasure Ω) => ν.map ⋯

If f : X → Y is continuous and Y is equipped with the Borel sigma algebra, then the push-forward of probability measures f* : ProbabilityMeasure X → ProbabilityMeasure Y is continuous (in the topologies of convergence in distribution).