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 has norm ; for assume is semifinite
Statement
Let be a measure space, let , and let be conjugate to . For , let Then If , then equality holds: If and hence , the same equality holds provided is semifinite.
Facts & Assumptions
Given: A measure space , an exponent , its conjugate exponent , and an element .
The pairing functional is bounded and satisfies (Every defines a bounded linear functional on ).
If and is conjugate to , then (Conjugate exponents, including the endpoint conventions).
The essential supremum is the least essential bound: if and is any measurable representative of , then almost everywhere. If and , then the set has positive measure; otherwise would be a smaller essential bound (The essential supremum is attained as the least essential bound).
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
The upper bound is exactly [L1].
If in , then by definition, so . Hence only the case remains.
Assume . Choose a representative of and define Then by [L2], so Also , so Therefore . Together with step 1.1, this gives .
Assume , so , and assume is semifinite. Put . Step 2.1 leaves only , so . Choose a representative of , and define For , [L3] gives a measurable set of positive measure. By [L4], choose with , and set Then and Hence for every , so . Step 1.1 gives the reverse inequality, and therefore .
Step 2.2 proves the strict-exponent case, and step 3.1 proves the endpoint under semifiniteness. Together with steps 1.1 and 2.1, this proves the proposition.