LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Overlap control gives a union lower bound

Statement

Let $B_{1}, \dots, B_{m}$ be finitely many events in a probability space, put $S : = \sum_{i = 1}^{m} \Pr [B_{i}]$ , and suppose that for a real number $C \geq 0$ $\sum_{1 \leq i < j \leq m} \Pr [B_{i} \cap B_{j}] \leq C S .$ Then $\Pr [⋃_{i = 1}^{m} B_{i}] \geq \frac{S}{1 + 2 C} .$ Both quantities vanish when $S = 0$ ; no hypothesis is imposed on the individual probabilities beyond $S < \infty$ , and the bound is uniform over all finite families with the stated overlap ratio.

Facts & Assumptions

Given: events $B_{1}, \dots, B_{m}$ on a probability space, the sum $S = \sum_{i} \Pr [B_{i}]$ , and a real $C \geq 0$ with $\sum_{i < j} \Pr [B_{i} \cap B_{j}] \leq C S$ .

[L1]

For vectors $u, v$ in a real or complex inner product space, $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ ; applied to the indicator functions of two events in $L^{2}$ of a finite probability space this is the inequality $E [∣ X Y ∣] \leq \sqrt{E [X^{2}] E [Y^{2}]}$ for random variables, and for a nonnegative integer-valued $N$ it gives $(E N)^{2} \leq \Pr [N > 0] E [N^{2}]$ , since $N = 0$ off the event ${N > 0}$ (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

Proof

technique · direct

1.1

Let $N : = \sum_{i = 1}^{m} 1_{B_{i}}$ count the events that occur. Then $N \geq 0$ is integer valued, with $E N = \sum_{i} \Pr [B_{i}] = S$ by linearity of expectation, and ${N > 0} = ⋃_{i} B_{i}$ .

givenalgebra

2.1

Expanding the square, $N^{2} = \sum_{i} 1_{B_{i}} + 2 \sum_{i < j} 1_{B_{i} \cap B_{j}}$ , so taking expectations and using the hypothesis gives $E N^{2} = S + 2 \sum_{i < j} \Pr [B_{i} \cap B_{j}] \leq S + 2 C S = (1 + 2 C) S$ , a finite bound.

step 1.1algebra

3.1

If $S = 0$ then $E N = 0$ with $N \geq 0$ , so every $\Pr [B_{i}] = 0$ , $N = 0$ almost surely, and both sides of the claimed inequality are zero; assume $S > 0$ from now on. Applying [L1] to $N$ and to the indicator of ${N > 0}$ gives $S^{2} = (E N)^{2} \leq \Pr [N > 0] E N^{2} \leq \Pr [N > 0] (1 + 2 C) S$ . Dividing by the positive number $(1 + 2 C) S$ gives $\Pr [⋃_{i} B_{i}] = \Pr [N > 0] \geq S / (1 + 2 C)$ , which is the claim.

step 1.1step 2.1L1algebra∎

Remarks

The hypothesis is a ratio condition, not a smallness condition on the intersections separately: the bound is useful exactly when $C$ is uniformly bounded, and then it loses only the factor $1 + 2 C$ relative to the first moment $S$ .
The Arora-Barak form of the same estimate (Claim 18.34) counts elements of finite sets, makes $2 C$ copies of each element and reduces to inclusion-exclusion, with the weaker constant $\frac{1}{4}$ and a hypothesis on the diameter of the set system; the probabilistic second-moment computation above is the convention of this page, and it applies directly to the events $B_{j, f}$ of Powering amplifies a small unsatisfaction gap, whose pair overlaps are controlled by Violated-edge positions have controlled collisions.
The constant is sharp already for two disjoint events: then $C = 0$ , $S = \Pr [B_{1}] + \Pr [B_{2}]$ and the union has probability exactly $S$ .

Depends on

Cauchy–Schwarz: $|\langle u,v\rangle|\leq\lVert u\rVert\lVert v\rVert$, with equality exactly for linearly dependent vectors

Used by

Powering amplifies a small unsatisfaction gap Lemma

Dependency tree · two levels

6 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

Arora and Barak, Computational Complexity: A Modern Approach, §18.5.1 Claim 18.34 and its counting proof, printed pp. 376-377. (standard reference, not scraped)
Irit Dinur, The PCP theorem by gap amplification, §6 equation (7) and Fact 2.6, printed pp. 21-22. (standard reference, not scraped)