Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Vitali convergence theorem on finite and sigma-finite measure spaces

Statement

Let (X,A,μ) be a measure space, let fn:XR be measurable with fnL1(μ) for every n, and let f:XR be measurable.

  1. If μ(X)<+, then fnf in L1(μ) if and only if fnf in measure and the family {fn:nN} is uniformly integrable.
  2. If μ is sigma-finite and fnf in measure, and the family {fn:nN} is uniformly integrable and tight, then fL1(μ) and fnf in L1(μ).

Facts & Assumptions

Given: Integrable real-valued functions fnL1(μ) and a measurable f:XR.

[L1]

Convergence in measure means that for every real ε>0, μ({fnf>ε})0. (Convergence in measure)

[L2]

Convergence in L1(μ) means fnfdμ0. (Convergence in L^1(mu))

[L3]

On a finite measure space, uniform integrability is equivalent to L1-boundedness plus uniform absolute continuity. (On a finite measure space, uniform integrability is equivalent to L^1-boundedness plus uniform absolute continuity)

[L4]

Convergence in L1(μ) implies convergence in measure. (Convergence in L^1(mu) implies convergence in measure)

[L5]

Convergence in measure has a subsequence converging almost everywhere. (Riesz's subsequence theorem for convergence in measure)

[L6]

If gL1(μ) and ε>0, then there is δ>0 such that μ(E)<δEgdμ<ε. (Absolute continuity of the integral)

[L7]

For nonnegative measurable functions un, lim infnundμlim infnundμ. (Fatou's lemma)

[L8]

A family is tight when for every ε>0 there is a measurable set E of finite measure such that supnXEfndμ<ε. (A tight family of integrable functions)

Proof

technique · direct
1.1

Assume μ(X)<+ and fnf in L1(μ). By [L4], the sequence converges to f in measure. To prove uniform integrability, it suffices by [L3] to show L1-boundedness and uniform absolute continuity. For L1-boundedness, choose N so that fnfdμ<1 for nN. Then fndμfdμ+1 for nN, and the finitely many initial terms may be absorbed into one larger bound.

L2L3L4algebra
1.2

Still on a finite measure space, assume fnf in measure and the family {fn} is uniformly integrable. By [L3], the family is L1-bounded and uniformly absolutely continuous on small sets. By [L5], some subsequence fnk converges to f almost everywhere. Fatou's lemma [L7] then gives fdμlim infkfnkdμ<+, so fL1(μ).

L3L5L7algebra
2.1

Still under step 1.1, let ε>0. Choose N so that fnfdμ<ε/2 for nN. Apply [L6] to f and to the finitely many functions f0,,fN1, and let δ be the minimum of the resulting positive numbers. Then μ(E)<δ implies Efndμ<ε for every n<N, while for nN one has EfndμEfdμ+fnfdμ<ε. So [L3] yields uniform integrability.

L2L3L6choosealgebra
2.2

Let ε>0. Choose δ>0 such that μ(E)<δ implies both supnEfndμ<ε/3 and Efdμ<ε/3; the first uses step 1.2 together with [L3], and the second uses [L6]. Choose η>0 with ημ(X)<ε/3. Since fnf in measure, there is N such that μ(Bn)<δ for nN, where Bn:={fnf>η}. Then for nN, fnfdμBnfndμ+Bnfdμ+XBnηdμ<ε. So fnf in L1(μ).

step 1.2L1L2L3L6choosealgebra
3.1

Assume now that μ is sigma-finite, that fnf in measure, and that the family {fn} is uniformly integrable and tight. Let ε>0. By [L8], choose a measurable set E with μ(E)<+ and supnXEfndμ<ε/4. Because fnf in measure on X, the restricted sequence converges in measure on E as well, and uniform integrability persists on E. Therefore step 2.2 applied on the finite measure space E gives fEL1(μ) and Efnfdμ0. By [L5], after passing to a subsequence if necessary we may assume fnkf almost everywhere on X. Applying [L7] to the nonnegative functions fnk1XE gives XEfdμlim infkXEfnkdμε/4. Hence fL1(μ). For all large n one has Efnfdμ<ε/2, and then fnfdμEfnfdμ+XEfndμ+XEfdμ<ε. So fnf in L1(μ).

step 2.2L5L7L8choosealgebra
4.1

Step 1.1 proves the forward finite implication, steps 1.2 and 2.2 prove the reverse finite implication, and step 3.1 proves the sigma-finite tight form.

step 1.1step 2.1step 1.2step 2.2step 3.1

Depends on

Used by

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources