Theorems · Theorem · measure theory

MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae

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

If f is a sequence of functions which converges in measure to g, then there exists a subsequence of f which converges a.e. to g.

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Cited by

5 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace