Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_lintegral

∀ {Ω : 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 Ω NNReal), Continuous fun x => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)

The characterization of weak convergence of probability measures by the condition that the integrals of every continuous bounded nonnegative function are continuous.

Defined in

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceTopologicalSpace