Theorems · Theorem · measure theory

BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure X}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (f : BoundedContinuousFunction X ℝ), 0 ≤ f → Filter.limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ) →
    ∀ (f : BoundedContinuousFunction X ℝ), Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (nhds (∫ (x : X), f x ∂μ))

Defined in

Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure