Convergence in measure

AbbreviationMeasurable functions representing \(L^0((0,1))\)#✓fully proved

The type of Borel measurable functions \(f : \mathbb{R} \to \mathbb{R}\), used as representatives of the elements of \(L^0([0,1])\).

The pseudometric and the convergence in measure built on them depend only on the restriction of \(f\) to \([0,1]\) up to a null set.

abbrev L0UnitInterval : Type := {f : ℝ → ℝ // Measurable f}

Used by 2

Used byThe \(L^0\) pseudometric on \((0,1)\) · Convergence in the \(L^0\) pseudometric is convergence in measure

DefinitionThe \(L^0\) pseudometric on \((0,1)\)#✓fully proved

For Borel measurable functions \(f, g : \mathbb{R} \to \mathbb{R}\),

\[ d(f,g) = \int_{[0,1]} \frac{|f(x) - g(x)|}{1 + |f(x) - g(x)|}\,dx, \]

the integral being with respect to Lebesgue measure on \([0,1]\).

This is a pseudometric: functions that agree almost everywhere on \([0,1]\) are at distance \(0\), and on the almost-everywhere classes it is the usual metric of \(L^0([0,1])\).

noncomputable def L0PseudoMetric (f g : L0UnitInterval) : ℝ :=
  ∫ x, |f.1 x - g.1 x| / (1 + |f.1 x - g.1 x|)
    ∂(MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))

Uses 1 · Used by 1

Statement usesMeasurable functions representing \(L^0((0,1))\)

Used byConvergence in the \(L^0\) pseudometric is convergence in measure

TheoremConvergence in the \(L^0\) pseudometric is convergence in measure#●ready to prove

Let \(f\) and \(f_0, f_1, f_2, \ldots\) be Borel measurable functions \(\mathbb{R} \to \mathbb{R}\), and let \(d\) be the pseudometric

\[ d(g,h) = \int_{[0,1]} \frac{|g(x) - h(x)|}{1 + |g(x) - h(x)|}\,dx \]

on such functions, the integral being with respect to Lebesgue measure. Then \(d(f_n, f) \to 0\) as \(n \to \infty\) if and only if \(f_n \to f\) in measure with respect to Lebesgue measure on \([0,1]\): for every \(\varepsilon > 0\), the Lebesgue measure of \(\{x \in [0,1] : |f_n(x) - f(x)| \ge \varepsilon\}\) tends to \(0\) as \(n \to \infty\).

The source states this for \(L^0([0,1])\), on which \(d\) is a metric; here it is stated for representatives, on which \(d\) is only a pseudometric. Both sides depend only on the almost-everywhere classes of the functions on \([0,1]\), so the two statements say the same thing.

public theorem_wanted tendsto_L0PseudoMetric_zero_iff_tendstoInMeasure
    (fSeq : ℕ → L0UnitInterval) (f : L0UnitInterval) :
    Filter.Tendsto (fun n => L0PseudoMetric (fSeq n) f) Filter.atTop (𝓝 (0 : ℝ)) ↔
      MeasureTheory.TendstoInMeasure
        (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1))
        (fun n x => (fSeq n).1 x) Filter.atTop (fun x => f.1 x)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Linear function spaces and their duals), problem ma_proofbench_l2_07, with the change above.

Uses 2

Statement usesThe \(L^0\) pseudometric on \((0,1)\) · Measurable functions representing \(L^0((0,1))\)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.