Independent local improvements of threshold cuts

A set I of vertices of a multigraph is independent when no edge has both endpoints in I. Then every edge is at at most one vertex of I, so changing a cut only at the vertices of I changes its size by the sum of the changes at the edges of each of them (ncard_edgeCut_add_sum_eq). In particular, improvements of the cut at each vertex of I, made simultaneously, improve the whole cut (ncard_edgeCut_le_of_local), and the gain is the sum of the local gains (ncard_edgeCut_eq_add_sum_sub).

For a layout by keys, the cuts are the threshold cuts {v | key v < t}. Moving the key of each vertex of an independent set to a median of the keys of its neighbours improves every threshold cut at once (ncard_edgeCut_threshold_le): at every threshold, a median sides with at least half of the neighbours. For a vertex with three edges, the median of the three keys of its neighbours is such a median (isMedianAt_median3).

Main definitions

• Cslib.Circuits.Frontier.Multigraph.otherEnd: the endpoint of an edge other than a vertex.
• Cslib.Circuits.Frontier.Multigraph.IsMedianAt: a median of the keys of the neighbours.
• Cslib.Circuits.Frontier.median3: the median of three values.

Main results

• Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_add_sum_eq: the exact change of a cut under changes at an independent set.
• Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_of_local: independent local improvements improve the cut.
• Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_threshold_le: independent median updates improve every threshold cut.
• Cslib.Circuits.Frontier.Multigraph.isMedianAt_median3: the median of three keys.

def Cslib.Circuits.Frontier.median3 {α : Type u_1} [LinearOrder α] (a b c : α) : α

The median of three values.

theorem Cslib.Circuits.Frontier.two_le_median3 {α : Type u_1} [LinearOrder α] (a b c : α) : (2 ≤ ((if a ≤ median3 a b c then 1 else 0) + if b ≤ median3 a b c then 1 else 0) + if c ≤ median3 a b c then 1 else 0) ∧ 2 ≤ ((if median3 a b c ≤ a then 1 else 0) + if median3 a b c ≤ b then 1 else 0) + if median3 a b c ≤ c then 1 else 0

At least two of three values are at most their median, and at least two are at least it.

Changes at an independent set

theorem Cslib.Circuits.Frontier.Multigraph.ncard_inter_touching {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {I : Finset V} (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (X : Set E) : (X ∩ G.touching ↑I).ncard = ∑ v ∈ I, (X ∩ G.incidenceSet v).ncard

Independent sets count edges once. If no edge has both endpoints in I, the edges of a set X at the vertices of I are the disjoint union of those at each vertex of I.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_add_sum_eq {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {I : Finset V} (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) {L L' : Set V} (hLL' : ∀ v ∉ I, v ∈ L ↔ v ∈ L') : (G.edgeCut L').ncard + ∑ v ∈ I, (G.edgeCut L ∩ G.incidenceSet v).ncard = (G.edgeCut L).ncard + ∑ v ∈ I, (G.edgeCut L' ∩ G.incidenceSet v).ncard

The exact change of a cut under changes at an independent set I: if L and L' agree outside I, the cut of L' together with the local cuts of L at the vertices of I balances the cut of L together with the local cuts of L'.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_of_local {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {I : Finset V} (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) {L L' : Set V} (hLL' : ∀ v ∉ I, v ∈ L ↔ v ∈ L') (hlocal : ∀ v ∈ I, (G.edgeCut L' ∩ G.incidenceSet v).ncard ≤ (G.edgeCut L ∩ G.incidenceSet v).ncard) : (G.edgeCut L').ncard ≤ (G.edgeCut L).ncard

Independent local improvements improve the cut. If L and L' agree outside an independent set I, and at each vertex of I at most as many edges cross L' as cross L, then at most as many edges cross L' as cross L.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_lt_of_local {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {I : Finset V} (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) {L L' : Set V} (hLL' : ∀ v ∉ I, v ∈ L ↔ v ∈ L') (hlocal : ∀ v ∈ I, (G.edgeCut L' ∩ G.incidenceSet v).ncard ≤ (G.edgeCut L ∩ G.incidenceSet v).ncard) (hstrict : ∃ v ∈ I, (G.edgeCut L' ∩ G.incidenceSet v).ncard < (G.edgeCut L ∩ G.incidenceSet v).ncard) : (G.edgeCut L').ncard < (G.edgeCut L).ncard

A strict local improvement at one vertex of I gives a strict improvement of the cut.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_eq_add_sum_sub {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [Finite E] {I : Finset V} (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) {L L' : Set V} (hLL' : ∀ v ∉ I, v ∈ L ↔ v ∈ L') (hlocal : ∀ v ∈ I, (G.edgeCut L' ∩ G.incidenceSet v).ncard ≤ (G.edgeCut L ∩ G.incidenceSet v).ncard) : (G.edgeCut L).ncard = (G.edgeCut L').ncard + ∑ v ∈ I, ((G.edgeCut L ∩ G.incidenceSet v).ncard - (G.edgeCut L' ∩ G.incidenceSet v).ncard)

The gain is the sum of the local gains: updated stars at an independent set do not interact.

Median updates of keys

def Cslib.Circuits.Frontier.Multigraph.otherEnd {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [DecidableEq V] (v : V) (e : E) : V

The endpoint of e other than v. When v is not an endpoint of e, this is the source of e.

theorem Cslib.Circuits.Frontier.Multigraph.mem_edgeCut_iff_otherEnd {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [DecidableEq V] {L : Set V} {v : V} {e : E} (he : e ∈ G.incidenceSet v) : e ∈ G.edgeCut L ↔ ¬(v ∈ L ↔ G.otherEnd v e ∈ L)

An edge at v crosses a cut when its other end lies on the other side.

theorem Cslib.Circuits.Frontier.Multigraph.otherEnd_notMem {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [DecidableEq V] {I : Finset V} (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) {v : V} (hv : v ∈ I) {e : E} (he : e ∈ G.incidenceSet v) : G.otherEnd v e ∉ I

In an independent set, the other ends of the edges at a vertex lie outside the set.

def Cslib.Circuits.Frontier.Multigraph.IsMedianAt {V : Type u_1} {E : Type u_2} (G : Multigraph V E) [DecidableEq V] {α : Type u_3} [LinearOrder α] (key : V → α) (v : V) (m : α) : Prop

m is a median at v of the keys of the neighbours of v: of the edges at v, at most as many lead to keys above m as to keys at most m, and at most as many lead to keys below m as to keys at least m.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_threshold_inter_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [DecidableEq V] [Finite E] {α : Type u_3} [LinearOrder α] {key key' : V → α} {v : V} (hfix : ∀ e ∈ G.incidenceSet v, key' (G.otherEnd v e) = key (G.otherEnd v e)) (hmed : G.IsMedianAt key v (key' v)) (t : α) : (G.edgeCut {w : V | key' w < t} ∩ G.incidenceSet v).ncard ≤ (G.edgeCut {w : V | key w < t} ∩ G.incidenceSet v).ncard

A median minimises the local threshold cuts. If the neighbours of v keep their keys and the new key of v is a median of theirs, then at every threshold at most as many edges at v cross the new threshold cut as crossed the old one.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_threshold_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [DecidableEq V] [Finite E] {α : Type u_3} [LinearOrder α] {I : Finset V} (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) {key key' : V → α} (hfix : ∀ v ∉ I, key' v = key v) (hmed : ∀ v ∈ I, G.IsMedianAt key v (key' v)) (t : α) : (G.edgeCut {w : V | key' w < t}).ncard ≤ (G.edgeCut {w : V | key w < t}).ncard

Median updates improve every threshold cut. Moving the keys of the vertices of an independent set I to medians of the keys of their neighbours does not increase the cut at any threshold.

theorem Cslib.Circuits.Frontier.Multigraph.isMedianAt_median3 {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [DecidableEq V] {α : Type u_3} [LinearOrder α] (key : V → α) {v : V} {e₀ e₁ e₂ : E} (h01 : e₀ ≠ e₁) (h02 : e₀ ≠ e₂) (h12 : e₁ ≠ e₂) (hv : G.incidenceSet v = {e₀, e₁, e₂}) : G.IsMedianAt key v (median3 (key (G.otherEnd v e₀)) (key (G.otherEnd v e₁)) (key (G.otherEnd v e₂)))

The median of three keys. At a vertex with exactly three edges, the median of the keys of the three neighbours is a median.