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.
Marcinkiewicz interpolation from weak and strong
Statement
Let be a measure space, let be a sublinear operator on measurable functions, and suppose:
- is of weak type with constant ;
- is of strong type with constant .
Then for every and every , In particular, is of strong type for every .
Facts & Assumptions
Given: A measure space , a sublinear operator , constants , an exponent , and a function .
Sublinearity, weak type , and strong type are as defined in Sublinear operators and weak or strong type bounds.
The distribution function of a measurable function is (The distribution function of absolute value)
For , for every measurable . (For 0 < p < infinity, the layer-cake formula computes the integral of |f|^p from the distribution function)
Proof
Fix and , and put . Since the strong [L1, given, construct, algebra] bound with constant also holds with the larger constant , split Sublinearity gives Since , the strong bound with constant yields Therefore
Apply the weak bound to : [L1, step 1.1, algebra]
Using [L3] with and then step 2.1, [L2, L3, step 2.1, algebra]
The integrand in step 3.1 is nonnegative, so Tonelli's theorem for [step 3.1, algebra] nonnegative integrals lets us swap the order: Because , so
Taking th roots in step 4.1 gives [step 4.1, algebra] Because was arbitrary, letting yields Thus is of strong type for every .
Depends on
Used by
Dependency tree · two levels
11 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 B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., Theorem 6.28 (standard reference, not scraped)
- Richard F. Bass, Real Analysis for Graduate Students, Chapter 24.1 (standard reference, not scraped)