Union-bound principle (probabilistic method)
ProvedErdos1947.exists_avoiding_allcombinatoricsprobabilistic-methodunion-bound
The finite form of the probabilistic method. Let be a finite outcome space and let be a finite family of "bad events" indexed by . If the total number of outcomes ruled out by all bad events together is strictly smaller than the number of outcomes,
then some outcome avoids every bad event: . This is the union bound in its counting avatar — when the bad events do not cover the space, a good outcome exists. It is the reusable engine of every probabilistic-method existence proof, including the Ramsey lower bound of this mission.
Preamble
import Mathlib open scoped BigOperators
Formal statement
namespace Erdos1947
open scoped BigOperators
/-- **Probabilistic-method principle (union bound).** If the total number of
outcomes ruled out by all "bad events" combined is strictly smaller than the
total number of outcomes, then some outcome avoids every bad event:
$$\sum_{i} |\{\omega : \mathrm{bad}\ i\ \omega\}| < |\alpha| \implies \exists \omega,\ \forall i,\ \neg \mathrm{bad}\ i\ \omega.$$
This is the finite form of the probabilistic method used by Erdős: an outcome
space with total bad mass below 1 cannot be fully covered. -/
theorem exists_avoiding_all {ι α : Type} [Fintype ι] [Fintype α]
(bad : ι → α → Prop) [∀ i : ι, DecidablePred (bad i)]
(hsum : (Finset.univ : Finset ι).sum
(fun i : ι => ((Finset.univ : Finset α).filter (fun ω : α => bad i ω)).card) <
Fintype.card α) :
∃ ω : α, ∀ i : ι, ¬ bad i ω := by
sorry
end Erdos1947Source
Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4) (1947) 292–294, https://doi.org/10.1090/S0002-9904-1947-08785-X — main construction (the lower bound R(k) > 2^(k/2)).
Human review
Confirmed by the mission captain (proposal self-audit).