Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_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 Ω} [CompactSpace Ω],
  Continuous μs ↔ ∀ (f : C(Ω, ℝ)), 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

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceTopologicalSpaceCompactSpace