LeanPool.AsymptoticTrianglePacking.Internal — Module A3 : greedy / maximal-matching lower bound

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

Content:

• matching_support_card — a matching in an r-uniform hypergraph covers exactly r · |M| vertices.
• edges_meeting_le — the number of edges meeting a vertex set S is at most ∑_{v∈S} deg v.
• greedy_bound — for a maximal matching M (every edge meets its support) with max degree ≤ Δ, |H| ≤ r · Δ · |M|, i.e. ν(H) ≥ |E| / (rΔ).

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

def Hypergraph.support {V : Type u_1} [DecidableEq V] (M : Finset (Finset V)) : Finset V

The support (vertex set) of a family of edges.

Equations

• Hypergraph.support M = M.biUnion id

theorem Hypergraph.matching_support_card {V : Type u_1} [DecidableEq V] {H M : Finset (Finset V)} {r : ℕ} (hr : IsUniform H r) (hM : IsMatching H M) : (support M).card = r * M.card

A3a — support cardinality. A matching of an r-uniform hypergraph covers exactly r * |M| vertices.

theorem Hypergraph.edges_meeting_le {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (S : Finset V) : {e ∈ H | (e ∩ S).Nonempty}.card ≤ ∑ v ∈ S, degree H v

A3b — edges meeting a set. The number of edges of H meeting a vertex set S is at most ∑_{v ∈ S} degree H v.

theorem Hypergraph.edges_meeting_le_of_not_disjoint {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (S : Finset V) : {e ∈ H | ¬Disjoint e S}.card ≤ ∑ v ∈ S, degree H v

The same incidence bound with meeting expressed as non-disjointness.

theorem Hypergraph.greedy_bound {V : Type u_1} [DecidableEq V] {H M : Finset (Finset V)} {r Δ : ℕ} (hr : IsUniform H r) (hM : IsMatching H M) (hcov : ∀ e ∈ H, (e ∩ support M).Nonempty) (hΔ : ∀ (v : V), degree H v ≤ Δ) : H.card ≤ r * Δ * M.card

A3 — greedy / maximal-matching bound. If M is a matching whose support meets every edge of H (a maximal matching) and every vertex has degree ≤ Δ, then |H| ≤ r · Δ · |M|. Equivalently ν(H) ≥ |E| / (rΔ).