Deterministic simultaneous matching selection

A pessimistic-estimator sweep chooses perfect matchings in overlapping apex neighbourhoods while keeping all previously selected matching edges disjoint. This is the deterministic core used for the r = 2 specialization of BKLO Lemma 10.7.

The used-degree counter and the potential

def BKLOK2.usedCnt {V : Type u_1} [DecidableEq V] (H : Finset (Sym2 V)) (W : Finset V) (F : Finset (Sym2 V)) (x y : V) : ℕ

The number of edges of the used set F at y lying inside the apex neighbourhood N_H(x,W). This is exactly the amount by which the Dirac degree of y in H[N_H(x,W)] has been eroded.

Equations

• BKLOK2.usedCnt H W F x y = BKLOK2.edeg (BKLOK2.edgesIn F (BKLOK2.nbhdIn H x W)) y

noncomputable def BKLOK2.pot {V : Type u_1} [DecidableEq V] (H : Finset (Sym2 V)) (W : Finset V) (q : ℝ) (F : Finset (Sym2 V)) (R : Finset V) : ℝ

The pessimistic-estimator potential. R is the set of apices not yet processed.

Equations

• BKLOK2.pot H W q F R = ∑ x ∈ R, ∑ y ∈ BKLOK2.nbhdIn H x W, 2 ^ BKLOK2.usedCnt H W F x y * (1 + q) ^ BKLOK2.degTo H y R

noncomputable def BKLOK2.wgt {V : Type u_1} [DecidableEq V] (H : Finset (Sym2 V)) (W : Finset V) (q : ℝ) (F : Finset (Sym2 V)) (R' R : Finset V) (y z : V) : ℝ

The weight function fed to the spread clause at the apex being processed: the potential mass carried by the pair (y, z), i.e. the total over the remaining apices containing both.

Equations

• BKLOK2.wgt H W q F R' R y z = ∑ x ∈ R' with y ∈ BKLOK2.nbhdIn H x W ∧ z ∈ BKLOK2.nbhdIn H x W, 2 ^ BKLOK2.usedCnt H W F x y * (1 + q) ^ BKLOK2.degTo H y R

theorem BKLOK2.wgt_nonneg {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W : Finset V} {q : ℝ} (hq : 0 ≤ q) (F : Finset (Sym2 V)) (R' R : Finset V) (y z : V) : 0 ≤ wgt H W q F R' R y z

theorem BKLOK2.pot_nonneg {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W : Finset V} {q : ℝ} (hq : 0 ≤ q) (F : Finset (Sym2 V)) (R : Finset V) : 0 ≤ pot H W q F R

theorem BKLOK2.pow_usedCnt_le_pot {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W : Finset V} {q : ℝ} (hq : 0 ≤ q) {F : Finset (Sym2 V)} {R : Finset V} {x y : V} (hx : x ∈ R) (hy : y ∈ nbhdIn H x W) : 2 ^ usedCnt H W F x y ≤ pot H W q F R

Every single term of the potential is at most the potential.

theorem BKLOK2.usedCnt_le_of_pot {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W : Finset V} {q : ℝ} (hq : 0 ≤ q) {F : Finset (Sym2 V)} {R : Finset V} {s : ℕ} (hpot : pot H W q F R < 2 ^ (s + 1)) {x y : V} (hx : x ∈ R) (hy : y ∈ nbhdIn H x W) : usedCnt H W F x y ≤ s

The potential controls the used degrees: if Φ < 2 ^ (s+1) then no counter exceeds s.

The step inequality

theorem BKLOK2.usedCnt_union_le {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W : Finset V} (F : Finset (Sym2 V)) {N : Finset V} {f : V → V} (hmap : ∀ a ∈ N, f a ∈ N) (hinv : ∀ a ∈ N, f (f a) = a) (x y : V) : usedCnt H W (F ∪ famEdges (involutionMatching N f)) x y ≤ usedCnt H W F x y + if y ∈ N ∧ y ∈ nbhdIn H x W ∧ f y ∈ nbhdIn H x W then 1 else 0

The used degree inside N_H(x,W) grows by at most one, and only at vertices of the current neighbourhood matched into N_H(x,W).

theorem BKLOK2.nbhdIn_erase {V : Type u_1} [DecidableEq V] (H : Finset (Sym2 V)) (R : Finset V) (x₀ y : V) : nbhdIn H y (R.erase x₀) = (nbhdIn H y R).erase x₀

Deleting an apex from the index set deletes it from every neighbourhood.

theorem BKLOK2.degTo_erase_of_mem_nbhd {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W R : Finset V} {x₀ y : V} (hx₀ : x₀ ∈ R) (hy : y ∈ nbhdIn H x₀ W) : degTo H y R = degTo H y (R.erase x₀) + 1

A vertex of the processed neighbourhood loses exactly one apex.

theorem BKLOK2.degTo_erase_of_notMem_nbhd {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W R : Finset V} {x₀ y : V} (hyW : y ∈ W) (hy : y ∉ nbhdIn H x₀ W) : degTo H y (R.erase x₀) = degTo H y R

A vertex outside the processed neighbourhood loses no apex.

theorem BKLOK2.pot_step_mem_term {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W : Finset V} {q : ℝ} {F : Finset (Sym2 V)} {R : Finset V} {x₀ x y : V} {f : V → V} (hx₀ : x₀ ∈ R) (hmap : ∀ a ∈ nbhdIn H x₀ W, f a ∈ nbhdIn H x₀ W) (hinv : ∀ a ∈ nbhdIn H x₀ W, f (f a) = a) (hq : 0 ≤ q) (hy : y ∈ nbhdIn H x W) (hy0 : y ∈ nbhdIn H x₀ W) : (1 + q) * (2 ^ usedCnt H W (F ∪ famEdges (involutionMatching (nbhdIn H x₀ W) f)) x y * (1 + q) ^ degTo H y (R.erase x₀)) ≤ 2 ^ usedCnt H W F x y * (1 + q) ^ degTo H y R + if f y ∈ nbhdIn H x W then 2 ^ usedCnt H W F x y * (1 + q) ^ degTo H y R else 0

The term bound at a vertex of the neighbourhood being processed: one unit of used degree may be created, and the factor (1+q) released by deleting x₀ from the index set pays for it.

theorem BKLOK2.pot_step_notMem_term {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {W : Finset V} {q : ℝ} {F : Finset (Sym2 V)} {R : Finset V} {x₀ x y : V} {f : V → V} (hmap : ∀ a ∈ nbhdIn H x₀ W, f a ∈ nbhdIn H x₀ W) (hinv : ∀ a ∈ nbhdIn H x₀ W, f (f a) = a) (hq : 0 ≤ q) (hy : y ∈ nbhdIn H x W) (hy0 : y ∉ nbhdIn H x₀ W) : 2 ^ usedCnt H W (F ∪ famEdges (involutionMatching (nbhdIn H x₀ W) f)) x y * (1 + q) ^ degTo H y (R.erase x₀) ≤ 2 ^ usedCnt H W F x y * (1 + q) ^ degTo H y R

The term bound away from the neighbourhood being processed: nothing changes there.

theorem BKLOK2.sum_wgt_partner_eq {V : Type u_1} [DecidableEq V] (H : Finset (Sym2 V)) (W : Finset V) (q : ℝ) (F : Finset (Sym2 V)) (R' R : Finset V) (x₀ : V) (f : V → V) : ∑ y ∈ nbhdIn H x₀ W, wgt H W q F R' R y (f y) = ∑ x ∈ R', ∑ y ∈ nbhdIn H x W with y ∈ nbhdIn H x₀ W, if f y ∈ nbhdIn H x W then 2 ^ usedCnt H W F x y * (1 + q) ^ degTo H y R else 0

Fubini for the partner weight. The mass the sweep pays at the processed apex is exactly the weight of the chosen involution.

theorem BKLOK2.sum_sum_wgt_eq {V : Type u_1} [DecidableEq V] (H : Finset (Sym2 V)) (W : Finset V) (q : ℝ) (F : Finset (Sym2 V)) (R' R : Finset V) (x₀ : V) : ∑ y ∈ nbhdIn H x₀ W, ∑ z ∈ nbhdIn H x₀ W, wgt H W q F R' R y z = ∑ x ∈ R', ↑(codegTo H x x₀ W) * ∑ y ∈ nbhdIn H x W with y ∈ nbhdIn H x₀ W, 2 ^ usedCnt H W F x y * (1 + q) ^ degTo H y R

The total weight, evaluated: each remaining apex contributes its codegree with x₀ times its own potential mass inside N_H(x₀, W).

theorem BKLOK2.pot_step_mem_sum {V : Type u_1} [DecidableEq V] {β q : ℝ} (hq : 0 ≤ q) {H : Finset (Sym2 V)} {W R : Finset V} {x₀ : V} (hx₀ : x₀ ∈ R) {F : Finset (Sym2 V)} {f : V → V} (hmap : ∀ a ∈ nbhdIn H x₀ W, f a ∈ nbhdIn H x₀ W) (hinv : ∀ a ∈ nbhdIn H x₀ W, f (f a) = a) (hbound : ∑ y ∈ nbhdIn H x₀ W, wgt H W q F (R.erase x₀) R y (f y) ≤ β * ∑ y ∈ nbhdIn H x₀ W, ∑ z ∈ nbhdIn H x₀ W, wgt H W q F (R.erase x₀) R y z) (hcodeg : ∀ x ∈ R.erase x₀, β * ↑(codegTo H x x₀ W) ≤ q) : ∑ x ∈ R.erase x₀, ∑ y ∈ nbhdIn H x W with y ∈ nbhdIn H x₀ W, 2 ^ usedCnt H W (F ∪ famEdges (involutionMatching (nbhdIn H x₀ W) f)) x y * (1 + q) ^ degTo H y (R.erase x₀) ≤ ∑ x ∈ R.erase x₀, ∑ y ∈ nbhdIn H x W with y ∈ nbhdIn H x₀ W, 2 ^ usedCnt H W F x y * (1 + q) ^ degTo H y R

The half of the step inequality living inside the processed neighbourhood: this is where the spread clause and the codegree bound are consumed.

theorem BKLOK2.pot_step {V : Type u_1} [DecidableEq V] {β q : ℝ} (hq : 0 ≤ q) {H : Finset (Sym2 V)} {W R : Finset V} {x₀ : V} (hx₀ : x₀ ∈ R) {F : Finset (Sym2 V)} {f : V → V} (hmap : ∀ a ∈ nbhdIn H x₀ W, f a ∈ nbhdIn H x₀ W) (hinv : ∀ a ∈ nbhdIn H x₀ W, f (f a) = a) (hbound : ∑ y ∈ nbhdIn H x₀ W, wgt H W q F (R.erase x₀) R y (f y) ≤ β * ∑ y ∈ nbhdIn H x₀ W, ∑ z ∈ nbhdIn H x₀ W, wgt H W q F (R.erase x₀) R y z) (hcodeg : ∀ x ∈ R.erase x₀, β * ↑(codegTo H x x₀ W) ≤ q) : pot H W q (F ∪ famEdges (involutionMatching (nbhdIn H x₀ W) f)) (R.erase x₀) ≤ pot H W q F R

The pessimistic estimator does not increase. Processing the apex x₀ with a matching chosen by the spread clause leaves the potential no larger.

The sweep

theorem BKLOK2.spread_process {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {U W : Finset V} {q : ℝ} {s₁ s₂ : ℕ} (hq : 0 ≤ q) (hloop : ∀ e ∈ H, ¬e.IsDiag) (hUW : Disjoint U W) (hEven : ∀ x ∈ U, Even (nbhdIn H x W).card) (hmindeg : ∀ x ∈ U, ∀ v ∈ nbhdIn H x W, (nbhdIn H x W).card / 2 + s₂ + s₁ ≤ edeg (edgesIn H (nbhdIn H x W)) v) (hcodeg : ∀ x ∈ U, ∀ x' ∈ U, x ≠ x' → ↑(codegTo H x x' W) ≤ q * (↑s₂ + 1)) (R : Finset V) : R ⊆ U → ∀ (F : Finset (Sym2 V)), pot H W q F R < 2 ^ (s₁ + 1) → ∃ (Mx : V → Finset (Finset V)), (∀ x ∈ R, GoodMatching H W x (Mx x)) ∧ ((↑R).Pairwise fun (x y : V) => Disjoint (famEdges (Mx x)) (famEdges (Mx y))) ∧ ∀ x ∈ R, Disjoint (famEdges (Mx x)) F

The sequential selection. The apices of R can be processed one at a time, each receiving a perfect matching of its neighbourhood avoiding all the edges used so far, as long as the potential stays below 2 ^ (s₁+1). The Dirac slack is split: s₁ absorbs the already used edges, and the remaining s₂ supplies the 1/(s₂+1)-spread matching of SimpleGraph.exists_spread_involution_of_edgeSet.

theorem BKLOK2.exists_matchings_of_spread {V : Type u_1} [DecidableEq V] {H : Finset (Sym2 V)} {U W : Finset V} {q : ℝ} {s₁ s₂ : ℕ} (hq : 0 ≤ q) (hloop : ∀ e ∈ H, ¬e.IsDiag) (hUW : Disjoint U W) (hEven : ∀ x ∈ U, Even (nbhdIn H x W).card) (hmindeg : ∀ x ∈ U, ∀ v ∈ nbhdIn H x W, (nbhdIn H x W).card / 2 + s₂ + s₁ ≤ edeg (edgesIn H (nbhdIn H x W)) v) (hcodeg : ∀ x ∈ U, ∀ x' ∈ U, x ≠ x' → ↑(codegTo H x x' W) ≤ q * (↑s₂ + 1)) (hpot : pot H W q ∅ U < 2 ^ (s₁ + 1)) : ∃ (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))

Edge-disjoint perfect matchings of all the apex neighbourhoods, from the spread clause and a potential bound at the start of the sweep.