Spread perfect matchings in Dirac graphs

Let N be a finite set of vertices of even cardinality in a simple graph G, and suppose that the Dirac condition with slack t holds: every vertex of N has at least |N| / 2 + t neighbours inside N.

Deleting the edges of a perfect matching of N drops each such degree by exactly one, so Dirac's theorem can be applied t + 1 times in a row: G contains t + 1 perfect matchings of N which are pairwise edge-disjoint (SimpleGraph.exists_involutions_pairwise_ne). Averaging over these t + 1 matchings, one of them has weight at most a 1 / (t + 1) fraction of the total weight against any prescribed nonnegative weight function: this is the spread property recorded in SimpleGraph.exists_spread_involution, and it is a deterministic substitute for the usual "a random perfect matching is spread" argument.

Main results

• SimpleGraph.exists_involution_adj: Dirac's theorem for perfect matchings, in the form of a fixed-point-free involution of N all of whose orbits are edges of G.
• SimpleGraph.exists_isPerfectMatching_of_card_le_minDegree: Dirac's theorem for a finite graph with an even number of vertices, phrased with SimpleGraph.Subgraph.IsPerfectMatching.
• SimpleGraph.exists_involutions_pairwise_ne: the Dirac condition with slack t produces t + 1 pairwise edge-disjoint perfect matchings of N.
• SimpleGraph.exists_spread_involution: the Dirac condition with slack t produces a perfect matching of N of weight at most 1 / (t + 1) times the total weight.

Implementation notes

Perfect matchings of a finite set N of vertices are presented as partner involutions: functions f : V → V mapping N to itself, involutive on N, without fixed points on N, and with G.Adj a (f a) for every a ∈ N. This presentation makes both edge-disjointness (f i a ≠ f j a) and the weight of a matching (∑ y ∈ N, w y (f y)) easy to state. The translation to SimpleGraph.Subgraph.IsPerfectMatching is SimpleGraph.exists_isPerfectMatching_of_involutive.

Dirac's theorem itself is proved from scratch, by the standard maximum-matching argument: if a matching of maximum size misses two vertices u, v, then all neighbours of u and of v are matched, and no matched edge x, f x has u adjacent to x and v adjacent to f x (otherwise the matching could be augmented), so the partner involution injects the neighbourhood of u into the complement of the neighbourhood of v, contradicting the degree hypothesis.

theorem SimpleGraph.exists_isPerfectMatching_of_involutive {V : Type u_1} {G : SimpleGraph V} {f : V → V} (hinv : ∀ (a : V), f (f a) = a) (hadj : ∀ (a : V), G.Adj a (f a)) : ∃ (M : G.Subgraph), M.IsPerfectMatching ∧ ∀ (a : V), M.Adj a (f a)

A fixed-point-free involution all of whose orbits are edges of G is a perfect matching of G, in the sense of SimpleGraph.Subgraph.IsPerfectMatching.

Matchings of a finite vertex set, as partner involutions

Dirac's theorem and spread matchings for simple graphs

theorem SimpleGraph.exists_spread_involution_of_edgeSet {V : Type u_1} [DecidableEq V] {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {A : Finset (Sym2 V)} {N : Finset V} {t : ℕ} (hEven : Even N.card) (hdeg : ∀ v ∈ N, N.card / 2 + t ≤ ({z ∈ N | s(v, z) ∈ A}.erase v).card) (w : V → V → R) (hw : ∀ (y z : V), 0 ≤ w y z) : ∃ (f : V → V), (∀ a ∈ N, f a ∈ N) ∧ (∀ a ∈ N, f (f a) = a) ∧ (∀ a ∈ N, f a ≠ a) ∧ (∀ a ∈ N, s(a, f a) ∈ A) ∧ ∑ y ∈ N, w y (f y) ≤ 1 / (↑t + 1) * ∑ y ∈ N, ∑ z ∈ N, w y z

Spread perfect matchings for a finite edge set. This is the edge-set interface used by the simultaneous matching selection in the r = 2 specialization of BKLO Lemma 10.7. Under a Dirac condition with slack t, it supplies a partner involution whose weight is at most the average weight over the t + 1 edge-disjoint perfect matchings available from that slack.

theorem SimpleGraph.exists_involution_adj {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {N : Finset V} (hEven : Even N.card) (hdeg : ∀ v ∈ N, N.card / 2 ≤ {z ∈ N | G.Adj v z}.card) : ∃ (f : V → V), (∀ a ∈ N, f a ∈ N) ∧ (∀ a ∈ N, f (f a) = a) ∧ (∀ a ∈ N, f a ≠ a) ∧ ∀ a ∈ N, G.Adj a (f a)

Dirac's theorem for perfect matchings. If N is a finite set of vertices of even cardinality such that every v ∈ N has at least |N| / 2 neighbours inside N, then N carries a perfect matching of G, presented as a fixed-point-free partner involution f of N with G.Adj a (f a) for all a ∈ N.

theorem SimpleGraph.exists_involutions_pairwise_ne {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {N : Finset V} {t : ℕ} (hEven : Even N.card) (hdeg : ∀ v ∈ N, N.card / 2 + t ≤ {z ∈ N | G.Adj v z}.card) : ∃ (F : Fin (t + 1) → V → V), (∀ (i : Fin (t + 1)), (∀ a ∈ N, F i a ∈ N) ∧ (∀ a ∈ N, F i (F i a) = a) ∧ (∀ a ∈ N, F i a ≠ a) ∧ ∀ a ∈ N, G.Adj a (F i a)) ∧ ∀ (i j : Fin (t + 1)), i ≠ j → ∀ a ∈ N, F i a ≠ F j a

Dirac's theorem with slack. If every vertex of an even set N has at least |N| / 2 + t neighbours inside N, then G contains t + 1 perfect matchings of N which are pairwise edge-disjoint: distinct matchings assign distinct partners to every vertex of N.

theorem SimpleGraph.exists_spread_involution {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {N : Finset V} {t : ℕ} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (hEven : Even N.card) (hdeg : ∀ v ∈ N, N.card / 2 + t ≤ {z ∈ N | G.Adj v z}.card) (w : V → V → R) (hw : ∀ (y z : V), 0 ≤ w y z) : ∃ (f : V → V), (∀ a ∈ N, f a ∈ N) ∧ (∀ a ∈ N, f (f a) = a) ∧ (∀ a ∈ N, f a ≠ a) ∧ (∀ a ∈ N, G.Adj a (f a)) ∧ ∑ y ∈ N, w y (f y) ≤ 1 / (↑t + 1) * ∑ y ∈ N, ∑ z ∈ N, w y z

Spread perfect matchings from Dirac slack. If every vertex of an even set N has at least |N| / 2 + t neighbours inside N, then for every nonnegative weight function w some perfect matching of N, presented as a partner involution f, has weight at most a 1 / (t + 1) fraction of the total weight: ∑ y ∈ N, w y (f y) ≤ (1 / (t + 1)) * ∑ y ∈ N, ∑ z ∈ N, w y z.

The matching is obtained by averaging over the t + 1 pairwise edge-disjoint perfect matchings supplied by SimpleGraph.exists_involutions_pairwise_ne.

theorem SimpleGraph.exists_isPerfectMatching_of_card_le_minDegree {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] (hEven : Even (Fintype.card V)) (hdeg : Fintype.card V / 2 ≤ G.minDegree) : ∃ (M : G.Subgraph), M.IsPerfectMatching

Dirac's theorem for perfect matchings, for a finite graph with an even number of vertices and minimum degree at least half the number of vertices.