Perfect and near-perfect matchings from high minimum degree

A finite simple graph whose minimum degree is at least half the number of vertices contains a perfect matching when its order is even and a near-perfect matching when its order is odd. The results are stated in the idiomatic SimpleGraph.Subgraph matching vocabulary.

Main results

• SimpleGraph.exists_isPerfectMatching_of_minDegree: if V has an even number of vertices and |V| ≤ 2 · δ(G), then G has a perfect matching (Subgraph.IsPerfectMatching).
• SimpleGraph.exists_isMatching_compl_singleton_of_minDegree: if V has an odd number of vertices and |V| ≤ 2 · δ(G) + 1, then G has a matching covering all but exactly one vertex, i.e. a matching M whose vertex set is the complement {w}ᶜ of a single vertex w (a near-perfect matching).

Implementation notes

The even case reuses the finite-set augmentation theorem from Spread. The odd case is reduced to it by adjoining a universal apex vertex and deleting that vertex from the resulting perfect matching. Both public formulations therefore share one proof of the degree criterion.

theorem SimpleGraph.exists_isPerfectMatching_of_minDegree {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (heven : Even (Fintype.card V)) (hδ : Fintype.card V ≤ 2 * G.minDegree) : ∃ (M : G.Subgraph), M.IsPerfectMatching

Dirac-type perfect matching (even case). A finite simple graph on an even number of vertices whose minimum degree satisfies |V| ≤ 2 · δ(G) has a perfect matching.

theorem SimpleGraph.exists_isMatching_compl_singleton_of_minDegree {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hodd : Odd (Fintype.card V)) (hδ : Fintype.card V ≤ 2 * G.minDegree + 1) : ∃ (M : G.Subgraph) (w : V), M.IsMatching ∧ M.verts = {w}ᶜ

Dirac-type near-perfect matching (odd case). A finite simple graph on an odd number of vertices whose minimum degree satisfies |V| ≤ 2 · δ(G) + 1 has a matching covering all but exactly one vertex: there is a vertex w and a matching M with vertex set {w}ᶜ.