Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09
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 Lq norm recovery from finite simple dual tests

Statement

Let 1q, let r be its conjugate exponent, and let Σfin denote the complex finite simple functions whose nonzero sets have finite measure. Define S(g):=sup{Xgsdμ:sΣfin, sr1}. On a sigma-finite measure space, if g:XC is measurable and gs is integrable for every sΣfin, then gq=S(g), allowing extended values. Thus a finite uniform bound on these tests proves gLq with its norm at most that bound.

If g is already in Lq, the same identity holds on every measure space for q<, and on semifinite measure spaces for q=. The pairing is bilinear; a sesquilinear formulation replaces s by its conjugate. The zero test is allowed, including on zero measure spaces.

Facts & Assumptions

Given: A measurable finite-valued complex function g and conjugate q,r[1,], with either the sigma-finite/test-integrability hypothesis or the stated already-Lq hypothesis.

[F1]

Complex measurability is componentwise and finite support here means finite-measure nonzero set (Complex Lp classes and Euclidean test-function conventions).

[F2]

Complex Hölder holds at all conjugate endpoints, and norms satisfy the triangle inequality (Complex Holder, Minkowski, and the quotient norm).

[F3]

Sigma-finiteness supplies a finite-measure exhaustion; semifiniteness supplies a positive finite-measure subset of each positive-measure set (Finite, sigma-finite, and semifinite measures).

[F4]

r=q/(q1) for 1<q<, while the endpoints are (q,r)=(1,),(,1) (Conjugate exponents, including the endpoint conventions).

[F5]

Essential supremum is the infimum of the essential bounds (The essential supremum of a measurable function with respect to a measure).

[F6]

Increasing nonnegative functions have increasing integrals converging to the integral of their limit (Monotone convergence for the integral).

[F7]

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

[F9]

Real sums and products of finite measurable functions are measurable (Arithmetic and lattice operations preserve measurability whenever they are defined).

[F10]

Real threshold preimages characterize measurability (Threshold characterisations of real-valued and extended-real-valued measurability).

[F11]

Integral monotonicity and scaling bound measures of level sets (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F12]

A countable union of null measurable sets is null (Finite and countable subadditivity of measures).

Proof

technique · Construct phase extremizers on bounded finite sets, approximate them by finite grids, and exhaust positive level sets
1.1

Put a=g and θ=g/a on {a>0}, zero elsewhere. The function b=1/a on {a>0}, zero elsewhere, is measurable: for t0, its strict upper level set is {0<a<1/t} when t>0 and {a>0} when t=0; negative upper thresholds give X. Real positive powers of a have upper sets {a>t1/γ} for γ>0,t0. Thus F9–F10 and F1 show the phase, the powers and all ensuing products are measurable. F8 gives θ1 and gθ=a.

F1F8F9F10
1.2

Let E be measurable of finite measure and let h be a bounded measurable function vanishing outside E, with hr1 and Eg<. Round each coordinate of h down to an integer multiple of 1/m on E and set the result tm to zero off E. This has finite range, measurable fibers, and tmh2/m. When r= and h1, replace each of its finitely many values z by z/max(1,z); these values lie in the closed unit disk and the error is at most 22/m, because the displacement of z is at most zh. For finite r, the uniform error em gives tmhremμ(E)1/r0; for infinity it gives tmhem0. Put dm=max(1,tmr) and sm=tm/dm. F2 gives 1dm1+tmhr, hence dm1 and smh uniformly, since h is bounded. Each sm is an admissible finite simple test, and F7 gives g(smh)supEsmhEg0. Therefore S(g)gh. If μ(E)=0, the integral is zero and the zero test already suffices.

F1F2F7F9F10
2.1

Let E have finite measure with aB< on E, and put A=g1Eq for finite q. If A=0, S(g)A from the zero test. If A>0 and 1<q<, set h=1Eθaq1/Aq1. This is bounded, and (q1)r=q gives hr=AqEaq=1. Moreover gh=A(q1)Eaq=A. For q=1 set h=1Eθ instead; it is bounded by one and gh=Ea=A. In both cases EgBμ(E)<, so step 1.2 applies and gives S(g)g1Eq.

F4F11step 1.1step 1.2
3.1

Under sigma-finiteness take a covering Hj of finite measure and put En=(jnHj){1/nan} for n1. These finite-measure sets increase and cover {a>0}. For finite q, aq1Enaq everywhere, so F6 yields g1Enqgq, possibly infinitely. Step 2.1 proves S(g)gq. If that norm is finite, F2 bounds every admissible test by gq; if it is infinite the lower bound already gives equality at infinity. The assumed test integrability ensures every integral in the defining supremum is meaningful.

F2F3F6step 2.1
3.2

If instead gLq with q< on an arbitrary measure space, use En={1/nan}. F11 gives nqμ(En)aq<, hence μ(En)<. The same increasing limit and step 2.1 give S(g)gq. Hölder gives the reverse bound and integrability of every gs: a finite simple function of finite-measure support belongs to every finite-exponent Lr, and is bounded when r=. No sigma-finiteness of X is needed.

F2F6F11step 2.1
4.1

Now let q= and M=g>0, possibly infinite under the sigma-finite hypothesis. For any 0<t<M, the measurable set D={a>t} has positive measure, since otherwise t would be an essential bound. In the sigma-finite case, D=n(DEn) with the sets from step 3.1. F12 implies some B=DEn has positive measure, and 0<μ(B)< with an there. In the semifinite already-L-infinity case, M<; the set {a>M+1} is null by F5. Semifiniteness applied to D{aM+1} gives a measurable B of finite positive measure. In either case h=θ1B/μ(B) is bounded, h1=1, and gh=μ(B)1Bat. Step 1.2 now yields S(g)t. Letting tM, or taking arbitrarily large t if M=, proves S(g)M. For finite M, F2 gives S(g)M. If M=0, F2 and the zero test give S(g)=0.

F2F3F4F5F12step 1.1step 1.2step 3.1
5.1

The measure on X={x} with μ()=0, μ(X)= is countably additive: a disjoint family contains at most one nonempty member. It is not semifinite. For g(x)=1, its essential norm is one, yet the only finite-measure-supported simple function is zero, so S(g)=0. This verifies the necessity of a measure hypothesis at the infinity endpoint. Finally the zero test makes every stated supremum nonempty; on zero measure spaces it and every other integral have value zero. The previous steps prove all the claimed identities and therefore the finite-bound membership conclusion.

step 3.1step 3.2step 4.1

Depends on

Used by

Dependency tree · two levels

58 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