mathlib3 documentation

measure_theory.measure.finite_measure

Finite measures #

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

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

Main results #

Implementation notes #

The topology of weak convergence of finite Borel measures is defined using a mapping from measure_theory.finite_measure Ω to weak_dual ℝ≥0 (Ω →ᵇ ℝ≥0), inheriting the topology from the latter.

The implementation of measure_theory.finite_measure Ω and 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 Ω. Another alternative would have been to use a bijection with measure_theory.vector_measure Ω ℝ≥0 as an intermediate step. Some considerations:

References #

Tags #

weak convergence of measures, finite measure

Finite measures #

In this section we define the Type of finite_measure Ω, 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. [opens_measurable_space Ω]), then finite_measure Ω 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).

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

The (total) mass of a finite measure μ is μ univ, i.e., the cast to nnreal of (μ : measure Ω) univ.

Equations
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]

Restrict a finite measure μ to a set A.

Equations
theorem measure_theory.finite_measure.restrict_apply {Ω : Type u_1} [measurable_space Ω] (μ : measure_theory.finite_measure Ω) (A : set Ω) {s : set Ω} (s_mble : measurable_set s) :
(μ.restrict A) s = μ (s A)

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 finite_measure.test_against_nn.

Equations

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

Equations

The total mass of a finite measure depends continuously on the measure.

theorem filter.tendsto.mass {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ measure_theory.finite_measure Ω} {μ : measure_theory.finite_measure Ω} (h : filter.tendsto μs F (nhds μ)) :
filter.tendsto (λ (i : γ), (μs i).mass) F (nhds μ.mass)

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 finite_measure.tendsto_zero_of_tendsto_zero_mass for a formulation stating the weak convergence of measures.

theorem measure_theory.finite_measure.tendsto_zero_of_tendsto_zero_mass {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] {γ : Type u_2} {F : filter γ} {μs : γ measure_theory.finite_measure Ω} (mass_lim : filter.tendsto (λ (i : γ), (μs i).mass) F (nhds 0)) :

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.

Bounded convergence results for finite measures #

This section is about bounded convergence theorems for finite measures.

theorem measure_theory.finite_measure.tendsto_lintegral_nn_filter_of_le_const {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] {ι : Type u_2} {L : filter ι} [L.is_countably_generated] (μ : measure_theory.measure Ω) [measure_theory.is_finite_measure μ] {fs : ι bounded_continuous_function Ω nnreal} {c : nnreal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) μ, (fs i) ω c) {f : Ω nnreal} (fs_lim : ∀ᵐ (ω : Ω) μ, filter.tendsto (λ (i : ι), (fs i) ω) L (nhds (f ω))) :
filter.tendsto (λ (i : ι), ∫⁻ (ω : Ω), ((fs i) ω) μ) L (nhds (∫⁻ (ω : Ω), (f ω) μ))

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 measure_theory.lintegral, i.e., the functions and their integrals are ℝ≥0∞-valued.
theorem measure_theory.finite_measure.tendsto_lintegral_nn_of_le_const {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] (μ : measure_theory.finite_measure Ω) {fs : bounded_continuous_function Ω nnreal} {c : nnreal} (fs_le_const : (n : ) (ω : Ω), (fs n) ω c) {f : Ω nnreal} (fs_lim : (ω : Ω), filter.tendsto (λ (n : ), (fs n) ω) filter.at_top (nhds (f ω))) :
filter.tendsto (λ (n : ), ∫⁻ (ω : Ω), ((fs n) ω) μ) filter.at_top (nhds (∫⁻ (ω : Ω), (f ω) μ))

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 (measure_theory.lintegral) against the finite measure tend to the integral of the limit.

A related result with more general assumptions is measure_theory.finite_measure.tendsto_lintegral_nn_filter_of_le_const.

theorem measure_theory.finite_measure.tendsto_test_against_nn_filter_of_le_const {Ω : Type u_1} [measurable_space Ω] [topological_space Ω] [opens_measurable_space Ω] {ι : Type u_2} {L : filter ι} [L.is_countably_generated] {μ : measure_theory.finite_measure Ω} {fs : ι bounded_continuous_function Ω nnreal} {c : nnreal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) μ, (fs i) ω c) {f : bounded_continuous_function Ω nnreal} (fs_lim : ∀ᵐ (ω : Ω) μ, filter.tendsto (λ (i : ι), (fs i) ω) L (nhds (f ω))) :
filter.tendsto (λ (i : ι), μ.test_against_nn (fs i)) L (nhds (μ.test_against_nn f))

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 (measure_theory.finite_measure.test_against_nn).

A related result using measure_theory.lintegral for integration is measure_theory.finite_measure.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 (measure_theory.finite_measure.test_against_nn) against the finite measure tend to the integral of the limit.

Related results:

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.