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-forward f* μ of a finite measure μ on Ω along a measurable function f : Ω → Ω'.
• MeasureTheory.FiniteMeasure.mapCLM: The push-forward along a given continuous f : Ω → Ω' as a continuous linear map f* : 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 the MeasureTheory.lintegral sense) of all bounded continuous nonnegative functions is MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto.
• MeasureTheory.FiniteMeasure.continuous_map: For a continuous function f : Ω → Ω', the push-forward of finite measures f* : 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, the NNReal-valued API could be more directly available.
• 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 to MeasureTheory.Measure Ω in any case.

References

• [Billingsley, Convergence of probability measures][billingsley1999]

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).

def MeasureTheory.FiniteMeasure (Ω : Type u_2) [MeasurableSpace Ω] : Type u_2

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 μ }

def MeasureTheory.FiniteMeasure.toMeasure {Ω : Type u_1} [MeasurableSpace Ω] : MeasureTheory.FiniteMeasure Ω → MeasureTheory.Measure Ω

Coercion from MeasureTheory.FiniteMeasure Ω to MeasureTheory.Measure Ω.

Equations

• MeasureTheory.FiniteMeasure.toMeasure = Subtype.val

instance MeasureTheory.FiniteMeasure.instCoe {Ω : Type u_1} [MeasurableSpace Ω] : Coe (MeasureTheory.FiniteMeasure Ω) (MeasureTheory.Measure Ω)

A finite measure can be interpreted as a measure.

Equations

• MeasureTheory.FiniteMeasure.instCoe = { coe := MeasureTheory.FiniteMeasure.toMeasure }

instance MeasureTheory.FiniteMeasure.isFiniteMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : MeasureTheory.IsFiniteMeasure ↑μ

Equations

• ⋯ = ⋯

instance MeasureTheory.FiniteMeasure.instCoeFun {Ω : Type u_1} [MeasurableSpace Ω] : CoeFun (MeasureTheory.FiniteMeasure Ω) fun (x : MeasureTheory.FiniteMeasure Ω) => Set Ω → NNReal

Equations

• MeasureTheory.FiniteMeasure.instCoeFun = { coe := fun (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) => (↑↑↑μ s).toNNReal }

@[simp]

theorem MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) : ↑((fun (s : Set Ω) => (↑↑↑ν s).toNNReal) s) = ↑↑↑ν s

@[simp]

theorem MeasureTheory.FiniteMeasure.val_eq_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.FiniteMeasure Ω) : ↑ν = ↑ν

theorem MeasureTheory.FiniteMeasure.toMeasure_injective {Ω : Type u_1} [MeasurableSpace Ω] : Function.Injective MeasureTheory.FiniteMeasure.toMeasure

theorem MeasureTheory.FiniteMeasure.apply_mono {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {s₁ : Set Ω} {s₂ : Set Ω} (h : s₁ ⊆ s₂) : (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) s₁ ≤ (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) s₂

def MeasureTheory.FiniteMeasure.mass {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : NNReal

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

Equations

• μ.mass = (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) Set.univ

@[simp]

theorem MeasureTheory.FiniteMeasure.apply_le_mass {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) : (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) s ≤ μ.mass

@[simp]

theorem MeasureTheory.FiniteMeasure.ennreal_mass {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} : ↑μ.mass = ↑↑↑μ Set.univ

instance MeasureTheory.FiniteMeasure.instZero {Ω : Type u_1} [MeasurableSpace Ω] : Zero (MeasureTheory.FiniteMeasure Ω)

Equations

• MeasureTheory.FiniteMeasure.instZero = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem MeasureTheory.FiniteMeasure.zero_mass {Ω : Type u_1} [MeasurableSpace Ω] : MeasureTheory.FiniteMeasure.mass 0 = 0

@[simp]

theorem MeasureTheory.FiniteMeasure.mass_zero_iff {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : μ.mass = 0 ↔ μ = 0

theorem MeasureTheory.FiniteMeasure.mass_nonzero_iff {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : μ.mass ≠ 0 ↔ μ ≠ 0

theorem MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) (h : ∀ (s : Set Ω), MeasurableSet s → ↑↑↑μ s = ↑↑↑ν s) : μ = ν

theorem MeasureTheory.FiniteMeasure.eq_of_forall_apply_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) (h : ∀ (s : Set Ω), MeasurableSet s → (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) s = (fun (s : Set Ω) => (↑↑↑ν s).toNNReal) s) : μ = ν

instance MeasureTheory.FiniteMeasure.instInhabited {Ω : Type u_1} [MeasurableSpace Ω] : Inhabited (MeasureTheory.FiniteMeasure Ω)

Equations

• MeasureTheory.FiniteMeasure.instInhabited = { default := 0 }

instance MeasureTheory.FiniteMeasure.instAdd {Ω : Type u_1} [MeasurableSpace Ω] : Add (MeasureTheory.FiniteMeasure Ω)

Equations

• MeasureTheory.FiniteMeasure.instAdd = { add := fun (μ ν : MeasureTheory.FiniteMeasure Ω) => ⟨↑μ + ↑ν, ⋯⟩ }

instance MeasureTheory.FiniteMeasure.instSMul {Ω : Type u_1} [MeasurableSpace Ω] {R : Type u_2} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] : SMul R (MeasureTheory.FiniteMeasure Ω)

Equations

• MeasureTheory.FiniteMeasure.instSMul = { smul := fun (c : R) (μ : MeasureTheory.FiniteMeasure Ω) => ⟨c • ↑μ, ⋯⟩ }

theorem MeasureTheory.FiniteMeasure.toMeasure_zero {Ω : Type u_1} [MeasurableSpace Ω] : ↑0 = 0

theorem MeasureTheory.FiniteMeasure.toMeasure_add {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) : ↑(μ + ν) = ↑μ + ↑ν

theorem MeasureTheory.FiniteMeasure.toMeasure_smul {Ω : Type u_1} [MeasurableSpace Ω] {R : Type u_2} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (μ : MeasureTheory.FiniteMeasure Ω) : ↑(c • μ) = c • ↑μ

@[simp]

theorem MeasureTheory.FiniteMeasure.coeFn_zero {Ω : Type u_1} [MeasurableSpace Ω] : (fun (s : Set Ω) => (↑↑↑0 s).toNNReal) = 0

@[simp]

theorem MeasureTheory.FiniteMeasure.coeFn_add {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) : (fun (s : Set Ω) => (↑↑↑(μ + ν) s).toNNReal) = (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) + fun (s : Set Ω) => (↑↑↑ν s).toNNReal

@[simp]

theorem MeasureTheory.FiniteMeasure.coeFn_smul {Ω : Type u_1} [MeasurableSpace Ω] {R : Type u_2} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal] (c : R) (μ : MeasureTheory.FiniteMeasure Ω) : (fun (s : Set Ω) => (↑↑↑(c • μ) s).toNNReal) = c • fun (s : Set Ω) => (↑↑↑μ s).toNNReal

instance MeasureTheory.FiniteMeasure.instAddCommMonoid {Ω : Type u_1} [MeasurableSpace Ω] : AddCommMonoid (MeasureTheory.FiniteMeasure Ω)

Equations

• MeasureTheory.FiniteMeasure.instAddCommMonoid = Function.Injective.addCommMonoid MeasureTheory.FiniteMeasure.toMeasure ⋯ ⋯ ⋯ ⋯

@[simp]

theorem MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom_apply {Ω : Type u_1} [MeasurableSpace Ω] : ∀ (a : MeasureTheory.FiniteMeasure Ω), MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom a = ↑a

def MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom {Ω : Type u_1} [MeasurableSpace Ω] : MeasureTheory.FiniteMeasure Ω →+ MeasureTheory.Measure Ω

Coercion is an AddMonoidHom.

Equations

• MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom = { toFun := MeasureTheory.FiniteMeasure.toMeasure, map_zero' := ⋯, map_add' := ⋯ }

instance MeasureTheory.FiniteMeasure.instModuleNNReal {Ω : Type u_3} [MeasurableSpace Ω] : Module NNReal (MeasureTheory.FiniteMeasure Ω)

Equations

• MeasureTheory.FiniteMeasure.instModuleNNReal = Function.Injective.module NNReal MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom ⋯ ⋯

theorem MeasureTheory.FiniteMeasure.coeFn_smul_apply {Ω : Type u_1} [MeasurableSpace Ω] {R : Type u_2} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal] (c : R) (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) : (fun (s : Set Ω) => (↑↑↑(c • μ) s).toNNReal) s = c • (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) s

def MeasureTheory.FiniteMeasure.restrict {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) : MeasureTheory.FiniteMeasure Ω

Restrict a finite measure μ to a set A.

Equations

• μ.restrict A = ⟨(↑μ).restrict A, ⋯⟩

theorem MeasureTheory.FiniteMeasure.restrict_measure_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) : ↑(μ.restrict A) = (↑μ).restrict A

theorem MeasureTheory.FiniteMeasure.restrict_apply_measure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble : MeasurableSet s) : ↑↑↑(μ.restrict A) s = ↑↑↑μ (s ∩ A)

theorem MeasureTheory.FiniteMeasure.restrict_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble : MeasurableSet s) : (fun (s : Set Ω) => (↑↑↑(μ.restrict A) s).toNNReal) s = (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) (s ∩ A)

theorem MeasureTheory.FiniteMeasure.restrict_mass {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) : (μ.restrict A).mass = (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) A

theorem MeasureTheory.FiniteMeasure.restrict_eq_zero_iff {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) : μ.restrict A = 0 ↔ (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) A = 0

theorem MeasureTheory.FiniteMeasure.restrict_nonzero_iff {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) : μ.restrict A ≠ 0 ↔ (fun (s : Set Ω) => (↑↑↑μ s).toNNReal) A ≠ 0

theorem MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {ν : MeasureTheory.FiniteMeasure Ω} (h : ∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν) : μ = ν

Two finite Borel measures are equal if the integrals of all bounded continuous functions with respect to both agree.

def MeasureTheory.FiniteMeasure.testAgainstNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) : NNReal

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

@[simp]

theorem MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {f : BoundedContinuousFunction Ω NNReal} : ↑(μ.testAgainstNN f) = ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ

theorem MeasureTheory.FiniteMeasure.testAgainstNN_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (c : NNReal) : μ.testAgainstNN (BoundedContinuousFunction.const Ω c) = c * μ.mass

theorem MeasureTheory.FiniteMeasure.testAgainstNN_mono {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {f : BoundedContinuousFunction Ω NNReal} {g : BoundedContinuousFunction Ω NNReal} (f_le_g : ⇑f ≤ ⇑g) : μ.testAgainstNN f ≤ μ.testAgainstNN g

@[simp]

theorem MeasureTheory.FiniteMeasure.testAgainstNN_zero {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : μ.testAgainstNN 0 = 0

@[simp]

theorem MeasureTheory.FiniteMeasure.testAgainstNN_one {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : μ.testAgainstNN 1 = μ.mass

@[simp]

theorem MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (f : BoundedContinuousFunction Ω NNReal) : MeasureTheory.FiniteMeasure.testAgainstNN 0 f = 0

theorem MeasureTheory.FiniteMeasure.zero_testAgainstNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] : MeasureTheory.FiniteMeasure.testAgainstNN 0 = 0

@[simp]

theorem MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (c : NNReal) (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) : (c • μ).testAgainstNN f = c • μ.testAgainstNN f

theorem MeasureTheory.FiniteMeasure.testAgainstNN_add {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (f₁ : BoundedContinuousFunction Ω NNReal) (f₂ : BoundedContinuousFunction Ω NNReal) : μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂

theorem MeasureTheory.FiniteMeasure.testAgainstNN_smul {Ω : Type u_1} [MeasurableSpace Ω] {R : Type u_2} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [IsScalarTower R NNReal NNReal] [PseudoMetricSpace R] [Zero R] [BoundedSMul R NNReal] (μ : MeasureTheory.FiniteMeasure Ω) (c : R) (f : BoundedContinuousFunction Ω NNReal) : μ.testAgainstNN (c • f) = c • μ.testAgainstNN f

theorem MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) (g : BoundedContinuousFunction Ω NNReal) : μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass

theorem MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : LipschitzWith μ.mass fun (f : BoundedContinuousFunction Ω NNReal) => μ.testAgainstNN f

def MeasureTheory.FiniteMeasure.toWeakDualBCNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : WeakDual NNReal (BoundedContinuousFunction Ω NNReal)

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 := ⋯ }

@[simp]

theorem MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) : ⇑μ.toWeakDualBCNN = μ.testAgainstNN

@[simp]

theorem MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) : μ.toWeakDualBCNN f = (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toNNReal

instance MeasureTheory.FiniteMeasure.instTopologicalSpace {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : TopologicalSpace (MeasureTheory.FiniteMeasure Ω)

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

theorem MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : Continuous MeasureTheory.FiniteMeasure.toWeakDualBCNN

theorem MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (f : BoundedContinuousFunction Ω NNReal) : Continuous fun (μ : MeasureTheory.FiniteMeasure Ω) => μ.testAgainstNN f

Integration of (nonnegative bounded continuous) test functions against finite Borel measures depends continuously on the measure.

theorem MeasureTheory.FiniteMeasure.continuous_mass {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : Continuous fun (μ : MeasureTheory.FiniteMeasure Ω) => μ.mass

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

theorem Filter.Tendsto.mass {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (h : Filter.Tendsto μs F (nhds μ)) : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds μ.mass)

Convergence of finite measures implies the convergence of their total masses.

theorem MeasureTheory.FiniteMeasure.tendsto_iff_weak_star_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} : Filter.Tendsto μs F (nhds μ) ↔ Filter.Tendsto (fun (i : γ) => (μs i).toWeakDualBCNN) F (nhds μ.toWeakDualBCNN)

theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} : Filter.Tendsto μs F (nhds μ) ↔ ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun (i : γ) => (μs i).toWeakDualBCNN f) F (nhds (μ.toWeakDualBCNN f))

theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} : Filter.Tendsto μs F (nhds μ) ↔ ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun (i : γ) => (μs i).testAgainstNN f) F (nhds (μ.testAgainstNN f))

theorem MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds 0)) (f : BoundedContinuousFunction Ω NNReal) : Filter.Tendsto (fun (i : γ) => (μs i).testAgainstNN f) F (nhds 0)

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.

theorem MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds 0)) : Filter.Tendsto μs F (nhds 0)

If the total masses of finite measures tend to zero, then the measures tend to zero.

theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} : Filter.Tendsto μs F (nhds μ) ↔ ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun (i : γ) => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (nhds (∫⁻ (x : Ω), ↑(f x) ∂↑μ))

A characterization of weak convergence in terms of integrals of bounded continuous nonnegative functions.

theorem MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] : Function.Injective MeasureTheory.FiniteMeasure.toWeakDualBCNN

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).

theorem MeasureTheory.FiniteMeasure.embedding_toWeakDualBCNN (Ω : Type u_1) [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] : Embedding MeasureTheory.FiniteMeasure.toWeakDualBCNN

instance MeasureTheory.FiniteMeasure.t2Space (Ω : Type u_1) [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] : T2Space (MeasureTheory.FiniteMeasure Ω)

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.

theorem MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) {f : Ω → NNReal} (fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun (n : ℕ) => (fs n) ω) Filter.atTop (nhds (f ω))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) Filter.atTop (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 (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.

theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [L.IsCountablyGenerated] {μ : MeasureTheory.FiniteMeasure Ω} {fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c) {f : BoundedContinuousFunction Ω NNReal} (fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Filter.Tendsto (fun (i : ι) => (fs i) ω) L (nhds (f ω))) : Filter.Tendsto (fun (i : ι) => μ.testAgainstNN (fs i)) L (nhds (μ.testAgainstNN 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 (MeasureTheory.FiniteMeasure.testAgainstNN).

A related result using MeasureTheory.lintegral for integration is MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const.

theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) {f : BoundedContinuousFunction Ω NNReal} (fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun (n : ℕ) => (fs n) ω) Filter.atTop (nhds (f ω))) : Filter.Tendsto (fun (n : ℕ) => μ.testAgainstNN (fs n)) Filter.atTop (nhds (μ.testAgainstNN 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 (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 assumptions
• MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const: using MeasureTheory.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.

theorem MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (h : ∀ (f : BoundedContinuousFunction Ω ℝ), Filter.Tendsto (fun (i : γ) => ∫ (x : Ω), f x ∂↑(μs i)) F (nhds (∫ (x : Ω), f x ∂↑μ))) : Filter.Tendsto μs F (nhds μ)

theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} : Filter.Tendsto μs F (nhds μ) ↔ ∀ (f : BoundedContinuousFunction Ω ℝ), Filter.Tendsto (fun (i : γ) => ∫ (x : Ω), f x ∂↑(μs i)) F (nhds (∫ (x : Ω), f x ∂↑μ))

A characterization of weak convergence in terms of integrals of bounded continuous real-valued functions.

noncomputable def MeasureTheory.FiniteMeasure.map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) (f : Ω → Ω') : MeasureTheory.FiniteMeasure Ω'

The push-forward of a finite measure by a function between measurable spaces.

Equations

• ν.map f = ⟨MeasureTheory.Measure.map f ↑ν, ⋯⟩

@[simp]

theorem MeasureTheory.FiniteMeasure.toMeasure_map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) (f : Ω → Ω') : ↑(ν.map f) = MeasureTheory.Measure.map f ↑ν

theorem MeasureTheory.FiniteMeasure.map_apply' {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'} (A_mble : MeasurableSet A) : ↑↑↑(ν.map f) A = ↑↑↑ν (f ⁻¹' A)

Note that this is an equality of elements of ℝ≥0∞. See also MeasureTheory.FiniteMeasure.map_apply for the corresponding equality as elements of ℝ≥0.

theorem MeasureTheory.FiniteMeasure.map_apply_of_aemeasurable {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'} (A_mble : MeasurableSet A) : (fun (s : Set Ω') => (↑↑↑(ν.map f) s).toNNReal) A = (fun (s : Set Ω) => (↑↑↑ν s).toNNReal) (f ⁻¹' A)

theorem MeasureTheory.FiniteMeasure.map_apply {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) {f : Ω → Ω'} (f_mble : Measurable f) {A : Set Ω'} (A_mble : MeasurableSet A) : (fun (s : Set Ω') => (↑↑↑(ν.map f) s).toNNReal) A = (fun (s : Set Ω) => (↑↑↑ν s).toNNReal) (f ⁻¹' A)

@[simp]

theorem MeasureTheory.FiniteMeasure.map_add {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {f : Ω → Ω'} (f_mble : Measurable f) (ν₁ : MeasureTheory.FiniteMeasure Ω) (ν₂ : MeasureTheory.FiniteMeasure Ω) : (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f

@[simp]

theorem MeasureTheory.FiniteMeasure.map_smul {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {f : Ω → Ω'} (c : NNReal) (ν : MeasureTheory.FiniteMeasure Ω) : (c • ν).map f = c • ν.map f

noncomputable def MeasureTheory.FiniteMeasure.mapHom {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {f : Ω → Ω'} (f_mble : Measurable f) : MeasureTheory.FiniteMeasure Ω →ₗ[NNReal] MeasureTheory.FiniteMeasure Ω'

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' := ⋯ }

theorem MeasureTheory.FiniteMeasure.tendsto_map_of_tendsto_of_continuous {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω'] {ι : Type u_3} {L : Filter ι} (νs : ι → MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) (lim : Filter.Tendsto νs L (nhds ν)) {f : Ω → Ω'} (f_cont : Continuous f) : Filter.Tendsto (fun (i : ι) => (νs i).map f) L (nhds (ν.map f))

If f : X → Y is continuous and Y is equipped with the Borel sigma algebra, then (weak) convergence of FiniteMeasures on X implies (weak) convergence of the push-forwards of these measures by f.

theorem MeasureTheory.FiniteMeasure.continuous_map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω'] {f : Ω → Ω'} (f_cont : Continuous f) : Continuous fun (ν : MeasureTheory.FiniteMeasure Ω) => ν.map 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).

noncomputable def MeasureTheory.FiniteMeasure.mapCLM {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω'] {f : Ω → Ω'} (f_cont : Continuous f) : MeasureTheory.FiniteMeasure Ω →L[NNReal] MeasureTheory.FiniteMeasure Ω'

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 := ⋯ }