ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck pass

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]

Expectation is linear on finite sums on the finite retention probability space. (Expectation is linear for every finite family of random variables, without any independence hypothesis)

[L3]

Each retention indicator has expectation equal to its event probability; the product of two indicators is the indicator of their intersection. (Indicators turn event probabilities, intersections, and finite counts into expectations and products)

[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.1L1

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

1.2L1L2L3algebra

Write $I_{i}$ for the indicator that element $i$ is retained, so $X = \sum_{i < n} I_{i}$ . By [L3], $I_{i}^{2} = I_{i}$ and $E I_{i} = p$ ; for distinct $i, j$ , [L1] and [L3] give $E [I_{i} I_{j}] = P (I_{i} = I_{j} = 1) = p^{2}$ . Finite linearity [L2] therefore gives $E X = n p$ , and expanding the finite square gives $E [X^{2}] = \sum_{i < n} E I_{i} + \sum_{i \neq j} E [I_{i} I_{j}] = n p + n (n - 1) p^{2} = n p (1 - p) + n^{2} p^{2} .$ There are $n (n - 1)$ ordered distinct pairs; when $n = 0$ or $n = 1$ that pair sum is empty.

2.1assume-case zeroL1step 1.2

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.

2.2assume-case positivestep 1.1step 1.2L4algebra

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)$ .

3.1step 2.1step 2.2cases-exhaustive∎

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$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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, Chapter 3 (standard reference, not scraped)