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 general inequalities compare cleanly with the published finite ones
The probability-space inequalities above recover the published finite statements exactly in the Markov, Chebyshev, and Cauchy-Schwarz cases, and they isolate the precise extra nonnegativity needed for the positive-probability bound.
- Markov's inequality for random variables restricts to Markov's inequality on a finite probability space.
- Chebyshev's inequality for random variables restricts to Chebyshev's inequality on a finite probability space.
- Cauchy-Schwarz for random variables restricts to Cauchy-Schwarz for finite random variables: .
- The second-moment lower bound for positive probability gives the nonnegative specialization of The finite second-moment bound when , with in place of .
The earlier finite proofs remain the canonical finite arguments. The present page packages them as consequences of the general integral theory on a probability space.
Depends on
- Markov's inequality for random variables
- Chebyshev's inequality for random variables
- Cauchy-Schwarz for random variables
- The second-moment lower bound for positive probability
- Markov's inequality on a finite probability space
- Chebyshev's inequality on a finite probability space
- Cauchy-Schwarz for finite random variables: $\mathbb E[XY]^2\le\mathbb E[X^2]\mathbb E[Y^2]$
- The finite second-moment bound $\mathbb P(X\ne0)\ge\mathbb E[X]^2/\mathbb E[X^2]$ when $\mathbb E[X^2]>0$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
19 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
- Rick Durrett, Probability: Theory and Examples, 5th ed., Section 1.6.1 (standard reference, not scraped)