LeanPool.AsymptoticTrianglePacking.Internal — Module C4b-3b (part 1) : probability a vertex is #
covered
Standalone, Mathlib-only. Foundation for the Rödl-nibble project.
Under a Bernoulli retention, a vertex x is covered in a round when it lies in some edge of the
round's matching. Since a matched edge is in particular retained, the covered event is contained in
the union of the retention events of the edges through x; a union bound gives
ℙ(x covered) ≤ deg(x) · p.
This union-bound estimate deliberately sidesteps the delicate correlation structure of the matching
(we only use "matched ⟹ retained"), and feeds the residual-degree mean lower bound
E[deg_residual(v)] ≥ deg(v)·(1 - r·d·p) (module C4b-3b part 2).
retainedSet ρ ω is the (classically decidable) set of retained edges at outcome ω.
Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].
The set of retained edges at outcome ω (classically decidable membership in the events).
Equations
- LeanPool.AsymptoticTrianglePacking.Internal.retainedSet H ρ ω = {e ∈ H | ω ∈ ρ.A e}
Instances For
C4b-3b(1) — vertex-covered probability bound. The probability that a vertex x is covered
by the round's matching is at most deg(x) · p.
C4b-3b(2) — edge-hit probability. The probability that an edge e loses a vertex to the
covered set (so it fails to survive into the residual) is at most ∑_{x∈e} deg(x)·p. Union bound
over the vertices of e of prob_vertex_covered.
C4b-3b(2') — edge-hit probability, regular form. For an r-uniform hypergraph with max
degree ≤ Δ, an edge is hit with probability at most r·Δ·p.