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
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.lintegralsense) of all bounded continuous nonnegative random variables is
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.
- 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.finite_measure Ω, the implementation of
is directly as a subtype of
measure_theory.measure Ω, and the coercion to a function is the
ennreal.to_nnreal and the coercion to function of
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
Ω is moreover a topological space and the sigma algebra on
Ω is finer than the Borel sigma
[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
Probability measures are defined as the subtype of measures that have the property of being probability measures (i.e., their total mass is one).
A probability measure can be interpreted as a 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
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.
Averaging with respect to a finite measure is the same as integraing against
If the normalized versions of finite measures converge weakly and their total masses also converge, then the finite measures themselves converge weakly.
If finite measures themselves converge weakly to a nonzero limit measure, then their normalized versions also converge weakly.
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.