LeanPool.AsymptoticTrianglePacking.Internal — the SHARP one-round covering probabilities

Standalone, Mathlib-only. This file supplies the sharp first-moment brick of one nibble round, the one the loose brackets residual_degree_expectation_lower (deg·(1 − rΔp)) and residual_degree_expectation_upper (deg·(1 − p(1−p)^{rΔ})) fail to give: the covering probability of a vertex is computed EXACTLY, and the survival probability of an edge is sandwiched between two expressions that agree to second order.

• coverRate H p x — the exact one-round covering rate ∑_{f ∋ x} p(1−p)^{c(f)} of a vertex.
• prob_vertex_covered_eq — ℙ(x covered) = coverRate H p x. The point: the events "f is in the round matching", for the edges f ∋ x, are pairwise DISJOINT (a matching has at most one edge at x), so the union bound prob_vertex_covered is in fact an equality.
• measureReal_biUnion_ge_bonferroni — the second Bonferroni inequality for a Finset-indexed family (not in Mathlib): ℙ(⋃ᵢ Aᵢ) ≥ ∑ᵢ ℙ(Aᵢ) − ∑ᵢ∑_{j≠i} ℙ(Aᵢ ∩ Aⱼ).
• prob_two_vertices_covered_le — ℙ(x covered ∧ y covered) ≤ deg(x)·deg(y)·p² + codeg(x,y)·p for x ≠ y: the second-order term is quadratically small in the nibble regime p ≈ γ/(rd) as soon as the codegree is o(d).

placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

The exact covering rate of a vertex

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.coverRate {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (p : ℝ) (x : V) : ℝ

The exact one-round covering rate of a vertex. ∑_{f ∋ x} p·(1−p)^{c(f)}, where c(f) is the number of edges conflicting with f. By prob_vertex_covered_eq this is exactly the probability that x is covered by the round matching.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.coverRate H p x = ∑ f ∈ H with x ∈ f, p * (1 - p) ^ (Hypergraph.conflicts H f).card

theorem LeanPool.AsymptoticTrianglePacking.Internal.coverRate_nonneg {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (x : V) : 0 ≤ coverRate H p x

theorem LeanPool.AsymptoticTrianglePacking.Internal.coverRate_le {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (x : V) : coverRate H p x ≤ ↑(Hypergraph.degree H x) * p

The covering rate is at most deg(x)·p.

theorem LeanPool.AsymptoticTrianglePacking.Internal.vertexCovered_eq_biUnion {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (x : V) : {ω : Ω | x ∈ Hypergraph.covered (retainedSet H ρ ω)} = ⋃ f ∈ {f ∈ H | x ∈ f}, {ω : Ω | f ∈ Hypergraph.roundMatching (retainedSet H ρ ω)}

The covering event of a vertex is the (disjoint) union of the matching events of the edges through it.

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_vertex_covered_eq {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (x : V) : MeasureTheory.volume.real {ω : Ω | x ∈ Hypergraph.covered (retainedSet H ρ ω)} = coverRate H p x

The exact per-vertex covering probability. ℙ(x covered) = ∑_{f ∋ x} p(1−p)^{c(f)}. Equality (not just the union bound prob_vertex_covered) because the matching events of the edges through x are pairwise disjoint.

A Bonferroni inequality

theorem LeanPool.AsymptoticTrianglePacking.Internal.measureReal_biUnion_ge_bonferroni {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {ι : Type u_3} [DecidableEq ι] (s : Finset ι) (A : ι → Set Ω) (hA : ∀ (i : ι), MeasurableSet (A i)) : ∑ i ∈ s, MeasureTheory.volume.real (A i) - ∑ i ∈ s, ∑ j ∈ s.erase i, MeasureTheory.volume.real (A i ∩ A j) ≤ MeasureTheory.volume.real (⋃ i ∈ s, A i)

The second Bonferroni inequality for a Finset-indexed family of measurable sets: ℙ(⋃ᵢ Aᵢ) ≥ ∑ᵢ ℙ(Aᵢ) − ∑ᵢ ∑_{j ≠ i} ℙ(Aᵢ ∩ Aⱼ). (Mathlib has the union bound but not this complementary direction.)

Two vertices covered simultaneously

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_two_retained {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {f g : Finset V} (hf : f ∈ H) (hg : g ∈ H) (hne : f ≠ g) : MeasureTheory.volume (ρ.A f ∩ ρ.A g) = ENNReal.ofReal p * ENNReal.ofReal p

Two distinct edges are retained simultaneously with probability p² (pairwise independence).

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_two_vertices_covered_le {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (x y : V) : MeasureTheory.volume.real ({ω : Ω | x ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | y ∈ Hypergraph.covered (retainedSet H ρ ω)}) ≤ ↑(Hypergraph.degree H x) * ↑(Hypergraph.degree H y) * p ^ 2 + ↑(Hypergraph.codegree H x y) * p

A second-order bound on the joint covering probability. For x ≠ y, ℙ(x covered ∧ y covered) ≤ deg(x)·deg(y)·p² + codeg(x,y)·p. In the nibble regime p = γ/(r d) with degrees ≈ d and codegree ≤ μd this is O(γ²/r² + μγ/r), i.e. genuinely of second order against the first-order covering rate ≈ γ/r.