LeanPool.AsymptoticTrianglePacking.Internal — Module C4b-0 : the conflict count of an edge

(deterministic)

Standalone, Mathlib-only. Foundation for the Rödl-nibble project.

In one nibble round an edge e is placed in the matching iff it is retained and none of its conflicting edges (other edges sharing a vertex with e) is retained. The number of conflicting edges controls the correlation between "e survives" events; this module bounds it deterministically.

• conflicts H e — the edges of H other than e that meet e.
• conflicts_card_le — |conflicts H e| ≤ ∑_{x∈e} deg x.
• conflicts_card_le_of_uniform — for an r-uniform hypergraph with max degree ≤ Δ, |conflicts H e| ≤ r · Δ.

Definitions (degree, IsUniform) come from LeanPool.AsymptoticTrianglePacking.Internal.Basic. Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

def Hypergraph.conflicts {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (e : Finset V) : Finset (Finset V)

The conflict set of an edge e: the other edges of H that meet e.

Equations

• Hypergraph.conflicts H e = {f ∈ H | f ≠ e ∧ (e ∩ f).Nonempty}

theorem Hypergraph.conflicts_card_le {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (e : Finset V) : (conflicts H e).card ≤ ∑ x ∈ e, degree H x

C4b-0a — conflict-count bound by degrees. |conflicts H e| ≤ ∑_{x∈e} deg x.

theorem Hypergraph.conflicts_card_le_of_uniform {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r Δ : ℕ} (hr : IsUniform H r) (hΔ : ∀ (x : V), degree H x ≤ Δ) {e : Finset V} (he : e ∈ H) : (conflicts H e).card ≤ r * Δ

C4b-0b — conflict-count bound for a regular uniform hypergraph. If H is r-uniform and every vertex has degree ≤ Δ, then every edge conflicts with at most r · Δ others.