Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-23 (gpt-6-sol)
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.

A bounded real C_0(X) functional is a difference of positive functionals

Statement

Every bounded real linear functional L on C0(X;R) can be written L=L+−L−, where L+ and L− are bounded positive linear functionals and ∥L±∥≤∥L∥.

Facts & Assumptions

Given: L:C0(X;R)→R is bounded and linear.

Proof

technique · direct
1.1given

For f≥0 define L+(f)=sup⁡{L(g):0≤g≤f}. The supremum is finite because ∣L(g)∣≤∥L∥∥f∥∞. It is positively homogeneous and monotone.

2.1step 1.1

If f,h≥0, decompositions 0≤g≤f+h satisfy g=g1+g2 with g1=min⁡(g,f) and g2=g−g1, where 0≤g1≤f and 0≤g2≤h. This gives L+(f+h)≤L+(f)+L+(h); the reverse inequality follows by adding independent approximants. Thus L+ is additive on the positive cone.

3.1step 1.1step 2.1∎

Extend L+ linearly by L+(u)=L+(u+)−L+(u−). Cone additivity makes this well defined and positive. Put L−=L+−L; for f≥0, the competitor g=f in step 1.1 gives L+(f)≥L(f), so L− is positive. For 0≤f≤1 pointwise, step 1.1 gives 0≤L+(f)≤∥L∥ and L−(f)=sup⁡0≤g≤f[−L(f−g)]≤∥L∥. For either positive functional P, ∣P(u)∣≤P(∣u∣) and 0≤∣u∣≤∥u∥∞, so these positive-unit-ball bounds imply ∥L±∥≤∥L∥. Finally L=L+−L−.

Depends on

Used by

Dependency tree · two levels

4 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