LeanPool.AsymptoticTrianglePacking.Internal — the LINEAR sandwich for the safe degree

The safe degree safeDegree H C v (LeanPool.AsymptoticTrianglePacking.Internal.SafeDegree) is a nonlinear functional of the covered set C — it counts the edges at v none of whose other vertices is covered. Its concentration is obtained here by sandwiching it between two quantities that are LINEAR (resp. quadratic) in the covering indicators, which are the objects whose moments the exact one-round covering law (LeanPool.AsymptoticTrianglePacking.Internal.prob_vertex_covered_eq, LeanPool.AsymptoticTrianglePacking.Internal.prob_two_vertices_covered_le) controls:

• coverWeight H v C = ∑_{u ∈ C, u ≠ v} codeg(v,u) = ∑_{e ∋ v} |(e∖v) ∩ C| — the loss weight;
• pairWeight H v C = ∑_{e ∋ v} C(|(e∖v) ∩ C|, 2) — the Bonferroni correction.

The sandwich reads

deg(v) ≤ safeDeg(v) + coverWeight (degree_le_safeDegree_add_coverWeight), safeDeg(v) + coverWeight ≤ deg(v) + pairWeight (safeDegree_add_coverWeight_le),

i.e. the loss deg(v) − safeDeg(v) is squeezed between coverWeight − pairWeight and coverWeight. Since coverWeight is a nonnegative combination ∑_u codeg(v,u)·1[u covered] of the covering indicators, its mean and variance are directly computable, and pairWeight has a small mean; this is what makes the SAFE degree concentrate where the residual degree cannot.

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

def LeanPool.AsymptoticTrianglePacking.Internal.coverWeight {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (C : Finset V) : ℕ

The loss weight of v against a covered set C: ∑_{u ∈ C, u ≠ v} codeg(v,u).

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.coverWeight H v C = ∑ u ∈ C.erase v, Hypergraph.codegree H v u

def LeanPool.AsymptoticTrianglePacking.Internal.pairWeight {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (C : Finset V) : ℕ

The Bonferroni correction: ∑_{e ∋ v} C(|(e∖v) ∩ C|, 2).

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.pairWeight H v C = ∑ e ∈ H with v ∈ e, (e.erase v ∩ C).card.choose 2

theorem LeanPool.AsymptoticTrianglePacking.Internal.coverWeight_eq_sum {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (C : Finset V) : coverWeight H v C = ∑ e ∈ H with v ∈ e, (e.erase v ∩ C).card

coverWeight counted edge-by-edge: ∑_{e ∋ v} |(e∖v) ∩ C|.

theorem LeanPool.AsymptoticTrianglePacking.Internal.degree_eq_safeDegree_add {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (C : Finset V) : Hypergraph.degree H v = safeDegree H C v + {e ∈ {e ∈ H | v ∈ e} | ¬Disjoint (e.erase v) C}.card

The edges at v are split by safety.

theorem LeanPool.AsymptoticTrianglePacking.Internal.unsafe_iff_inter_nonempty {V : Type u_1} [DecidableEq V] {e : Finset V} {v : V} {C : Finset V} : ¬Disjoint (e.erase v) C ↔ 0 < (e.erase v ∩ C).card

An edge at v is unsafe exactly when it meets C outside v.

theorem LeanPool.AsymptoticTrianglePacking.Internal.degree_le_safeDegree_add_coverWeight {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (C : Finset V) : Hypergraph.degree H v ≤ safeDegree H C v + coverWeight H v C

Sandwich, lower half. deg(v) ≤ safeDeg(v) + coverWeight.

theorem LeanPool.AsymptoticTrianglePacking.Internal.nat_le_indicator_add_choose_two (m : ℕ) : m ≤ (if 0 < m then 1 else 0) + m.choose 2

The elementary Bonferroni step: m ≤ 1[m ≥ 1] + C(m,2).

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_add_coverWeight_le {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (C : Finset V) : safeDegree H C v + coverWeight H v C ≤ Hypergraph.degree H v + pairWeight H v C

Sandwich, upper half. safeDeg(v) + coverWeight ≤ deg(v) + pairWeight.