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.
Conditional lp contraction
Statement
Assume AC. For , conditional expectation is a linear map from real to real satisfying .
Facts & Assumptions
Given: AC, , real , and a conditioning sub-sigma-algebra G.
On a finite measure space, higher Lp spaces and L-infinity embed in . (Finite-measure includes into for )
is finite Borel convex for every finite . (Absolute real powers are Borel measurable and convex)
Conditional Jensen applies when X and the finite convex function of X are integrable. (Conditional jensen inequality)
Conditional expectation is linear, preserves expectation and order, and satisfies the modulus bound. (Basic algebra and order properties of conditional expectation)
Lp elements are almost-everywhere classes of measurable representatives. (The space as the quotient by null functions)
Proof
For , [F1] with makes integrable; for it is integrable by assumption. Put . For finite , [F2] supplies the convex Borel function and supplies its integrability. Jensen yields . Taking expectations using [F4] gives and hence the norm inequality by taking the increasing positive pth root. At this is also the modulus estimate of [F4].
If , let . The inequalities for all positive integers hold outside a common null set; their limit gives almost surely. Conditional order and constants imply almost surely. Thus . Equality of input representatives preserves the conditional class, so the maps are well defined on [F5]; linearity is [F4].
Source notes
Durrett Theorem 4.1.11 and proof, printed pp.211–212; van der Vaart Lemma 1.9(vii), printed p.4. The infinite endpoint uses the essential bound directly.
Depends on
Used by
Dependency tree · two levels
36 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
- Durrett, Probability: Theory and Examples, 5th ed. (standard reference, not scraped)