LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Cauchy-Schwarz for finite random variables: $E [X Y]^{2} \leq E [X^{2}] E [Y^{2}]$

Statement

For real random variables $X, Y$ on a finite probability space, $E [X Y]^{2} \leq E [X^{2}] E [Y^{2}] .$ No equality characterization is asserted on outcomes of probability zero.

Facts & Assumptions

Given: Real random variables $X, Y$ on one finite probability space.

[L1]

Expectation is linear for finite linear combinations (Expectation is linear for every finite family of random variables, without any independence hypothesis).

[L2]

Expectation preserves pointwise order, so the expectation of a nonnegative variable is nonnegative (Expectation preserves pointwise order and lies between the minimum and maximum attained values).

[L3]

Expectation is the finite sum of values times nonnegative outcome weights (Expectation of a real random variable on a finite probability space).

Proof

technique · cases

1.1

Assume first that $E [X^{2}] = 0$ . Every nonnegative summand $X (ω)^{2} w (ω)$ is then zero, so $X = 0$ on all positive-weight outcomes and $E [X Y] = 0$ .

assume-case zeroL2L3algebra

1.2

Assume now that $E [X^{2}] > 0$ and put $t = E [X Y] / E [X^{2}]$ .

assume-case positivechoose

1.3

Since $(Y - t X)^{2} \geq 0$ , linearity gives $0 \leq E [Y^{2}] - 2 t E [X Y] + t^{2} E [X^{2}]$ .

L1L2

2.1

In this case the asserted inequality reads $0 \leq 0$ .

step 1.1algebra

2.2

Substitution of $t$ into step 1.3 yields $0 \leq E [Y^{2}] - E [X Y]^{2} / E [X^{2}]$ , and multiplication by the positive denominator gives the result.

step 1.2step 1.3algebra

3.1

The cases $E [X^{2}] = 0$ and $E [X^{2}] > 0$ are exhaustive because $E [X^{2}] \geq 0$ .

step 2.1step 2.2L2cases-exhaustive∎

Depends on

Used by

The finite second-moment bound ℙ(X≠0)geE[X]²/E[X²] when E[X²]>0 Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

H. Pishro-Nik, Introduction to Probability, Statistics, and Random Processes, Section 6.2.4 (standard reference, not scraped)

Cauchy-Schwarz for finite random variables: E[XY]2≤E[X2]E[Y2]E[XY]2≤E[X2]E[Y2]