Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Almost uniform convergence implies almost-everywhere convergence and convergence in measure

Statement

Let (X,A,μ) be a measure space and let fn,f:XR be measurable. If fnf almost uniformly, then fnf μ-almost everywhere and fnf in measure.

Facts & Assumptions

Given: A measure space (X,A,μ), measurable functions fn,f:XR, and almost-uniform convergence of (fn) to f.

[L1]

Almost-uniform convergence means that for every ε>0 there is a measurable E with μ(E)<ε such that fnf uniformly on XE. (Almost uniform convergence)

[L2]

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

[L3]

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

[L4]

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

Proof

technique · direct
1.1

For each m1, [L1] gives a measurable set Em with μ(Em)<1/m such that fnf uniformly on XEm. Let N:=m=1Em. Since NEm for every m, [L4] gives μ(N)1/m for every m, hence μ(N)=0. If xXN, then xEm for some m, and uniform convergence on XEm implies fn(x)f(x). Therefore fnf almost everywhere by [L2].

L1L2L4
1.2

Fix ε>0 and η>0. By [L1] choose a measurable set E with μ(E)<η such that fnf uniformly on XE. Then there is N such that for nN and xXE one has fn(x)f(x)ε, so {fnf>ε}E. Hence μ({fnf>ε})μ(E)<η for nN. Since η was arbitrary, [L3] follows.

L1L3L4
2.1

Steps 1.1 and 1.2 prove the two asserted conclusions.

step 1.1step 1.2

Depends on

Used by

Dependency tree · two levels

8 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