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

For 1p<, every Lp(μ) class has a sigma-finite essential support

Statement

Let (X,A,μ) be a measure space and let 1p<. For every element [f]Lp(μ) there is a measurable sigma-finite set SX such that f=0 almost everywhere on XS.

Facts & Assumptions

Given: A measure space (X,A,μ), an exponent 1p<, and a class [f]Lp(μ).

[L1]

Elements of Lp(μ) are almost-everywhere classes of measurable representatives (The space Lp(μ) as the quotient by null functions).

[L2]

Chebyshev-Markov gives μ({upt})t1updμ(t>0) (Chebyshev-Markov inequality for the integral).

[L3]

Sigma-finiteness means a countable union of finite-measure measurable sets (Finite, sigma-finite, and semifinite measures).

Proof

Proof technique: Take a representative u and use the level sets {u1/n}. Chebyshev-Markov makes each level set finite-measure, and their union contains every point where u0.

1.1

Choose a measurable representative u of [f] and, for each n1, [L1, L2, given, choose, construct] set En:={u1/n}={upnp}. Since uLp(μ), [L2] gives μ(En)npupdμ<. So every En has finite measure.

2.1

Put [L3, step 1.1] S:=n=1En. By step 1.1 and [L3], the set S is sigma-finite.

3.1

If xS, then u(x)<1/n for every n1, hence u(x)=0. [step 2.1, algebra] Therefore u=0 on XS, so the class [f] vanishes almost everywhere outside the sigma-finite set S. ∎

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