ExampleConstruction: AI-adaptedVerification: 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.

First- and second-moment bounds for a nonempty Bernoulli random subset

Example

Retain each element of $[n]$ independently with probability $p$ , and let $X$ be the size of the random subset. Then $E [X] = n p, E [X^{2}] = n p (1 - p) + n^{2} p^{2}, P (X > 0) = 1 - (1 - p)^{n} .$ When $n p > 0$ , the first- and second-moment bounds give $P (X > 0) \leq n p, P (X > 0) \geq \frac{n p}{1 - p + n p} .$

Facts & Assumptions

Given: Naturals $n$ and a real $p \in [0, 1]$ .

[L1]

$X$ is a sum of $n$ mutually independent Bernoulli $(p)$ variables, and mutual independence factors their joint attained-value probabilities (Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials, Pairwise and mutual independence of finite-valued random variables).

[L2]

Its mean and variance are $n p$ and $n p (1 - p)$ (A Bernoulli $(p)$ variable has mean $p$ and variance $p (1 - p)$ ; a binomial $(n, p)$ variable has mean $n p$ and variance $n p (1 - p)$ ).

[L3]

$Var (X) = E [X^{2}] - E [X]^{2}$ ( $Var (X) = E [X^{2}] - E [X]^{2}$ and $Cov (X, Y) = E [X Y] - E [X] E [Y]$ ).

[L4]

Markov and the second-moment theorem give their respective upper and lower bounds (Markov's inequality on a finite probability space, The finite second-moment bound $P (X \neq 0) \geq E [X]^{2} / E [X^{2}]$ when $E [X^{2}] > 0$ ).

Verification

technique · cases

1.1

The event $X = 0$ means every retention coordinate is zero, so $P (X > 0) = 1 - (1 - p)^{n}$ .

1.2

The identity [L3] and [L2] give $E [X^{2}] = n p (1 - p) + n^{2} p^{2}$ .

L2L3algebra

1.3

If $n p = 0$ , then $n = 0$ or $p = 0$ , and $X = 0$ almost surely; all three displayed exact formulas give zero where appropriate, while the second-moment ratio is not formed.

assume-case zeroL1L2

2.1

If $n p > 0$ , Markov at threshold $1$ gives $P (X > 0) \leq n p$ , and the second-moment bound with steps 1.1 and 1.2 gives $P (X > 0) \geq (n p)^{2} / (n p (1 - p) + n^{2} p^{2}) = n p / (1 - p + n p)$ .

assume-case positivestep 1.1step 1.2L4algebra

3.1

The cases are exhaustive. At $p = 1$ and $n > 0$ , the exact probability is $1$ and the second-moment lower bound is $n p / (1 - p + n p) = 1$ , while the Markov upper bound is $n p = n$ and is vacuous for $n \geq 2$ .

step 1.3step 2.1cases-exhaustive∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 36 results over 13 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

Y. Zhao, MIT 18.218 Probabilistic Method in Combinatorics, Chapter 3 (standard reference, not scraped)