CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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.

$P (X = 0) \leq Var (X) / E [X]^{2}$ whenever $E [X] \neq 0$

Statement

If $X$ is a finite real random variable with $E [X] \neq 0$ , then $P (X = 0) \leq \frac{Var (X)}{E [X]^{2}} .$ Equivalently, $P (X \neq 0) \geq 1 - \frac{Var (X)}{E [X]^{2}} .$

Facts & Assumptions

Given: A finite real random variable $X$ with $E [X] \neq 0$ .

[L1]

Chebyshev gives $P (∣ X - E [X] ∣ \geq t) \leq Var (X) / t^{2}$ for $t > 0$ (Chebyshev's inequality on a finite probability space).

Proof

technique · direct

1.1

If $X = 0$ , then $∣ X - E [X] ∣ = ∣ E [X] ∣$ , and the latter is positive. Thus ${X = 0} \subseteq {∣ X - E [X] ∣ \geq ∣ E [X] ∣}$ .

given

2.1

Apply [L1] at $t = ∣ E [X] ∣$ and use $t^{2} = E [X]^{2}$ to obtain the first inequality.

step 1.1L1algebra

3.1

Taking complements gives the equivalent lower bound. The assumption $E [X] \neq 0$ is exactly what makes the threshold positive and the denominator nonzero.

step 2.1algebra∎

Depends on

Chebyshev's inequality on a finite probability space

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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

Y. Zhao, MIT 18.218 Probabilistic Method in Combinatorics, Section 3.3 (standard reference, not scraped)
H. Pishro-Nik, Introduction to Probability, Statistics, and Random Processes, Section 6.2.2 (standard reference, not scraped)

P(X=0)≤Var⁡(X)/E[X]2P(X=0)≤Var(X)/E[X]2 whenever E[X]≠0E[X]=0