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.
Vanishing tail control bounds truncated second moments
Statement
Let be a real random variable with as positive integers . Then for real , and Moreover for every .
Facts & Assumptions
Zero truncation at a positive level: For a real random variable and a deterministic level , its zero truncation is The threshold event is measurable because is measurable and is Borel; its indicator and the product are measurable by thm-arithmetic-and-lattice-operations-preserve-measurability. Thus is a real random variable as in def-random-element-and-real-random-variable. It equals at both cutoff endpoints and is zero outside the interval. Since , for every its absolute th moment is at most . This is not clipping to the endpoints.
For 0 < p < infinity, the layer-cake formula computes the integral of |f|^p from the distribution function: Let be a measure space, let be measurable, and let . Then where either side may be .
Proof
Given: The objects and hypotheses of the statement.
For , put . Monotonicity of the tail gives , which tends to zero. Consequently is bounded on and tends to zero.
Apply layer cake with exponent to . Its tail is at most that of for and is zero for . Thus its second moment is at most . If for , division by bounds this by for . Let then . No moment assumption on the untruncated square was used.
For , layer cake gives . On this is at most . If , the remaining integral is at most . This also covers and bounded laws. Neither endpoint p=0 nor p=1 is asserted.
Depends on
Used by
Dependency tree · two levels
10 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
- Theorem 2.2.12 proof with Lemma 2.2.13, pp. 63–64 (standard reference, not scraped)