Weak convergence of Radon measures

This file defines the three conditions for weak convergence of Radon measures appearing in Evans--Gariepy, Revised Edition, Theorem 1.40, and proves their equivalence for Radon measures on Euclidean space.

Radon measures are modelled here by Borel measures (MeasurableSpace X together with BorelSpace X) that are regular in Mathlib's sense, i.e. satisfy MeasureTheory.Measure.Regular: they are finite on compact sets, outer regular by open sets and inner regular by compact sets on open sets.

def MeasureTheory.Measure.WeaklyConverges {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (μ : ℕ → Measure X) (ν : Measure X) : Prop

A sequence of Radon measures μ converges weakly to a Radon measure ν if integrals against every real-valued compactly supported continuous function converge.

This is called weak convergence by Evans--Gariepy and is also commonly called vague convergence.

Equations

• MeasureTheory.Measure.WeaklyConverges μ ν = ∀ (f : CompactlySupportedContinuousMap X ℝ), Filter.Tendsto (fun (k : ℕ) => ∫ (x : X), f x ∂μ k) Filter.atTop (nhds (∫ (x : X), f x ∂ν))

def MeasureTheory.Measure.WeaklyConvergesByCompactOpenBounds {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (μ : ℕ → Measure X) (ν : Measure X) : Prop

Evans--Gariepy, Revised Edition, Theorem 1.40(ii): the compact-set upper bound and open-set lower bound characterizing weak convergence.

Both clauses together constitute condition (ii); neither clause separately is equivalent to weak convergence.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.Measure.WeaklyConvergesOnBoundedContinuitySets {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [Bornology X] (μ : ℕ → Measure X) (ν : Measure X) : Prop

Evans--Gariepy, Revised Edition, Theorem 1.40(iii): convergence on every bounded Borel continuity set of the limit measure.

Under BorelSpace X, MeasurableSet B says that B is Borel. For Euclidean space, Bornology.IsBounded B is the usual metric boundedness condition.

Equations

• One or more equations did not get rendered due to their size.

Equivalence on Euclidean space

theorem MeasureTheory.Measure.weaklyConverges_iff_compactOpenBounds {n : ℕ} (μ : ℕ → Measure (EuclideanSpace ℝ (Fin n))) (ν : Measure (EuclideanSpace ℝ (Fin n))) (hμ : ∀ (k : ℕ), (μ k).Regular) (hν : ν.Regular) : WeaklyConverges μ ν ↔ WeaklyConvergesByCompactOpenBounds μ ν

Evans--Gariepy, Revised Edition, Theorem 1.40, equivalence of conditions (i) and (ii) for Radon measures on Euclidean space.

theorem MeasureTheory.Measure.weaklyConvergesByCompactOpenBounds_iff_boundedContinuitySets {n : ℕ} (μ : ℕ → Measure (EuclideanSpace ℝ (Fin n))) (ν : Measure (EuclideanSpace ℝ (Fin n))) (hν : ν.Regular) : WeaklyConvergesByCompactOpenBounds μ ν ↔ WeaklyConvergesOnBoundedContinuitySets μ ν

Evans--Gariepy, Revised Edition, Theorem 1.40, equivalence of conditions (ii) and (iii) for Radon measures on Euclidean space.

theorem MeasureTheory.Measure.weaklyConverges_iff_boundedContinuitySets {n : ℕ} (μ : ℕ → Measure (EuclideanSpace ℝ (Fin n))) (ν : Measure (EuclideanSpace ℝ (Fin n))) (hμ : ∀ (k : ℕ), (μ k).Regular) (hν : ν.Regular) : WeaklyConverges μ ν ↔ WeaklyConvergesOnBoundedContinuitySets μ ν

Evans--Gariepy, Revised Edition, Theorem 1.40, equivalence of conditions (i) and (iii) for Radon measures on Euclidean space.