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 , let be its conjugate exponent, and let denote the complex finite simple functions whose nonzero sets have finite measure. Define On a sigma-finite measure space, if is measurable and is integrable for every , then , allowing extended values. Thus a finite uniform bound on these tests proves with its norm at most that bound.
If is already in , the same identity holds on every measure space for , and on semifinite measure spaces for . The pairing is bilinear; a sesquilinear formulation replaces by its conjugate. The zero test is allowed, including on zero measure spaces.
Facts & Assumptions
Given: A measurable finite-valued complex function and conjugate , with either the sigma-finite/test-integrability hypothesis or the stated already-Lq hypothesis.
Complex measurability is componentwise and finite support here means finite-measure nonzero set (Complex Lp classes and Euclidean test-function conventions).
Complex Hölder holds at all conjugate endpoints, and norms satisfy the triangle inequality (Complex Holder, Minkowski, and the quotient norm).
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).
for , while the endpoints are (Conjugate exponents, including the endpoint conventions).
Essential supremum is the infimum of the essential bounds (The essential supremum of a measurable function with respect to a measure).
Increasing nonnegative functions have increasing integrals converging to the integral of their limit (Monotone convergence for the integral).
for integrable complex (The modulus of an integral is bounded by the integral of the modulus).
and modulus is multiplicative (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Real sums and products of finite measurable functions are measurable (Arithmetic and lattice operations preserve measurability whenever they are defined).
Real threshold preimages characterize measurability (Threshold characterisations of real-valued and extended-real-valued measurability).
Integral monotonicity and scaling bound measures of level sets (Monotonicity and nonnegative homogeneity of the nonnegative integral).
A countable union of null measurable sets is null (Finite and countable subadditivity of measures).
Proof
Put and on , zero elsewhere. The function on , zero elsewhere, is measurable: for , its strict upper level set is when and when ; negative upper thresholds give . Real positive powers of have upper sets for . Thus F9–F10 and F1 show the phase, the powers and all ensuing products are measurable. F8 gives and .
Let be measurable of finite measure and let be a bounded measurable function vanishing outside , with and . Round each coordinate of down to an integer multiple of on and set the result to zero off . This has finite range, measurable fibers, and . When and , replace each of its finitely many values by ; these values lie in the closed unit disk and the error is at most , because the displacement of is at most . For finite , the uniform error gives ; for infinity it gives . Put and . F2 gives , hence and uniformly, since is bounded. Each is an admissible finite simple test, and F7 gives . Therefore . If , the integral is zero and the zero test already suffices.
Let have finite measure with on , and put for finite . If , from the zero test. If and , set . This is bounded, and gives . Moreover . For set instead; it is bounded by one and . In both cases , so step 1.2 applies and gives .
Under sigma-finiteness take a covering of finite measure and put for . These finite-measure sets increase and cover . For finite , everywhere, so F6 yields , possibly infinitely. Step 2.1 proves . If that norm is finite, F2 bounds every admissible test by ; 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.
If instead with on an arbitrary measure space, use . F11 gives , hence . The same increasing limit and step 2.1 give . Hölder gives the reverse bound and integrability of every : a finite simple function of finite-measure support belongs to every finite-exponent Lr, and is bounded when . No sigma-finiteness of is needed.
Now let and , possibly infinite under the sigma-finite hypothesis. For any , the measurable set has positive measure, since otherwise would be an essential bound. In the sigma-finite case, with the sets from step 3.1. F12 implies some has positive measure, and with there. In the semifinite already-L-infinity case, ; the set is null by F5. Semifiniteness applied to gives a measurable of finite positive measure. In either case is bounded, , and . Step 1.2 now yields . Letting , or taking arbitrarily large if , proves . For finite , F2 gives . If , F2 and the zero test give .
The measure on with , is countably additive: a disjoint family contains at most one nonempty member. It is not semifinite. For , its essential norm is one, yet the only finite-measure-supported simple function is zero, so . 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.
Depends on
- Complex Holder, Minkowski, and the quotient norm
- Complex finite-simple and smooth compact-support density for finite p
- Finite, sigma-finite, and semifinite measures
- Conjugate exponents, including the endpoint conventions
- The essential supremum of a measurable function with respect to a measure
- Monotone convergence for the integral
- The modulus of an integral is bounded by the integral of the modulus
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- Arithmetic and lattice operations preserve measurability whenever they are defined
- Threshold characterisations of real-valued and extended-real-valued measurability
- Complex Lp classes and Euclidean test-function conventions
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- Finite and countable subadditivity of measures
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
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)