Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integral

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.ProbabilityMeasure Ω},
  Continuous μs ↔ ∀ (f : BoundedContinuousFunction Ω ℝ), Continuous fun x => ∫ (ω : Ω), f ω ∂↑(μs x)

The characterization of weak convergence of probability measures by the usual (defining) condition that the integrals of every continuous bounded function are continuous.

Defined in

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Cited by

2 results in Mathlib

Foundations

Depth 259 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceTopologicalSpace