Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

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

Statement

Let (X,A,μ) be a measure space with μ(X)<+∞, and let fn,f:X→R be measurable. If fn→f μ-almost everywhere, then fn→f in measure.

Facts & Assumptions

Given: A finite measure space (X,A,μ) and measurable functions fn,f:X→R such that fn→f almost everywhere.

[L1]

Almost-everywhere convergence means pointwise convergence off a measurable null set. (Convergence almost everywhere relative to a measure)

[L2]

Convergence in measure means that for every real ε>0, μ({∣fn−f∣>ε})→0. (Convergence in measure)

[L3]

If (En) is a decreasing sequence of measurable sets and one En0 has finite measure, then μ(⋂nEn)=inf⁡nμ(En). (Continuity from above when one set has finite measure)

[L4]

If A⊆B are measurable, then μ(A)≤μ(B). (Measures are monotone)

Proof

technique · direct
1.1givenL1

Fix ε>0, and let N be a measurable null set outside which fn(x)→f(x). For r≥0 put Er:=⋃n≥r{∣fn−f∣>ε}. Then (Er) is a decreasing sequence of measurable sets, each contained in X, and ⋂r=0∞Er⊆N because outside N only finitely many indices can satisfy ∣fn(x)−f(x)∣>ε.

2.1step 1.1L2L3L4

Because μ(X)<+∞, [L3] applies to (Er). The intersection in step 1.1 is null, so μ(Er)↓μ ⁣(⋂r=0∞Er)=0. For each r one has {∣fr−f∣>ε}⊆Er, hence by [L4] μ({∣fr−f∣>ε})≤μ(Er)→0. This is exactly [L2].

3.1step 2.1L2∎

Since ε>0 was arbitrary, the sequence converges in measure.

Depends on

Used by

Dependency tree · two levels

10 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