Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Complex l one functionals on finite measure spaces have bounded densities

Statement

Assume the Axiom of Choice. If (X,A,μ) is a finite measure space and Λ:L1(μ;C)C is bounded and complex-linear, then there is an essentially bounded complex measurable g such that Λ(f)=Xfgdμ(fL1(μ;C)). One may take g2Λ. The pairing contains no conjugation. AC is used through the finite-measure real Radon–Nikodym representation supplier.

Facts & Assumptions

[F1]

Under AC a bounded real functional on finite-measure Lp, 1p<, has a real integrable density representing it on every bounded measurable representative (On a finite-measure space, a bounded Lp functional is integration against its Radon-Nikodym density).

[F2]

Complex integration is defined through real and imaginary parts (Integrable real and complex functions, and their integrals).

[F3]

The assumed axiom is The Axiom of Choice.

[F4]

Dominated convergence yields L1 convergence under an integrable majorant (Dominated convergence).

[F5]

hh for integrable complex h (The modulus of an integral is bounded by the integral of the modulus).

Proof

Given: AC, the finite measure space and Λ; put M=Λ.

1.1

Restrict ReΛ and ImΛ to real L1 classes. They are real-linear with norm at most M. F1 with p=1, under F3, gives real h1,h2L1 representing them on bounded real measurable functions.

givenF1F3
2.1

Fix either density h and its real functional A. For k1, set Ek={h>M+1/k}. Its indicator is in L1 since the measure space is finite. Then (M+1/k)μ(Ek)Ekh=A(1Ek)Mμ(Ek), so μ(Ek)=0. Apply the same reasoning to {h>M+1/k} with the negative functional. Their countable union shows hM almost everywhere. Define g=h1+ih2; it is measurable and g2M almost everywhere. We may set it to zero on the explicitly determined null set where this bound fails.

step 1.1F2algebra
3.1

For a bounded complex function f=a+ib with real bounded a,b, complex linearity gives Λ(f)=Λ(a)+iΛ(b)=a(h1+ih2)+ib(h1+ih2)=fg, using F2. For arbitrary fL1, let fN=fmin(1,N/f), with zero value at f=0. Then fN is bounded, fNf pointwise and fNff, so F4 gives fNf10. Boundedness of Λ gives Λ(fN)Λ(f), while step 2.1 and F5 give (fNf)g2MfNf10. Passing to the limit proves the formula for all L1 classes.

step 2.1step 1.1F2F4F5
4.1

If M=0, the same level-set argument gives g=0 almost everywhere; if μ(X)=0, L1 is the zero space and take g=0. Indicator tests were used only on a finite-measure space, and truncations were explicitly defined. The full AC use is precisely F1, not a presumed complex duality theorem.

step 3.1F1F3

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