CubicPathwidth.CoreCounting

Source file CubicPathwidth/CoreCounting.lean of the Lean project (how it is built).

import CubicPathwidth.BoundaryInduction

/-!
# Degree excess and leaf pruning

All counts refer to induced vertex sets with stable ambient labels. An edge
inside a set contributes twice to its incidence sum. The excess is therefore
twice edges minus twice vertices, with subtraction in the integers.
-/

noncomputable section
namespace CubicPathwidth
open scoped BigOperators

variable {n : ℕ} (G : SimpleGraph (Fin n))

/-- Count incidences directed from U into V. -/
def incidence (U V : Finset (Fin n)) : ℕ :=
  ∑ u ∈ U, (sectionNeighbors G V u).card

theorem incidence_symm (U V : Finset (Fin n)) : incidence G U V = incidence G V U := by
  classical
  simp only [incidence, sectionNeighbors, Finset.card_eq_sum_ones, Finset.sum_filter]
  rw [Finset.sum_comm]
  apply Finset.sum_congr rfl
  intro v hv
  apply Finset.sum_congr rfl
  intro u hu
  rw [G.adj_comm]

theorem incidence_union_left {U V W : Finset (Fin n)} (h : Disjoint U V) :
    incidence G (U ∪ V) W = incidence G U W + incidence G V W := by
  classical
  exact Finset.sum_union h

theorem incidence_union_right {U V W : Finset (Fin n)} (h : Disjoint V W) :
    incidence G U (V ∪ W) = incidence G U V + incidence G U W := by
  rw [incidence_symm G U, incidence_union_left G h,
    incidence_symm G V U, incidence_symm G W U]

theorem incidence_le_subcubic (hG : IsSubcubic G) (U V : Finset (Fin n)) :
    incidence G U V ≤ 3 * U.card := by
  classical
  calc
    incidence G U V ≤ ∑ _u ∈ U, 3 := by
      apply Finset.sum_le_sum
      intro u hu
      apply le_trans (Finset.card_le_card (show sectionNeighbors G V u ⊆ G.neighborFinset u from ?_))
        (hG u)
      intro v hv
      exact (G.mem_neighborFinset _ _).mpr (mem_sectionNeighbors.mp hv).2
    _ = 3 * U.card := by simp [Nat.mul_comm]

/-- Twice the edge-minus-vertex excess, allowing negative values for trees. -/
def degreeExcess (U : Finset (Fin n)) : ℤ :=
  (incidence G U U : ℤ) - 2 * (U.card : ℤ)

theorem incidence_singleton (v : Fin n) : incidence G {v} {v} = 0 := by
  classical
  simp [incidence, sectionNeighbors]

theorem incidence_insert {U : Finset (Fin n)} {v : Fin n} (hv : v ∉ U) :
    incidence G (insert v U) (insert v U) =
      incidence G U U + 2 * (sectionNeighbors G U v).card := by
  classical
  have hd : Disjoint ({v} : Finset (Fin n)) U := Finset.disjoint_singleton_left.mpr hv
  rw [← Finset.singleton_union, incidence_union_left G hd,
    incidence_union_right G hd, incidence_union_right G hd, incidence_singleton]
  rw [incidence_symm G U {v}]
  simp [incidence]
  omega

theorem degreeExcess_insert {U : Finset (Fin n)} {v : Fin n} (hv : v ∉ U) :
    degreeExcess G (insert v U) =
      degreeExcess G U + 2 * (sectionNeighbors G U v).card - 2 := by
  classical
  rw [degreeExcess, incidence_insert G hv, Finset.card_insert_of_notMem hv]
  push_cast
  unfold degreeExcess
  ring

theorem sectionNeighbors_erase_self (U : Finset (Fin n)) (v : Fin n) :
    sectionNeighbors G (U.erase v) v = sectionNeighbors G U v := by
  classical
  ext u
  simp only [mem_sectionNeighbors, Finset.mem_erase]
  constructor
  · exact fun h => ⟨h.1.2, h.2⟩
  · intro h
    exact ⟨⟨h.2.ne.symm, h.1⟩, h.2⟩

/-- Removing a leaf preserves edges minus vertices exactly. -/
theorem degreeExcess_erase_leaf {U : Finset (Fin n)} {v : Fin n}
    (hv : v ∈ U) (hdeg : (sectionNeighbors G U v).card = 1) :
    degreeExcess G (U.erase v) = degreeExcess G U := by
  have h := degreeExcess_insert G (Finset.notMem_erase v U)
  rw [Finset.insert_erase hv, sectionNeighbors_erase_self, hdeg] at h
  omega

/-- The boundary uses at least two incidences at each of its vertices.
Consequently the complement's excess is at most |U| - 3|X|. -/
theorem stable_degreeExcess_bound (hG : IsSubcubic G)
    {U X : Finset (Fin n)} (hX : X ⊆ U) (hs : StableBoundary G U X) :
    degreeExcess G (U \ X) ≤ (U.card : ℤ) - 3 * (X.card : ℤ) := by
  classical
  have hlower : 2 * X.card ≤ incidence G X (U \ X) := by
    calc
      2 * X.card = ∑ _v ∈ X, 2 := by simp [Nat.mul_comm]
      _ ≤ incidence G X (U \ X) := Finset.sum_le_sum hs
  have hd : Disjoint (U \ X) X := Finset.sdiff_disjoint
  have hupper := incidence_le_subcubic G hG (U \ X) ((U \ X) ∪ X)
  rw [incidence_union_right G hd, incidence_symm G (U \ X) X] at hupper
  have hc := Finset.card_sdiff_add_card_eq_card hX
  unfold degreeExcess
  omega

/-- A minimum-degree-two subcubic section has degree two or three at every
vertex, so its excess counts exactly its degree-three vertices. -/
theorem degreeExcess_eq_branch_card (hG : IsSubcubic G) (U : Finset (Fin n))
    (hmin : ∀ v ∈ U, 2 ≤ (sectionNeighbors G U v).card) :
    degreeExcess G U = ((U.filter (fun v => (sectionNeighbors G U v).card = 3)).card : ℤ) := by
  classical
  have hdeg : ∀ v ∈ U, (sectionNeighbors G U v).card ≤ 3 := by
    intro v hv
    calc
      _ ≤ (G.neighborFinset v).card := Finset.card_le_card (by
        intro u hu
        exact (G.mem_neighborFinset _ _).mpr (mem_sectionNeighbors.mp hu).2)
      _ ≤ 3 := hG v
  have he : ∀ v ∈ U, ((sectionNeighbors G U v).card : ℤ) =
      2 + if (sectionNeighbors G U v).card = 3 then 1 else 0 := by
    intro v hv
    have hi := hmin v hv
    have hu := hdeg v hv
    split_ifs <;> omega
  have hsum : (incidence G U U : ℤ) = 2 * (U.card : ℤ) +
      ((U.filter (fun v => (sectionNeighbors G U v).card = 3)).card : ℤ) := by
    simp only [incidence, Nat.cast_sum]
    rw [Finset.sum_congr rfl he, Finset.sum_add_distrib]
    simp [mul_comm]
  unfold degreeExcess
  omega

end CubicPathwidth
Back to top