Localisation of an unbalanced pair to one Kempe component

An imbalance between two colour classes occurs in a connected component of their two-colour subgraph. Swapping the colours on that component preserves properness and decreases the square-energy. Finite descent therefore produces an equitable colouring on the original palette.

theorem LeanPool.Vizing.Equitable.two_mul_card_colourClass_le_vertices {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {H : SimpleGraph V} [DecidableRel H.Adj] (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn H.edgeFinset colour) (a : Color) : 2 * (ColourClasses.colourClass H.edgeFinset colour a).card ≤ Fintype.card V

A literal colour class is a matching, hence its distinct endpoints occupy twice as many vertices as it has edges.

theorem LeanPool.Vizing.Equitable.finTwo_class_zero_le_one_add_one {V : Type u_1} [Fintype V] [DecidableEq V] {H : SimpleGraph V} [DecidableRel H.Adj] (hconnected : H.Connected) (colour : Sym2 V → Fin 2) (hproper : ColourClasses.ProperOn H.edgeFinset colour) : (ColourClasses.colourClass H.edgeFinset colour 0).card ≤ (ColourClasses.colourClass H.edgeFinset colour 1).card + 1

In a connected graph properly edge-coloured with two colours, either colour has at most one edge more than the other.

def LeanPool.Vizing.Equitable.twoColourGraph {V : Type u_1} {Color : Type u_2} {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) : SimpleGraph V

The spanning subgraph whose edges have one of the selected colours.

Equations

• LeanPool.Vizing.Equitable.twoColourGraph colour a b = { Adj := fun (u v : V) => G.Adj u v ∧ (colour s(u, v) = a ∨ colour s(u, v) = b), symm := ⋯, loopless := ⋯ }

@[instance_reducible]

noncomputable instance LeanPool.Vizing.Equitable.twoColourGraphDecidableAdj {V : Type u_1} {Color : Type u_2} {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) : DecidableRel (twoColourGraph colour a b).Adj

Equations

• LeanPool.Vizing.Equitable.twoColourGraphDecidableAdj colour a b = Classical.decRel (LeanPool.Vizing.Equitable.twoColourGraph colour a b).Adj

@[instance_reducible]

noncomputable instance LeanPool.Vizing.Equitable.twoColourGraphComponentFintype {V : Type u_1} {Color : Type u_2} [Fintype V] {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) : Fintype (twoColourGraph colour a b).ConnectedComponent

Equations

• LeanPool.Vizing.Equitable.twoColourGraphComponentFintype colour a b = Fintype.ofFinite (LeanPool.Vizing.Equitable.twoColourGraph colour a b).ConnectedComponent

noncomputable def LeanPool.Vizing.Equitable.edgeAnchor {V : Type u_1} (e : Sym2 V) : V

A deterministic endpoint used only to name the component containing an edge. No orientation is introduced into the resource model.

Equations

• LeanPool.Vizing.Equitable.edgeAnchor e = (Quot.out e).1

theorem LeanPool.Vizing.Equitable.edgeAnchor_mem {V : Type u_1} (e : Sym2 V) : edgeAnchor e ∈ e

noncomputable def LeanPool.Vizing.Equitable.componentClass {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (x : Color) : Finset (Sym2 V)

Edges of colour x assigned to one connected component of the selected two-colour graph.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanPool.Vizing.Equitable.mem_componentClass {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (x : Color) (e : Sym2 V) : e ∈ componentClass colour a b c x ↔ e ∈ G.edgeFinset ∧ colour e = x ∧ (twoColourGraph colour a b).connectedComponentMk (edgeAnchor e) = c

theorem LeanPool.Vizing.Equitable.sum_card_componentClass {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b x : Color) : ∑ c : (twoColourGraph colour a b).ConnectedComponent, (componentClass colour a b c x).card = (ColourClasses.colourClass G.edgeFinset colour x).card

The component classes partition a global colour class exactly.

theorem LeanPool.Vizing.Equitable.exists_component_strict_imbalance {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hlarge : (ColourClasses.colourClass G.edgeFinset colour b).card < (ColourClasses.colourClass G.edgeFinset colour a).card) : ∃ (c : (twoColourGraph colour a b).ConnectedComponent), (componentClass colour a b c b).card < (componentClass colour a b c a).card

A global strict imbalance between two colours occurs in at least one literal two-colour connected component.

theorem LeanPool.Vizing.Equitable.exists_pair_gap_two_of_not_equitable {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (hnot : ¬EquitableDefinitions.IsEquitable G.edgeFinset colour) : ∃ (a : Color) (b : Color), (ColourClasses.colourClass G.edgeFinset colour b).card + 1 < (ColourClasses.colourClass G.edgeFinset colour a).card

Negating equitability produces the ordered pair needed by the Kempe descent step.

Restriction to one connected component

noncomputable def LeanPool.Vizing.Equitable.liftComponentEdge {V : Type u_1} {Color : Type u_2} {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) : Sym2 ↥c → Sym2 V

Forget the component subtype on an unordered pair.

Equations

• LeanPool.Vizing.Equitable.liftComponentEdge colour a b c = Sym2.map Subtype.val

theorem LeanPool.Vizing.Equitable.liftComponentEdge_injective {V : Type u_1} {Color : Type u_2} {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) : Function.Injective (liftComponentEdge colour a b c)

theorem LeanPool.Vizing.Equitable.liftComponentEdge_mem_graphEdges {V : Type u_1} {Color : Type u_2} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) [Fintype ↥c] [DecidableRel c.toSimpleGraph.Adj] {e : Sym2 ↥c} (he : e ∈ c.toSimpleGraph.edgeFinset) : liftComponentEdge colour a b c e ∈ G.edgeFinset

theorem LeanPool.Vizing.Equitable.liftComponentEdge_has_selected_colour {V : Type u_1} {Color : Type u_2} {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) [Fintype ↥c] [DecidableRel c.toSimpleGraph.Adj] {e : Sym2 ↥c} (he : e ∈ c.toSimpleGraph.edgeFinset) : colour (liftComponentEdge colour a b c e) = a ∨ colour (liftComponentEdge colour a b c e) = b

def LeanPool.Vizing.Equitable.twoColourCode {Color : Type u_2} [DecidableEq Color] (a x : Color) : Fin 2

Encode the selected pair of colours as Fin 2.

Equations

• LeanPool.Vizing.Equitable.twoColourCode a x = if x = a then 0 else 1

theorem LeanPool.Vizing.Equitable.twoColourCode_injective_on_pair {Color : Type u_2} [DecidableEq Color] {a b x y : Color} (hab : a ≠ b) (hx : x = a ∨ x = b) (hy : y = a ∨ y = b) (hcode : twoColourCode a x = twoColourCode a y) : x = y

noncomputable def LeanPool.Vizing.Equitable.componentColour {V : Type u_1} {Color : Type u_2} [DecidableEq Color] {G : SimpleGraph V} (colour : Sym2 V → Color) {a b : Color} (_hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) : Sym2 ↥c → Fin 2

The original colouring restricted to one connected component and recoded with exactly two colours.

Equations

• LeanPool.Vizing.Equitable.componentColour colour _hab c e = LeanPool.Vizing.Equitable.twoColourCode a (colour (LeanPool.Vizing.Equitable.liftComponentEdge colour a b c e))

theorem LeanPool.Vizing.Equitable.componentColour_proper {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn G.edgeFinset colour) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) [Fintype ↥c] [DecidableRel c.toSimpleGraph.Adj] : ColourClasses.ProperOn c.toSimpleGraph.edgeFinset (componentColour colour hab c)

theorem LeanPool.Vizing.Equitable.endpoint_mem_component_of_anchor {V : Type u_1} {Color : Type u_2} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (e : Sym2 V) (heG : e ∈ G.edgeFinset) (hcolour : colour e = a ∨ colour e = b) (hcomponent : (twoColourGraph colour a b).connectedComponentMk (edgeAnchor e) = c) (v : V) : v ∈ e → v ∈ c.supp

Every endpoint of a selected-colour edge lies in the connected component named by its anchor.

noncomputable def LeanPool.Vizing.Equitable.restrictComponentEdge {V : Type u_1} {Color : Type u_2} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (e : Sym2 V) (heG : e ∈ G.edgeFinset) (hcolour : colour e = a ∨ colour e = b) (hcomponent : (twoColourGraph colour a b).connectedComponentMk (edgeAnchor e) = c) : Sym2 ↥c

Put a selected original edge into the subtype of its named component.

Equations

• LeanPool.Vizing.Equitable.restrictComponentEdge colour a b c e heG hcolour hcomponent = s(⟨(Quot.out e).1, ⋯⟩, ⟨(Quot.out e).2, ⋯⟩)

@[simp]

theorem LeanPool.Vizing.Equitable.lift_restrictComponentEdge {V : Type u_1} {Color : Type u_2} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (e : Sym2 V) (heG : e ∈ G.edgeFinset) (hcolour : colour e = a ∨ colour e = b) (hcomponent : (twoColourGraph colour a b).connectedComponentMk (edgeAnchor e) = c) : liftComponentEdge colour a b c (restrictComponentEdge colour a b c e heG hcolour hcomponent) = e

theorem LeanPool.Vizing.Equitable.restrictComponentEdge_mem_graphEdges {V : Type u_1} {Color : Type u_2} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) [Fintype ↥c] [DecidableRel c.toSimpleGraph.Adj] (e : Sym2 V) (heG : e ∈ G.edgeFinset) (hcolour : colour e = a ∨ colour e = b) (hcomponent : (twoColourGraph colour a b).connectedComponentMk (edgeAnchor e) = c) : restrictComponentEdge colour a b c e heG hcolour hcomponent ∈ c.toSimpleGraph.edgeFinset

theorem LeanPool.Vizing.Equitable.anchor_liftComponentEdge_mem_support {V : Type u_1} {Color : Type u_2} {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (e : Sym2 ↥c) : edgeAnchor (liftComponentEdge colour a b c e) ∈ c.supp

theorem LeanPool.Vizing.Equitable.card_componentClass {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) [Fintype ↥c] [DecidableRel c.toSimpleGraph.Adj] (x : Color) (hx : x = a ∨ x = b) : (componentClass colour a b c x).card = (ColourClasses.colourClass c.toSimpleGraph.edgeFinset (componentColour colour hab c) (twoColourCode a x)).card

Restricting a component preserves the size of either selected colour class.

theorem LeanPool.Vizing.Equitable.card_componentClass_left {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) [Fintype ↥c] [DecidableRel c.toSimpleGraph.Adj] : (componentClass colour a b c a).card = (ColourClasses.colourClass c.toSimpleGraph.edgeFinset (componentColour colour hab c) 0).card

The local zero-class and the original a-class have the same cardinality.

theorem LeanPool.Vizing.Equitable.card_componentClass_right {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) [Fintype ↥c] [DecidableRel c.toSimpleGraph.Adj] : (componentClass colour a b c b).card = (ColourClasses.colourClass c.toSimpleGraph.edgeFinset (componentColour colour hab c) 1).card

The local one-class and the original b-class have the same cardinality.

theorem LeanPool.Vizing.Equitable.componentClass_left_le_right_add_one {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn G.edgeFinset colour) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) : (componentClass colour a b c a).card ≤ (componentClass colour a b c b).card + 1

Swapping one component

theorem LeanPool.Vizing.Equitable.anchor_components_eq_of_common_endpoint {V : Type u_1} {Color : Type u_2} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) {e f : Sym2 V} (heG : e ∈ G.edgeFinset) (hfG : f ∈ G.edgeFinset) (he : colour e = a ∨ colour e = b) (hf : colour f = a ∨ colour f = b) {v : V} (hve : v ∈ e) (hvf : v ∈ f) : (twoColourGraph colour a b).connectedComponentMk (edgeAnchor e) = (twoColourGraph colour a b).connectedComponentMk (edgeAnchor f)

def LeanPool.Vizing.Equitable.InSwappedComponent {V : Type u_1} {Color : Type u_2} {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (e : Sym2 V) : Prop

An edge has one of the chosen colours and its anchor belongs to the component on which the exchange is performed.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Vizing.Equitable.swapComponentColour {V : Type u_1} {Color : Type u_2} [DecidableEq Color] {G : SimpleGraph V} (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) : Sym2 V → Color

Swap the two chosen colours exactly on one connected component.

Equations

• LeanPool.Vizing.Equitable.swapComponentColour colour a b c e = if LeanPool.Vizing.Equitable.InSwappedComponent colour a b c e then (Equiv.swap a b) (colour e) else colour e

theorem LeanPool.Vizing.Equitable.swapComponentColour_proper {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn G.edgeFinset colour) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) : ColourClasses.ProperOn G.edgeFinset (swapComponentColour colour a b c)

theorem LeanPool.Vizing.Equitable.colourClass_swapComponent_left {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) : ColourClasses.colourClass G.edgeFinset (swapComponentColour colour a b c) a = ColourClasses.colourClass G.edgeFinset colour a \ componentClass colour a b c a ∪ componentClass colour a b c b

theorem LeanPool.Vizing.Equitable.colourClass_swapComponent_right {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) : ColourClasses.colourClass G.edgeFinset (swapComponentColour colour a b c) b = ColourClasses.colourClass G.edgeFinset colour b \ componentClass colour a b c b ∪ componentClass colour a b c a

theorem LeanPool.Vizing.Equitable.componentClass_subset_colourClass {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) (x : Color) : componentClass colour a b c x ⊆ ColourClasses.colourClass G.edgeFinset colour x

theorem LeanPool.Vizing.Equitable.card_colourClass_exchange_add {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (a b : Color) (c : (twoColourGraph colour a b).ConnectedComponent) {x y : Color} (hxy : x ≠ y) : (ColourClasses.colourClass G.edgeFinset colour x \ componentClass colour a b c x ∪ componentClass colour a b c y).card + (componentClass colour a b c x).card = (ColourClasses.colourClass G.edgeFinset colour x).card + (componentClass colour a b c y).card

Exchanging two disjoint colour classes gives the same cardinality accounting for either direction of a component swap.

theorem LeanPool.Vizing.Equitable.card_swapComponent_left_add {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) : (ColourClasses.colourClass G.edgeFinset (swapComponentColour colour a b c) a).card + (componentClass colour a b c a).card = (ColourClasses.colourClass G.edgeFinset colour a).card + (componentClass colour a b c b).card

theorem LeanPool.Vizing.Equitable.card_swapComponent_right_add {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b : Color} (hab : a ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) : (ColourClasses.colourClass G.edgeFinset (swapComponentColour colour a b c) b).card + (componentClass colour a b c b).card = (ColourClasses.colourClass G.edgeFinset colour b).card + (componentClass colour a b c a).card

theorem LeanPool.Vizing.Equitable.colourClass_swapComponent_of_ne {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) {a b x : Color} (hab : a ≠ b) (hxa : x ≠ a) (hxb : x ≠ b) (c : (twoColourGraph colour a b).ConnectedComponent) : ColourClasses.colourClass G.edgeFinset (swapComponentColour colour a b c) x = ColourClasses.colourClass G.edgeFinset colour x

theorem LeanPool.Vizing.Equitable.sum_eq_two_add_rest {Color : Type u_2} [Fintype Color] [DecidableEq Color] (f : Color → ℕ) {a b : Color} (hab : a ≠ b) : ∑ x : Color, f x = f a + f b + ∑ x ∈ (Finset.univ.erase a).erase b, f x

theorem LeanPool.Vizing.Equitable.exists_energy_decreasing_swap {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [Fintype Color] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn G.edgeFinset colour) {a b : Color} (hgap : (ColourClasses.colourClass G.edgeFinset colour b).card + 1 < (ColourClasses.colourClass G.edgeFinset colour a).card) : ∃ (colour' : Sym2 V → Color), ColourClasses.ProperOn G.edgeFinset colour' ∧ EquitableDefinitions.energy G.edgeFinset colour' < EquitableDefinitions.energy G.edgeFinset colour

One unbalanced pair admits a proper component swap of strictly smaller square-energy.

theorem LeanPool.Vizing.Equitable.exists_equitable_colouring {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq Color] {G : SimpleGraph V} [DecidableRel G.Adj] [Finite Color] (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn G.edgeFinset colour) : ∃ (colour' : Sym2 V → Color), ColourClasses.ProperOn G.edgeFinset colour' ∧ EquitableDefinitions.IsEquitable G.edgeFinset colour'

Every finite proper literal edge colouring has an equitable proper recolouring on the same palette.

noncomputable def LeanPool.Vizing.Equitable.equitableVizingBoundedColouring {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : EquitableDefinitions.BoundedColouring G.edgeFinset (Fin (G.maxDegree + 1)) (EquitableDefinitions.classCeiling G.edgeFinset.card (G.maxDegree + 1))

Vizing's colouring, equitably rebalanced, with the average class-size bound.

Equations

• LeanPool.Vizing.Equitable.equitableVizingBoundedColouring G = ⋯.mp (LeanPool.Vizing.EquitableDefinitions.boundedColouringOfEquitable G.edgeFinset (Classical.choose ⋯) ⋯ ⋯)