Scheffé's lemma

TheoremScheffé's lemma#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(f_n : \alpha \to \mathbb{R}\) (\(n \in \mathbb{N}\)) be \(\mu\)-almost everywhere strongly measurable, and let \(g : \alpha \to \mathbb{R}\) be in \(L^1(\mu)\). Write \(\|h\|_1 = \int |h| \, d\mu \in [0, \infty]\) for the \(L^1\) seminorm. If \(f_n(x) \to g(x)\) for \(\mu\)-almost every \(x\) and \(\|f_n\|_1 \to \|g\|_1\) in \([0, \infty]\), then \(\|f_n - g\|_1 \to 0\), that is, \(f_n \to g\) in \(L^1(\mu)\).

theorem scheffe_lemma {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    {f : ℕ → α → ℝ} {g : α → ℝ}
    (hfm : ∀ n, AEStronglyMeasurable (f n) μ)
    (hg : MemLp g 1 μ)
    (hae : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)))
    (hnorm : Tendsto (fun n => eLpNorm (f n) 1 μ) atTop (𝓝 (eLpNorm g 1 μ))) :
    Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)

Used by 1

Used byScheffé's lemma for convergence in measure

TheoremScheffé's lemma for convergence in measure#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(f_n : \alpha \to \mathbb{R}\) (\(n \in \mathbb{N}\)) and \(g : \alpha \to \mathbb{R}\) be in \(L^1(\mu)\), and write \(\|h\|_1 = \int |h| \, d\mu\). If \(f_n \to g\) in \(\mu\)-measure (for every \(\varepsilon > 0\), \(\mu\{x : |f_n(x) - g(x)| \ge \varepsilon\} \to 0\)) and \(\|f_n\|_1 \to \|g\|_1\), then \(\|f_n - g\|_1 \to 0\), that is, \(f_n \to g\) in \(L^1(\mu)\).

The proof applies Scheffé's lemma along a further subsequence, extracted from every subsequence by convergence in measure.

theorem tendsto_eLpNorm_one_of_tendstoInMeasure_of_tendsto_eLpNorm
    {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    {f : ℕ → α → ℝ} {g : α → ℝ}
    (hf : ∀ n, MemLp (f n) 1 μ) (hg : MemLp g 1 μ)
    (hfg : TendstoInMeasure μ f atTop g)
    (hnorm : Tendsto (fun n => eLpNorm (f n) 1 μ) atTop (𝓝 (eLpNorm g 1 μ))) :
    Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)

Uses 1 · Used by 2

Proof usesScheffé's lemma

Used byConvergence in measure with converging L¹ norms implies uniform integrability · Uniform integrability equivalences

TheoremConvergence in measure with converging L¹ norms implies uniform integrability#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\alpha\), let \(f_n : \alpha \to \mathbb{R}\) (\(n \in \mathbb{N}\)) and \(g : \alpha \to \mathbb{R}\) be in \(L^1(\mu)\), and write \(\|h\|_1 = \int |h| \, d\mu\). If \(f_n \to g\) in \(\mu\)-measure (for every \(\varepsilon > 0\), \(\mu\{x : |f_n(x) - g(x)| \ge \varepsilon\} \to 0\)) and \(\|f_n\|_1 \to \|g\|_1\), then the family \((f_n)\) is uniformly integrable: \(\sup_n \|f_n\|_1 < \infty\), and the supremum of \(\int_s |f_n| \, d\mu\) over all \(n\) and all sets \(s \subseteq \alpha\) with \(\mu(s) \le \delta\) tends to \(0\) as \(\delta \to 0\).

The proof combines the \(L^1\) convergence \(\|f_n - g\|_1 \to 0\) given by Scheffé's lemma for convergence in measure with the Vitali convergence theorem.

theorem uniformIntegrable_of_tendstoInMeasure_of_tendsto_eLpNorm
    {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    {f : ℕ → α → ℝ} {g : α → ℝ}
    (hf : ∀ n, MemLp (f n) 1 μ) (hg : MemLp g 1 μ)
    (hfg : TendstoInMeasure μ f atTop g)
    (hnorm : Tendsto (fun n => eLpNorm (f n) 1 μ) atTop (𝓝 (eLpNorm g 1 μ))) :
    UniformIntegrable f 1 μ

Uses 1

Proof usesScheffé's lemma for convergence in measure

TheoremUniform integrability equivalences#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \(\alpha\), let \(f_n : \alpha \to \mathbb{R}\) (\(n \in \mathbb{N}\)) and \(g : \alpha \to \mathbb{R}\) be in \(L^1(\mu)\), write \(\|h\|_1 = \int |h| \, d\mu\), and suppose that \(f_n \to g\) in \(\mu\)-measure (for every \(\varepsilon > 0\), \(\mu\{x : |f_n(x) - g(x)| \ge \varepsilon\} \to 0\)). Then the following are equivalent: (1) the family \((f_n)\) is uniformly integrable, that is, \(\sup_n \|f_n\|_1 < \infty\) and the supremum of \(\int_s |f_n| \, d\mu\) over all \(n\) and all sets \(s \subseteq \alpha\) with \(\mu(s) \le \delta\) tends to \(0\) as \(\delta \to 0\); (2) \(f_n \to g\) in \(L^1(\mu)\), that is, \(\|f_n - g\|_1 \to 0\); (3) \(\|f_n\|_1 \to \|g\|_1\).

The equivalence of (1) and (2) is the Vitali convergence theorem; (3) implies (2) by Scheffé's lemma for convergence in measure, and (2) implies (3) by the reverse triangle inequality.

theorem uniformIntegrable_tfae_of_tendstoInMeasure
    {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    [IsFiniteMeasure μ]
    {f : ℕ → α → ℝ} {g : α → ℝ}
    (hf : ∀ n, MemLp (f n) 1 μ) (hg : MemLp g 1 μ)
    (hfg : TendstoInMeasure μ f atTop g) :
    [UniformIntegrable f 1 μ,
     Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0),
     Tendsto (fun n => eLpNorm (f n) 1 μ) atTop (𝓝 (eLpNorm g 1 μ))].TFAE

Uses 1

Proof usesScheffé's lemma for convergence in measure

TheoremScheffé's lemma on the real line#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be integrable and let \((f_n)_{n \in \mathbb{N}}\) be a sequence of integrable real functions \(f_n\) on \(\mathbb{R}\) such that \(f_n(x) \to f(x)\) for almost every \(x \in \mathbb{R}\). If \(\int_{\mathbb{R}} |f_n| \to \int_{\mathbb{R}} |f|\) as \(n \to \infty\), then \(\int_{\mathbb{R}} |f_n - f| \to 0\).

public theorem_wanted tendsto_integral_abs_sub_of_ae_tendsto_of_tendsto_integral_abs
  (f : ℝ → ℝ)
  (fn : ℕ → ℝ → ℝ)
  (hf : MeasureTheory.Integrable f)
  (hfn : ∀ n : ℕ, MeasureTheory.Integrable (fn n))
  (hae : ∀ᵐ x ∂MeasureTheory.volume, Filter.Tendsto (fun n : ℕ => fn n x) Filter.atTop (nhds (f x)))
  (hnorm : Filter.Tendsto
      (fun n : ℕ => ∫ x : ℝ, |fn n x|)
      Filter.atTop
      (nhds (∫ x : ℝ, |f x|))) :
  Filter.Tendsto
    (fun n : ℕ => ∫ x : ℝ, |fn n x - f x|)
    Filter.atTop
    (nhds 0)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_76.

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.