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

Main results #

TODO:

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 #

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.

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
Instances for measure_theory.probability_measure

A probability measure can be interpreted as a finite measure.

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

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.

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.

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

Equations
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

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

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.