Theorems · Definition · measure theory

MeasureTheory.TendstoInMeasure

{α : Type u_1} →
  {ι : Type u_2} →
    {E : Type u_4} →
      [EDist E] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (ι → α → E) → Filter ι → (α → E) → Prop

A sequence of functions f is said to converge in measure to some function g if for all ε > 0, the measure of the set {x | ε ≤ dist (f i x) (g x)} tends to 0 as i converges along some given filter l.

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Cited by

51 results in Mathlib

Foundations

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

Assumes

EDist