Alphabeta Math
PropositionStatement: 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.

On a semifinite measure space, a representing Lq function is unique

Statement

Let (X,A,μ) be a semifinite measure space, let 1≤p<∞, and let q be conjugate to p. If g,h∈Lq(μ) satisfy ∫fg dμ=∫fh dμ([f]∈Lp(μ)), then g=h in Lq(μ). Equivalently, on a semifinite measure space a bounded functional on Lp(μ) has at most one representing Lq(μ) class.

Facts & Assumptions

Given: A semifinite measure space (X,A,μ), an exponent 1≤p<∞, its conjugate exponent q, and g,h∈Lq(μ) such that ∫fg dμ=∫fh dμ for every [f]∈Lp(μ).

[L1]

On a semifinite measure space, ∥Λu∥=∥u∥q(u∈Lq(μ)) (The functional Λg has norm ∥g∥q; for q=∞ assume μ is semifinite).

[L2]

For finite exponents, the Lq norm is a genuine norm on the quotient space The Lp norm descends to the quotient and makes Lp a normed space for 1≤p≤∞.

[L3]

If ∥u∥∞=0, then ∣u∣≤0 almost everywhere, so u=0 almost everywhere (The essential supremum is attained as the least essential bound).

Proof

technique · Subtract the two representing functions, observe that the induced pairing is the zero functional, and use the norm formula for $\Lambda_g$ to force the difference to be the zero $L^q$ class
1.1givenalgebra

For every [f]∈Lp(μ), the assumption gives [given, algebra] Λg−h([f])=∫f(g−h) dμ=0. So Λg−h is the zero functional on Lp(μ).

2.1L1step 1.1

Applying [L1] to u=g−h yields [L1, step 1.1] ∥g−h∥q=∥Λg−h∥=0.

3.1L2L3step 2.1∎

If q<∞, [L2] says that zero Lq norm means the zero class, so [L2, L3, step 2.1] g=h in Lq(μ). If q=∞, then step 2.1 and [L3] give g=h almost everywhere. In either case the representing class is unique.

Depends on

Used by

Dependency tree · two levels

15 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