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

The functional Λg has norm gq; for q= assume μ is semifinite

Statement

Let (X,A,μ) be a measure space, let 1p<, and let q be conjugate to p. For gLq(μ), let Λg([f])=fgdμ. Then Λggq. If 1<p<, then equality holds: Λg=gq. If p=1 and hence q=, the same equality holds provided μ is semifinite.

Facts & Assumptions

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

[L1]

The pairing functional Λg is bounded and satisfies Λggq (Every gLq(μ) defines a bounded linear functional on Lp(μ)).

[L2]

If 1<p< and q is conjugate to p, then p(q1)=q (Conjugate exponents, including the endpoint conventions).

[L3]

The essential supremum is the least essential bound: if M=g and u is any measurable representative of g, then uM almost everywhere. If M>0 and 0<ε<M, then the set {u>Mε} has positive measure; otherwise Mε would be a smaller essential bound (The essential supremum is attained as the least essential bound).

[L4]

In a semifinite measure space, every measurable set of positive measure contains a measurable subset of positive finite measure (Finite, sigma-finite, and semifinite measures).

Proof

technique · Use Holder for the upper bound. For $1<p<\infty$ test against the normalized extremizer $|g|^{q-1}\operatorname{sgn} g$; for $p=1$ use a finite-measure subset of an almost-maximal level set, which is exactly where semifiniteness enters
1.1

The upper bound Λggq is exactly [L1].

L1given
2.1

If g=0 in Lq(μ), then Λg=0 by definition, so Λg=0=gq. Hence only the case g0 remains.

step 1.1given
2.2

Assume 1<p<. Choose a representative u of g and define s(x):={u(x)/u(x),u(x)0,0,u(x)=0,f(x):=u(x)q1s(x)gqq1. Then fp=uq/gqq by [L2], so [f]pp=1gqquqdμ=1. Also fu=uq/gqq1, so Λg([f])=1gqq1uqdμ=gq. Therefore Λggq. Together with step 1.1, this gives Λg=gq.

L2step 1.1givenchooseconstruct
3.1

Assume p=1, so q=, and assume μ is semifinite. Put M:=g. Step 2.1 leaves only g0, so M>0. Choose a representative u of g, and define s(x):={1,u(x)>0,1,u(x)<0,0,u(x)=0. For 0<ε<M, [L3] gives a measurable set Eε:={u>Mε} of positive measure. By [L4], choose FεEε with 0<μ(Fε)<, and set fε:=s1Fεμ(Fε). Then [fε]1=1 and Λg([fε])=1μ(Fε)FεudμMε. Hence ΛgMε for every 0<ε<M, so ΛgM=g. Step 1.1 gives the reverse inequality, and therefore Λg=g.

L3L4step 1.1step 2.1givenchooseconstruct
4.1

Step 2.2 proves the strict-exponent case, and step 3.1 proves the q= endpoint under semifiniteness. Together with steps 1.1 and 2.1, this proves the proposition.

step 1.1step 2.1step 2.2step 3.1

Depends on

Used by

Dependency tree · two levels

16 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