Theorems · Theorem · measure theory

MeasureTheory.tendstoInMeasure_of_tendsto_ae

∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
      MeasureTheory.TendstoInMeasure μ f Filter.atTop g

Convergence a.e. implies convergence in measure in a finite measure space.

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Cited by

4 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceMeasureTheory.IsFiniteMeasure