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.

Egorov's theorem

Statement

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

The finite-measure hypothesis is used exactly at the continuity-from-above step below.

Facts & Assumptions

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

[L1]

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

[L2]

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

[L3]

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

[L4]

For measurable (Ek) one has μ(kEk)k=0μ(Ek). (Finite and countable subadditivity of measures)

[L5]

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

Proof

technique · direct
1.1

Let ε>0, and let N be a measurable null set outside which fn(x)f(x). For m,k1 put Ek,m:=jk{fjf>1/m}. For fixed m the sets Ek,m decrease with k, each lies in X, and k=1Ek,mN because outside N only finitely many j satisfy fj(x)f(x)>1/m. Therefore [L3] and [L5] give μ(Ek,m)μ ⁣(k=1Ek,m)=0. So for each m1 there is a least index k(m) with μ(Ek(m),m)<ε2m.

L1L3L5choose
2.1

Put E:=m=1Ek(m),m. Then [L4] and step 1.1 give μ(E)m=1μ(Ek(m),m)<m=1ε2m=ε. If xXE, then for every m1 and every jk(m) one has fj(x)f(x)1/m. Hence for any η>0 one may choose m with 1/m<η and then jk(m) gives fj(x)f(x)<η. So fnf uniformly on XE.

step 1.1L4algebra
3.1

Since ε>0 was arbitrary, step 2.1 is exactly [L2]. Therefore fnf almost uniformly.

step 2.1L2

Depends on

Used by

Dependency tree · two levels

14 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