Finite measures #
This file defines the type of finite 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 finite measures is equipped with the topology of weak convergence
of measures. The topology of weak convergence is the coarsest topology w.r.t. which
for every bounded continuous ℝ≥0
-valued function f
, the integration of f
against the
measure is continuous.
Main definitions #
The main definitions are
MeasureTheory.FiniteMeasure Ω
: The type of finite measures onΩ
with the topology of weak convergence of measures.MeasureTheory.FiniteMeasure.toWeakDualBCNN : FiniteMeasure Ω → (WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0))
: Interpret a finite measure as a continuous linear functional on the space of bounded continuous nonnegative functions onΩ
. This is used for the definition of the topology of weak convergence.MeasureTheory.FiniteMeasure.map
: The push-forwardf* μ
of a finite measureμ
onΩ
along a measurable functionf : Ω → Ω'
.MeasureTheory.FiniteMeasure.mapCLM
: The push-forward along a given continuousf : Ω → Ω'
as a continuous linear mapf* : FiniteMeasure Ω →L[ℝ≥0] FiniteMeasure Ω'
.
Main results #
- Finite measures
μ
onΩ
give rise to continuous linear functionals on the space of bounded continuous nonnegative functions onΩ
via integration:MeasureTheory.FiniteMeasure.toWeakDualBCNN : FiniteMeasure Ω → (WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0))
MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto
: Convergence of finite measures is characterized by the convergence of integrals of all bounded continuous functions. This shows that the chosen definition of topology coincides with the common textbook definition of weak convergence of measures. A similar characterization by the convergence of integrals (in theMeasureTheory.lintegral
sense) of all bounded continuous nonnegative functions isMeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto
.MeasureTheory.FiniteMeasure.continuous_map
: For a continuous functionf : Ω → Ω'
, the push-forward of finite measuresf* : FiniteMeasure Ω → FiniteMeasure Ω'
is continuous.MeasureTheory.FiniteMeasure.t2Space
: The topology of weak convergence of finite Borel measures is Hausdorff on spaces where indicators of closed sets have continuous decreasing approximating sequences (in particular on any pseudo-metrizable spaces).
Implementation notes #
The topology of weak convergence of finite Borel measures is defined using a mapping from
MeasureTheory.FiniteMeasure Ω
to WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)
, inheriting the topology from the
latter.
The implementation of MeasureTheory.FiniteMeasure Ω
and 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 Ω
. Another alternative would have been to
use a bijection with MeasureTheory.VectorMeasure Ω ℝ≥0
as an intermediate step. Some
considerations:
- Potential advantages of using the
NNReal
-valued vector measure alternative:- The coercion to function would avoid need to compose with
ENNReal.toNNReal
, theNNReal
-valued API could be more directly available.
- The coercion to function would avoid need to compose with
- Potential drawbacks of the vector measure alternative:
- The coercion to function would lose monotonicity, as non-measurable sets would be defined to have measure 0.
- No integration theory directly. E.g., the topology definition requires
MeasureTheory.lintegral
w.r.t. a coercion toMeasureTheory.Measure Ω
in any case.
References #
Tags #
weak convergence of measures, finite measure
Finite measures #
In this section we define the Type
of MeasureTheory.FiniteMeasure Ω
, when Ω
is a measurable
space. Finite measures on Ω
are a module over ℝ≥0
.
If Ω
is moreover a topological space and the sigma algebra on Ω
is finer than the Borel sigma
algebra (i.e. [OpensMeasurableSpace Ω]
), then MeasureTheory.FiniteMeasure Ω
is equipped with
the topology of weak convergence of measures. This is implemented by defining a pairing of finite
measures μ
on Ω
with continuous bounded nonnegative functions f : Ω →ᵇ ℝ≥0
via integration,
and using the associated weak topology (essentially the weak-star topology on the dual of
Ω →ᵇ ℝ≥0
).
Finite measures are defined as the subtype of measures that have the property of being finite measures (i.e., their total mass is finite).
Equations
- MeasureTheory.FiniteMeasure Ω = { μ : MeasureTheory.Measure Ω // MeasureTheory.IsFiniteMeasure μ }
Instances For
Coercion from MeasureTheory.FiniteMeasure Ω
to MeasureTheory.Measure Ω
.
Equations
- MeasureTheory.FiniteMeasure.toMeasure = Subtype.val
Instances For
A finite measure can be interpreted as a measure.
Equations
- MeasureTheory.FiniteMeasure.instCoe = { coe := MeasureTheory.FiniteMeasure.toMeasure }
Equations
- ⋯ = ⋯
Equations
- MeasureTheory.FiniteMeasure.instFunLike = { coe := fun (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) => (↑μ s).toNNReal, coe_injective' := ⋯ }
The (total) mass of a finite measure μ
is μ univ
, i.e., the cast to NNReal
of
(μ : measure Ω) univ
.
Equations
- μ.mass = μ Set.univ
Instances For
Equations
- MeasureTheory.FiniteMeasure.instZero = { zero := ⟨0, ⋯⟩ }
Equations
- MeasureTheory.FiniteMeasure.instInhabited = { default := 0 }
Equations
- MeasureTheory.FiniteMeasure.instAdd = { add := fun (μ ν : MeasureTheory.FiniteMeasure Ω) => ⟨↑μ + ↑ν, ⋯⟩ }
Equations
- MeasureTheory.FiniteMeasure.instSMul = { smul := fun (c : R) (μ : MeasureTheory.FiniteMeasure Ω) => ⟨c • ↑μ, ⋯⟩ }
Equations
- MeasureTheory.FiniteMeasure.instAddCommMonoid = Function.Injective.addCommMonoid MeasureTheory.FiniteMeasure.toMeasure ⋯ ⋯ ⋯ ⋯
Coercion is an AddMonoidHom
.
Equations
- MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom = { toFun := MeasureTheory.FiniteMeasure.toMeasure, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- MeasureTheory.FiniteMeasure.instModuleNNReal = Function.Injective.module NNReal MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom ⋯ ⋯
Restrict a finite measure μ to a set A.
Equations
- μ.restrict A = ⟨(↑μ).restrict A, ⋯⟩
Instances For
Two finite Borel measures are equal if the integrals of all bounded continuous functions with respect to both agree.
The pairing of a finite (Borel) measure μ
with a nonnegative bounded continuous
function is obtained by (Lebesgue) integrating the (test) function against the measure.
This is MeasureTheory.FiniteMeasure.testAgainstNN
.
Equations
- μ.testAgainstNN f = (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ).toNNReal
Instances For
Finite measures yield elements of the WeakDual
of bounded continuous nonnegative
functions via MeasureTheory.FiniteMeasure.testAgainstNN
, i.e., integration.
Equations
- μ.toWeakDualBCNN = { toFun := fun (f : BoundedContinuousFunction Ω NNReal) => μ.testAgainstNN f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
The topology of weak convergence on MeasureTheory.FiniteMeasure Ω
is inherited (induced)
from the weak-* topology on WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)
via the function
MeasureTheory.FiniteMeasure.toWeakDualBCNN
.
Equations
- MeasureTheory.FiniteMeasure.instTopologicalSpace = TopologicalSpace.induced MeasureTheory.FiniteMeasure.toWeakDualBCNN inferInstance
Integration of (nonnegative bounded continuous) test functions against finite Borel measures depends continuously on the measure.
The total mass of a finite measure depends continuously on the measure.
Convergence of finite measures implies the convergence of their total masses.
If the total masses of finite measures tend to zero, then the measures tend to
zero. This formulation concerns the associated functionals on bounded continuous
nonnegative test functions. See MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass
for
a formulation stating the weak convergence of measures.
If the total masses of finite measures tend to zero, then the measures tend to zero.
A characterization of weak convergence in terms of integrals of bounded continuous nonnegative functions.
The mapping toWeakDualBCNN
from finite Borel measures to the weak dual of Ω →ᵇ ℝ≥0
is
injective, if in the underlying space Ω
, indicator functions of closed sets have decreasing
approximations by sequences of continuous functions (in particular if Ω
is pseudometrizable).
On topological spaces where indicators of closed sets have decreasing approximating sequences of
continuous functions (HasOuterApproxClosed
), the topology of weak convergence of finite Borel
measures is Hausdorff (T2Space
).
Equations
- ⋯ = ⋯
Bounded convergence results for finite measures #
This section is about bounded convergence theorems for finite measures.
A bounded convergence theorem for a finite measure:
If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant
and tend pointwise to a limit, then their integrals (MeasureTheory.lintegral
) against the finite
measure tend to the integral of the limit.
A related result with more general assumptions is
MeasureTheory.tendsto_lintegral_nn_filter_of_le_const
.
A bounded convergence theorem for a finite measure: If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a limit, then their integrals against the finite measure tend to the integral of the limit. This formulation assumes:
- the functions tend to a limit along a countably generated filter;
- the limit is in the almost everywhere sense;
- boundedness holds almost everywhere;
- integration is the pairing against non-negative continuous test functions
(
MeasureTheory.FiniteMeasure.testAgainstNN
).
A related result using MeasureTheory.lintegral
for integration is
MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const
.
A bounded convergence theorem for a finite measure:
If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and
tend pointwise to a limit, then their integrals (MeasureTheory.FiniteMeasure.testAgainstNN
)
against the finite measure tend to the integral of the limit.
Related results:
MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const
: more general assumptionsMeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const
: usingMeasureTheory.lintegral
for integration.
Weak convergence of finite measures with bounded continuous real-valued functions #
In this section we characterize the weak convergence of finite measures by the usual (defining) condition that the integrals of all bounded continuous real-valued functions converge.
A characterization of weak convergence in terms of integrals of bounded continuous real-valued functions.
The push-forward of a finite measure by a function between measurable spaces.
Equations
- ν.map f = ⟨MeasureTheory.Measure.map f ↑ν, ⋯⟩
Instances For
Note that this is an equality of elements of ℝ≥0∞
. See also
MeasureTheory.FiniteMeasure.map_apply
for the corresponding equality as elements of ℝ≥0
.
The push-forward of a finite measure by a function between measurable spaces as a linear map.
Equations
- MeasureTheory.FiniteMeasure.mapHom f_mble = { toFun := fun (ν : MeasureTheory.FiniteMeasure Ω) => ν.map f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
If f : X → Y
is continuous and Y
is equipped with the Borel sigma algebra, then
(weak) convergence of FiniteMeasure
s on X
implies (weak) convergence of the push-forwards
of these measures by f
.
If f : X → Y
is continuous and Y
is equipped with the Borel sigma algebra, then
the push-forward of finite measures f* : FiniteMeasure X → FiniteMeasure Y
is continuous
(in the topologies of weak convergence of measures).
The push-forward of a finite measure by a continuous function between Borel spaces as a continuous linear map.
Equations
- MeasureTheory.FiniteMeasure.mapCLM f_cont = { toFun := fun (ν : MeasureTheory.FiniteMeasure Ω) => ν.map f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }