Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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.

Every gLq(μ) defines a bounded linear functional on Lp(μ)

Statement

Let (X,A,μ) be a measure space, let 1p<, and let q be conjugate to p. For each gLq(μ), the formula Λg([f]):=fgdμ defines a bounded linear functional on Lp(μ), and Λg([f])[f]pgq([f]Lp(μ)). In particular, Λggq.

Facts & Assumptions

Given: A measure space (X,A,μ), an exponent 1p<, its conjugate exponent q, an element gLq(μ), and an element [f]Lp(μ).

[L1]

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

[L2]

Holder's inequality gives uvdμupvq for measurable representatives uLp(μ) and vLq(μ) when both exponents are finite, with the corresponding L1--L representative form at the endpoint (Holder's inequality for integrals, including the endpoint cases).

[L3]

Two integrable functions have the same integral whenever they are equal almost everywhere (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree).

[L4]

The Lebesgue integral is linear on L1(μ) (The Lebesgue integral is linear on L1(μ)).

Proof

technique · Use Holder to make the pairing integrable, then use almost-everywhere invariance of the integral to descend from representatives to $L^p$ classes
1.1

Choose measurable representatives u of [f] and v of g. Then uLp(μ); if q< then vLq(μ), while if q= then v is an essentially bounded representative. Thus [L2] gives uvL1(μ) and uvdμupvq=[f]pgq.

L1L2given
2.1

If u is another representative of [f], then u=u almost everywhere. Hence uv=uv almost everywhere. Since both products are integrable by step 1.1, [L3] gives uvdμ=uvdμ, so Λg([f]) is well defined on the class [f].

L1L3step 1.1
2.2

If v is another representative of g, then v=v almost everywhere. Hence uv=uv almost everywhere. Since both products are integrable by step 1.1, [L3] gives uvdμ=uvdμ, so Λg([f]) is independent of the chosen representative of g.

L1L3step 1.1
3.1

Let [f],[h]Lp(μ) and let a,bR. Choose representatives u,w. By step 2.1 we may compute with representatives, and [L4] gives Λg(a[f]+b[h])=(au+bw)vdμ=auvdμ+bwvdμ=aΛg([f])+bΛg([h]). The estimate from step 1.1 also shows Λg([f])[f]pgq, so Λg is linear and bounded.

step 1.1step 2.1step 2.2L4given
4.1

The estimate in step 3.1 holds for every [f] with [f]p1. Taking the supremum over the unit ball gives Λggq. Thus Λg is a bounded linear functional on Lp(μ).

step 3.1given

Depends on

Used by

Dependency tree · two levels

21 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