mathlib3 documentation

measure_theory.measure.probability_measure

Probability measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measure_theory.probability_measure Ω with the topology of convergence in distribution (a.k.a. convergence in law, weak convergence of measures);
measure_theory.probability_measure.to_finite_measure: Interpret a probability measure as a finite measure;
measure_theory.finite_measure.normalize: Normalize a finite measure to a probability measure (returns junk for the zero measure).

Main results #

measure_theory.probability_measure.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 measure_theory.lintegral sense) of all bounded continuous nonnegative random variables is measure_theory.probability_measure.tendsto_iff_forall_lintegral_tendsto.
measure_theory.finite_measure.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.

TODO:

Probability measures form a convex space.

Implementation notes #

The topology of convergence in distribution on measure_theory.probability_measure Ω is inherited weak convergence of finite measures via the mapping measure_theory.probability_measure.to_finite_measure.

Like measure_theory.finite_measure Ω, the implementation of measure_theory.probability_measure Ω is directly as a subtype of measure_theory.measure Ω, and the coercion to a function is the composition ennreal.to_nnreal and the coercion to function of measure_theory.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 measure_theory.probability_measure Ω.

If Ω is moreover a topological space and the sigma algebra on Ω is finer than the Borel sigma algebra (i.e. [opens_measurable_space Ω]), then measure_theory.probability_measure Ω 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 measure_theory.probability_measure.to_finite_measure.

def measure_theory.probability_measure (Ω : Type u_1) [measurable_space Ω] :

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

measure_theory.probability_measure Ω = {μ // measure_theory.is_probability_measure μ}

Instances for measure_theory.probability_measure

@[protected, instance]

noncomputable def measure_theory.probability_measure.inhabited {Ω : Type u_1} [measurable_space Ω] [inhabited Ω] :

inhabited (measure_theory.probability_measure Ω)

Equations

measure_theory.probability_measure.inhabited = {default := ⟨measure_theory.measure.dirac inhabited.default, _⟩}

@[protected, instance]

def measure_theory.probability_measure.measure_theory.measure.has_coe {Ω : Type u_1} [measurable_space Ω] :

has_coe (measure_theory.probability_measure Ω) (measure_theory.measure Ω)

A probability measure can be interpreted as a measure.

Equations

measure_theory.probability_measure.measure_theory.measure.has_coe = coe_subtype

@[protected, instance]

def measure_theory.probability_measure.has_coe_to_fun {Ω : Type u_1} [measurable_space Ω] :

has_coe_to_fun (measure_theory.probability_measure Ω) (λ (_x : measure_theory.probability_measure Ω), set Ω → nnreal)

Equations

measure_theory.probability_measure.has_coe_to_fun = {coe := λ (μ : measure_theory.probability_measure Ω) (s : set Ω), (⇑μ s).to_nnreal}

@[protected, instance]

def measure_theory.probability_measure.measure_theory.is_probability_measure {Ω : Type u_1} [measurable_space Ω] (μ : measure_theory.probability_measure Ω) :

measure_theory.is_probability_measure ↑μ

theorem measure_theory.probability_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure {Ω : Type u_1} [measurable_space Ω] (ν : measure_theory.probability_measure Ω) :

⇑ν = λ (s : set Ω), (⇑↑ν s).to_nnreal

@[simp]

theorem measure_theory.probability_measure.val_eq_to_measure {Ω : Type u_1} [measurable_space Ω] (ν : measure_theory.probability_measure Ω) :

ν.val = ↑ν

theorem measure_theory.probability_measure.coe_injective {Ω : Type u_1} [measurable_space Ω] :

function.injective coe

@[simp]

theorem measure_theory.probability_measure.coe_fn_univ {Ω : Type u_1} [measurable_space Ω] (ν : measure_theory.probability_measure Ω) :

⇑ν set.univ = 1

theorem measure_theory.probability_measure.coe_fn_univ_ne_zero {Ω : Type u_1} [measurable_space Ω] (ν : measure_theory.probability_measure Ω) :

⇑ν set.univ ≠ 0

def measure_theory.probability_measure.to_finite_measure {Ω : Type u_1} [measurable_space Ω] (μ : measure_theory.probability_measure Ω) :

measure_theory.finite_measure Ω

A probability measure can be interpreted as a finite measure.

Equations

μ.to_finite_measure = ⟨↑μ, _⟩

@[simp]

theorem measure_theory.probability_measure.coe_comp_to_finite_measure_eq_coe {Ω : Type u_1} [measurable_space Ω] (ν : measure_theory.probability_measure Ω) :

↑(ν.to_finite_measure) = ↑ν

@[simp]

theorem measure_theory.probability_measure.coe_fn_comp_to_finite_measure_eq_coe_fn {Ω : Type u_1} [measurable_space Ω] (ν : measure_theory.probability_measure Ω) :

⇑(ν.to_finite_measure) = ⇑ν

@[simp]

theorem measure_theory.probability_measure.ennreal_coe_fn_eq_coe_fn_to_measure {Ω : Type u_1} [measurable_space Ω] (ν : measure_theory.probability_measure Ω) (s : set Ω) :

↑(⇑ν s) = ⇑↑ν s

theorem measure_theory.probability_measure.apply_mono {Ω : Type u_1} [measurable_space Ω] (μ : measure_theory.probability_measure Ω) {s₁ s₂ : set Ω} (h : s₁ ⊆ s₂) :

⇑μ s₁ ≤ ⇑μ s₂

theorem measure_theory.probability_measure.nonempty_of_probability_measure {Ω : Type u_1} [measurable_space Ω] (μ : measure_theory.probability_measure Ω) :

@[ext]

theorem measure_theory.probability_measure.eq_of_forall_measure_apply_eq {Ω : Type u_1} [measurable_space Ω] (μ ν : measure_theory.probability_measure Ω) (h : ∀ (s : set Ω), measurable_set s → ⇑↑μ s = ⇑↑ν s) :

μ = ν

theorem measure_theory.probability_measure.eq_of_forall_apply_eq {Ω : Type u_1} [measurable_space Ω] (μ ν : measure_theory.probability_measure Ω) (h : ∀ (s : set Ω), measurable_set s → ⇑μ s = ⇑ν s) :

μ = ν

@[simp]

theorem measure_theory.probability_measure.mass_to_finite_measure {Ω : Type u_1} [measurable_space Ω] (μ : measure_theory.probability_measure Ω) :

μ.to_finite_measure.mass = 1

theorem measure_theory.probability_measure.to_finite_measure_nonzero {Ω : Type u_1} [measurable_space Ω] (μ : measure_theory.probability_measure Ω) :

μ.to_finite_measure ≠ 0

theorem measure_theory.probability_measure.test_against_nn_lipschitz {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] (μ : measure_theory.probability_measure Ω) :

lipschitz_with 1 (λ (f : bounded_continuous_function Ω nnreal), μ.to_finite_measure.test_against_nn f)

@[protected, instance]

noncomputable def measure_theory.probability_measure.topological_space {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] :

topological_space (measure_theory.probability_measure Ω)

The topology of weak convergence on measure_theory.probability_measure Ω. This is inherited (induced) from the topology of weak convergence of finite measures via the inclusion measure_theory.probability_measure.to_finite_measure.

Equations

measure_theory.probability_measure.topological_space = topological_space.induced measure_theory.probability_measure.to_finite_measure infer_instance

theorem measure_theory.probability_measure.to_finite_measure_continuous {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] :

continuous measure_theory.probability_measure.to_finite_measure

noncomputable def measure_theory.probability_measure.to_weak_dual_bcnn {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] :

measure_theory.probability_measure Ω → weak_dual nnreal (bounded_continuous_function Ω nnreal)

Probability measures yield elements of the weak_dual of bounded continuous nonnegative functions via measure_theory.finite_measure.test_against_nn, i.e., integration.

Equations

measure_theory.probability_measure.to_weak_dual_bcnn = measure_theory.finite_measure.to_weak_dual_bcnn ∘ measure_theory.probability_measure.to_finite_measure

@[simp]

theorem measure_theory.probability_measure.coe_to_weak_dual_bcnn {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] (μ : measure_theory.probability_measure Ω) :

⇑(μ.to_weak_dual_bcnn) = μ.to_finite_measure.test_against_nn

@[simp]

theorem measure_theory.probability_measure.to_weak_dual_bcnn_apply {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] (μ : measure_theory.probability_measure Ω) (f : bounded_continuous_function Ω nnreal) :

⇑(μ.to_weak_dual_bcnn) f = (∫⁻ (ω : Ω), ↑(⇑f ω) ∂↑μ).to_nnreal

theorem measure_theory.probability_measure.to_weak_dual_bcnn_continuous {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] :

continuous (λ (μ : measure_theory.probability_measure Ω), μ.to_weak_dual_bcnn)

theorem measure_theory.probability_measure.continuous_test_against_nn_eval {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] (f : bounded_continuous_function Ω nnreal) :

continuous (λ (μ : measure_theory.probability_measure Ω), μ.to_finite_measure.test_against_nn f)

theorem measure_theory.probability_measure.to_finite_measure_embedding (Ω : Type u_1) [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] :

embedding measure_theory.probability_measure.to_finite_measure

theorem measure_theory.probability_measure.tendsto_nhds_iff_to_finite_measures_tendsto_nhds {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] {δ : Type u_2} (F : filter δ) {μs : δ → measure_theory.probability_measure Ω} {μ₀ : measure_theory.probability_measure Ω} :

filter.tendsto μs F (nhds μ₀) ↔ filter.tendsto (measure_theory.probability_measure.to_finite_measure ∘ μs) F (nhds μ₀.to_finite_measure)

theorem measure_theory.probability_measure.tendsto_iff_forall_lintegral_tendsto {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.probability_measure Ω} {μ : measure_theory.probability_measure Ω} :

filter.tendsto μs F (nhds μ) ↔ ∀ (f : bounded_continuous_function Ω nnreal), filter.tendsto (λ (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 measure_theory.probability_measure.tendsto_iff_forall_integral_tendsto {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.probability_measure Ω} {μ : measure_theory.probability_measure Ω} :

filter.tendsto μs F (nhds μ) ↔ ∀ (f : bounded_continuous_function Ω ℝ), filter.tendsto (λ (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.

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.

noncomputable def measure_theory.finite_measure.normalize {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) :

measure_theory.probability_measure Ω

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

Equations

μ.normalize = dite (μ.mass = 0) (λ (zero : μ.mass = 0), ⟨measure_theory.measure.dirac _inst_1.some, _⟩) (λ (zero : ¬μ.mass = 0), ⟨(μ.mass)⁻¹ • ↑μ, _⟩)

@[simp]

theorem measure_theory.finite_measure.self_eq_mass_mul_normalize {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) (s : set Ω) :

⇑μ s = μ.mass * ⇑(μ.normalize) s

theorem measure_theory.finite_measure.self_eq_mass_smul_normalize {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) :

μ = μ.mass • μ.normalize.to_finite_measure

theorem measure_theory.finite_measure.normalize_eq_of_nonzero {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) (nonzero : μ ≠ 0) (s : set Ω) :

⇑(μ.normalize) s = (μ.mass)⁻¹ * ⇑μ s

theorem measure_theory.finite_measure.normalize_eq_inv_mass_smul_of_nonzero {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) (nonzero : μ ≠ 0) :

μ.normalize.to_finite_measure = (μ.mass)⁻¹ • μ

theorem measure_theory.finite_measure.coe_normalize_eq_of_nonzero {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) (nonzero : μ ≠ 0) :

↑(μ.normalize) = (μ.mass)⁻¹ • ↑μ

@[simp]

theorem probability_measure.to_finite_measure_normalize_eq_self {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.probability_measure Ω) :

μ.to_finite_measure.normalize = μ

theorem measure_theory.finite_measure.average_eq_integral_normalize {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (nonzero : μ ≠ 0) (f : Ω → E) :

measure_theory.average ↑μ f = ∫ (ω : Ω), f ω ∂↑(μ.normalize)

Averaging with respect to a finite measure is the same as integraing against measure_theory.finite_measure.normalize.

theorem measure_theory.finite_measure.test_against_nn_eq_mass_mul {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) [topological_space Ω] (f : bounded_continuous_function Ω nnreal) :

μ.test_against_nn f = μ.mass * μ.normalize.to_finite_measure.test_against_nn f

theorem measure_theory.finite_measure.normalize_test_against_nn {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} (μ : measure_theory.finite_measure Ω) [topological_space Ω] (nonzero : μ ≠ 0) (f : bounded_continuous_function Ω nnreal) :

μ.normalize.to_finite_measure.test_against_nn f = (μ.mass)⁻¹ * μ.test_against_nn f

theorem measure_theory.finite_measure.tendsto_test_against_nn_of_tendsto_normalize_test_against_nn_of_tendsto_mass {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} {μ : measure_theory.finite_measure Ω} [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure Ω} (μs_lim : filter.tendsto (λ (i : γ), (μs i).normalize) F (nhds μ.normalize)) (mass_lim : filter.tendsto (λ (i : γ), (μs i).mass) F (nhds μ.mass)) (f : bounded_continuous_function Ω nnreal) :

filter.tendsto (λ (i : γ), (μs i).test_against_nn f) F (nhds (μ.test_against_nn f))

theorem measure_theory.finite_measure.tendsto_normalize_test_against_nn_of_tendsto {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} {μ : measure_theory.finite_measure Ω} [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure Ω} (μs_lim : filter.tendsto μs F (nhds μ)) (nonzero : μ ≠ 0) (f : bounded_continuous_function Ω nnreal) :

filter.tendsto (λ (i : γ), (μs i).normalize.to_finite_measure.test_against_nn f) F (nhds (μ.normalize.to_finite_measure.test_against_nn f))

theorem measure_theory.finite_measure.tendsto_of_tendsto_normalize_test_against_nn_of_tendsto_mass {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} {μ : measure_theory.finite_measure Ω} [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure Ω} (μs_lim : filter.tendsto (λ (i : γ), (μs i).normalize) F (nhds μ.normalize)) (mass_lim : filter.tendsto (λ (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 measure_theory.finite_measure.tendsto_normalize_of_tendsto {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} {μ : measure_theory.finite_measure Ω} [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure Ω} (μs_lim : filter.tendsto μs F (nhds μ)) (nonzero : μ ≠ 0) :

filter.tendsto (λ (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 measure_theory.finite_measure.tendsto_normalize_iff_tendsto {Ω : Type u_1} [nonempty Ω] {m0 : measurable_space Ω} {μ : measure_theory.finite_measure Ω} [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure Ω} (nonzero : μ ≠ 0) :

filter.tendsto (λ (i : γ), (μs i).normalize) F (nhds μ.normalize) ∧ filter.tendsto (λ (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.