BKLO Lemma 10.7 for matchings

This file proves the r = 2 specialization of the simultaneous factor-selection step in Lemma 10.7 of Barber--Kühn--Lo--Osthus, Edge-decompositions of graphs with high minimum degree, Adv. Math. 288 (2016), 337--385.

In the configuration used here, each x ∈ U indexes the induced graph on its neighbourhood in W. Under the parity, minimum-degree, codegree, and incidence hypotheses below, these graphs admit perfect matchings whose edge sets are pairwise disjoint. The published argument uses a randomized greedy process. The formal proof instead uses the deterministic pessimistic-estimator sweep in BKLOSelection.

A largeness threshold

theorem BKLOK2.exists_threshold_sq_le_exp {a : ℝ} (ha : 0 < a) {k : ℕ} (hk : 0 < k) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → ↑n ^ 2 ≤ Real.exp (a * (↑n / ↑k - 1))

For any a > 0 and k ≥ 1, the exponential exp (a (n / k - 1)) eventually dominates n².

Parameter bookkeeping

theorem BKLOK2.codeg_budget_of_hyps {V : Type} [DecidableEq V] {ρ t q : ℝ} {k s₂ : ℕ} {H : Finset (Sym2 V)} {U W : Finset V} (hkR : 0 < ↑k) (hqpos : 0 < q) (hst : √ρ * t = ρ ^ 2) (hq : q = 2 * √ρ / (9 * ↑k)) (hs₂ : s₂ = ⌊9 * ↑k * t * ↑W.card⌋₊) (hiii : ∀ x ∈ U, ∀ x' ∈ U, x ≠ x' → ↑(codegTo H x x' W) ≤ 2 * ρ ^ 2 * ↑W.card) (x : V) : x ∈ U → ∀ x' ∈ U, x ≠ x' → ↑(codegTo H x x' W) ≤ q * (↑s₂ + 1)

With q = 2√ρ/(9k), the codegree hypothesis fits the spread-selection budget.

theorem BKLOK2.pot_empty_lt_of_hyps {V : Type} [DecidableEq V] {ρ t q : ℝ} {k s : ℕ} {H : Finset (Sym2 V)} {S U W : Finset V} (hkR : 0 < ↑k) (hk1 : 1 ≤ ↑k) (hqpos : 0 < q) (htpos : 0 < t) (hts : t = ρ * √ρ) (hq : q = 2 * √ρ / (9 * ↑k)) (hs : s = ⌊9 * ↑k * t * ↑W.card⌋₊) (hUS : U ⊆ S) (hWS : W ⊆ S) (hiv : ∀ y ∈ W, ↑(degTo H y U) ≤ 2 * ↑k * ρ * ↑W.card) (hSsq : ↑S.card ^ 2 ≤ Real.exp (t * ↑W.card)) : pot H W q ∅ U < 2 ^ (s + 1)

The empty-state pessimistic potential is smaller than the available matching supply.

The r = 2 simultaneous factor theorem

theorem BKLOK2.lemma107K2_holds (ρ : ℝ) (k : ℕ) : 0 < ρ → 0 < k → ∃ (n₀ : ℕ), ∀ {V : Type} [inst : DecidableEq V] (H : Finset (Sym2 V)) (S U W : Finset V), n₀ ≤ S.card → (∀ e ∈ H, ¬e.IsDiag) → H ⊆ cliqueEdges S → U ⊆ S → W ⊆ S → Disjoint U W → ↑S.card / ↑k - 1 ≤ ↑W.card → (∀ x ∈ U, 2 ∣ degTo H x W) → (∀ x ∈ U, ∀ y ∈ nbhdIn H x W, 1 / 2 * ↑(degTo H x W) + 18 * ↑k * √ρ ^ 3 * ↑W.card ≤ ↑(degTo H y (nbhdIn H x W))) → (∀ x ∈ U, ∀ x' ∈ U, x ≠ x' → ↑(codegTo H x x' W) ≤ 2 * ρ ^ 2 * ↑W.card) → (∀ y ∈ W, ↑(degTo H y U) ≤ 2 * ↑k * ρ * ↑W.card) → ∃ (Mx : V → Finset (Finset V)), (∀ x ∈ U, GoodMatching H W x (Mx x)) ∧ (↑U).Pairwise fun (x y : V) => Disjoint (famEdges (Mx x)) (famEdges (Mx y))

BKLO Lemma 10.7, specialized to r = 2 and indexed by apex neighbourhoods.

For all sufficiently large configurations, the neighbourhood graph associated with each apex x ∈ U has a perfect matching, and all the chosen matching edge sets are pairwise disjoint. The four substantive assumptions are parity, a Dirac condition with quantitative slack, a pairwise codegree bound, and a vertex-incidence bound.