LeanPool.AsymptoticTrianglePacking.Internal — deterministic pruning counts

Each nibble round produces a small set B of vertices whose safe degree left the target band; the tight-band invariant is restored by DELETING them (and the edges through them). Deleting B costs every other vertex the edges it shares with B, and this file bounds that cost:

• card_edges_meeting_le — at most |B|·Δ edges meet B;
• card_heavyLoss_le — at most r·|B|·Δ/t vertices lose ≥ t edges to the deletion;
• degree_prune_ge — the degree in the pruned hypergraph is the old degree minus the lost edges.

Pure Finset combinatorics, no probability. placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

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

The edges lost at v when the vertex set B is deleted.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.lostDegree H B v = {e ∈ H | v ∈ e ∧ ¬Disjoint e B}.card

def LeanPool.AsymptoticTrianglePacking.Internal.prune {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (B : Finset V) : Finset (Finset V)

The hypergraph with all edges meeting B removed.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.prune H B = {e ∈ H | Disjoint e B}

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_edges_meeting_le {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {Δ : ℕ} (hΔ : ∀ (x : V), Hypergraph.degree H x ≤ Δ) (B : Finset V) : {e ∈ H | ¬Disjoint e B}.card ≤ B.card * Δ

At most |B|·Δ edges meet B.

theorem LeanPool.AsymptoticTrianglePacking.Internal.degree_prune_ge {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} (B : Finset V) (v : V) : Hypergraph.degree H v ≤ Hypergraph.degree (prune H B) v + lostDegree H B v

Pruning splits the degree.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_heavyLoss_le {V : Type u_1} [DecidableEq V] [Fintype V] {H : Finset (Finset V)} {r Δ : ℕ} (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (x : V), Hypergraph.degree H x ≤ Δ) (B : Finset V) (t : ℕ) : {v : V | t ≤ lostDegree H B v}.card * t ≤ r * (B.card * Δ)

Few vertices lose many edges. At most r·|B|·Δ/t vertices lose ≥ t edges when B is deleted.