Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck 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.

Dominated convergence is a Vitali corollary

Statement

Let (X,A,μ) be a sigma-finite measure space. Let fn:X→R be measurable, let g∈L1(μ) be nonnegative, and suppose ∣fn∣≤g almost everywhere for every n and fn→f almost everywhere. Then f∈L1(μ) and fn→f in L1(μ).

Facts & Assumptions

Given: A sigma-finite measure space (X,A,μ), measurable functions fn,f:X→R, and a nonnegative integrable function g with ∣fn∣≤g almost everywhere and fn→f almost everywhere.

[L1]

A dominated family is uniformly integrable. (Dominated families are uniformly integrable)

[L2]

On a sigma-finite measure space, convergence in measure together with uniform integrability and tightness implies convergence in L1. (Vitali convergence theorem on finite and sigma-finite measure spaces)

[L3]

On a finite measure space, almost-everywhere convergence implies convergence in measure. (On a finite measure space, almost-everywhere convergence implies convergence in measure)

[L4]

If h:X→[0,+∞] is measurable and t>0, then μ({h≥t})≤t−1∫h dμ. (Chebyshev-Markov inequality for the integral)

[L5]

For an increasing sequence of nonnegative measurable functions, the integrals increase to the integral of the limit. (Monotone convergence for the integral)

[L6]

If two integrable functions are equal almost everywhere, then their integrals over every measurable set agree. (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree)

[L7]

Sigma-finiteness means that X=⋃mXm for some measurable sets Xm of finite measure. (Finite, sigma-finite, and semifinite measures)

[L8]

For a measurable set E and a nonnegative measurable function u, ∫Eu dμ=∫uχE dμ. (Integral over a measurable subset)

[L10]

Countable unions of null sets are null. (Finite and countable subadditivity of measures)

Proof

technique · direct
1.1L10construct

Let N∗ be a null set outside which fn(x)→f(x), and for each n∈N let Nn be a null set outside which ∣fn∣≤g. Put N:=N∗∪⋃n=0∞Nn. By [L10], the set N is null. On X∖N one has fn(x)→f(x) for every x and ∣fn(x)∣≤g(x) for every n, so also ∣f(x)∣≤g(x) there.

1.2L1

By [L1], the family {fn:n∈N} is uniformly integrable.

2.1step 1.1L5L6L7L8L9algebra

By [L7], choose measurable sets Ym of finite measure with X=⋃mYm, and put Xm:=⋃j=0mYj. Then Xm is measurable of finite measure, Xm↑X, and hence gχXm↑g. Fact [L5] gives ∫Xmg dμ↑∫g dμ, so ∫X∖Xmg dμ→0. Fix ε>0 and choose m with ∫X∖Xmg dμ<ε. For each n, put un,m:=∣fn∣χ(X∖Xm)∖N. Then un,m=∣fn∣χX∖Xm almost everywhere and un,m≤gχX∖Xm pointwise, so [L6], [L8], and [L9] give ∫X∖Xm∣fn∣ dμ=∫X∖Xmun,m dμ≤∫X∖Xmg dμ<ε. So the family {fn} is tight.

2.2step 1.1L3L4L8L9choosealgebra

Let ε,η>0. Choose m so that ∫X∖Xmg dμ<εη/8. On the finite measure space Xm, step 1.1 and [L3] make fn→f in measure. Define hn:=∣fn−f∣χ(X∖Xm)∖N. Then {hn>ε}={∣fn−f∣>ε}∩((X∖Xm)∖N), and hn≤2gχX∖Xm pointwise. Since N is null, μ({∣fn−f∣>ε}∩(X∖Xm))=μ({hn>ε}). Therefore [L4], [L8], and [L9] give μ({∣fn−f∣>ε}∩(X∖Xm))≤ε−1∫X∖Xmhn dμ≤2ε∫X∖Xmg dμ<η/4. Combining this with convergence in measure on Xm shows fn→f in measure on all of X.

3.1step 1.2step 2.1step 2.2L2∎

Step 1.2 gives uniform integrability, step 2.1 gives tightness, and step 2.2 gives convergence in measure. Applying [L2] yields f∈L1(μ) and fn→f in L1(μ).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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