CubicPathwidth.T4.Cor5S

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

import CubicPathwidth.T4.Defs
import CubicPathwidth.Relabelling
import Mathlib.Combinatorics.SimpleGraph.DegreeSum

noncomputable section

namespace CubicPathwidth
namespace T4

open SectionDecomposition

theorem hasPathwidth_mono {n : ℕ} {G : SimpleGraph (Fin n)} {a b : ℝ}
    (h : HasPathwidthAtMost G a) (hab : a ≤ b) : HasPathwidthAtMost G b := by
  obtain ⟨D, hD⟩ := h
  exact ⟨D, fun i => (hD i).trans (by linarith)⟩

/-- Adding isolated vertices one at a time. -/
theorem add_isolated {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] {w : ℝ} (hw : 0 ≤ w) :
    ∀ (S : Finset (Fin n)) (U : Finset (Fin n)),
      (∀ v ∈ S, v ∉ U ∧ G.degree v = 0) →
      ∀ P : SectionDecomposition G U, P.toBagPath.WidthAtMost w →
      ∃ Q : SectionDecomposition G (S ∪ U), Q.toBagPath.WidthAtMost w := by
  intro S
  induction S using Finset.induction_on with
  | empty =>
    intro U _ P hP
    rw [Finset.empty_union]
    exact ⟨P, hP⟩
  | insert a S ha ih =>
    intro U hS P hP
    have haU : a ∉ U := (hS a (Finset.mem_insert_self _ _)).1
    have hdeg : G.degree a = 0 := (hS a (Finset.mem_insert_self _ _)).2
    have hno : ∀ u, ¬ G.Adj a u := by
      intro u hu
      have := (G.degree_pos_iff_exists_adj a).mpr ⟨u, hu⟩
      omega
    let R := P.restoreVertex a haU {a} (Finset.mem_singleton_self a)
      (by intro u hu; simp at hu; subst hu; exact Finset.mem_insert_self _ _)
      (by intro u hu hau; rw [Finset.mem_singleton] at hu; exact absurd (hu ▸ hau) haU)
      (fun u _ h => absurd h (hno u))
    have hR : R.toBagPath.WidthAtMost w := by
      have := restoreVertex_width P a haU {a} (Finset.mem_singleton_self a)
        (by intro u hu; simp at hu; subst hu; exact Finset.mem_insert_self _ _)
        (by intro u hu hau; rw [Finset.mem_singleton] at hu; exact absurd (hu ▸ hau) haU)
        (fun u _ h => absurd h (hno u)) hP
      exact fun i hi => (this i hi).trans (by simp [hw])
    obtain ⟨Q, hQ⟩ := ih (insert a U) (by
      intro v hv
      have := hS v (Finset.mem_insert_of_mem hv)
      refine ⟨?_, this.2⟩
      intro hv'
      rcases Finset.mem_insert.mp hv' with rfl | h
      · exact ha hv
      · exact this.1 h) R hR
    have heq : S ∪ insert a U = insert a S ∪ U := by
      ext x; simp
    have key : ∃ Q : SectionDecomposition G (S ∪ insert a U), Q.toBagPath.WidthAtMost w :=
      ⟨Q, hQ⟩
    rw [heq] at key
    exact key

/-- Per-degree bound `a_d ≤ (7/96) d`. -/
theorem coeff_le (d : ℕ) : thm4Coeff d ≤ 7 / 96 * (d : ℝ) := by
  by_cases h2 : d ≤ 2
  · simp only [thm4Coeff, if_pos h2]; positivity
  by_cases h13 : d ≤ 13
  · interval_cases d <;> norm_num [thm4Coeff]
  · push_neg at h13
    have hd : (14 : ℝ) ≤ d := by exact_mod_cast h13
    have h1 : thm4Coeff d ≤ 1 := by
      have : ¬ d ≤ 2 := h2
      have h6 : ¬ d ≤ 6 := by omega
      have h10 : ¬ d ≤ 10 := by omega
      simp only [thm4Coeff, if_neg this, if_neg h6, if_neg h10]
      have : 0 ≤ 4 / ((d : ℝ) + 1) := by positivity
      linarith
    linarith

theorem pw_extend {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] {w : ℝ} (hw : 0 ≤ w) :
    HasPathwidthAtMost (inducedOnFin G (Finset.univ.filter (fun v => 0 < G.degree v)))
      w → HasPathwidthAtMost G w := by
  intro ⟨D, hD⟩
  generalize hU : Finset.univ.filter (fun v => 0 < G.degree v) = U at D hD
  have hP := lift_width G U D hD
  obtain ⟨Q, hQ⟩ := add_isolated G hw (Finset.univ.filter (fun v => ¬ 0 < G.degree v)) U
    (by
      intro v hv
      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hv
      refine ⟨?_, by omega⟩
      rw [← hU]; simp [hv]) (lift G U D) hP
  have hall : (Finset.univ.filter (fun v => ¬ 0 < G.degree v)) ∪ U = Finset.univ := by
    ext x; subst hU; simp; omega
  have key : ∃ Q : SectionDecomposition G ((Finset.univ.filter (fun v => ¬ 0 < G.degree v)) ∪ U),
      Q.toBagPath.WidthAtMost w := ⟨Q, hQ⟩
  rw [hall] at key
  obtain ⟨Q, hQ⟩ := key
  exact ⟨Q.toFull, Q.toFull_width hQ⟩

theorem deg_induced_le {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    [DecidableRel (inducedOnFin G (Finset.univ.filter (fun v => 0 < G.degree v))).Adj]
    (U : Finset (Fin n)) [DecidableRel (inducedOnFin G U).Adj] (i : Fin U.card) :
    (inducedOnFin G U).degree i ≤ G.degree (enumerate U i) := by
  have hsub : ((inducedOnFin G U).neighborFinset i).image (enumerate U) ⊆
      G.neighborFinset (enumerate U i) := by
    intro u hu
    obtain ⟨w, hw, rfl⟩ := Finset.mem_image.mp hu
    apply (G.mem_neighborFinset _ _).mpr
    exact ((inducedOnFin G U).mem_neighborFinset i w).mp hw
  calc (inducedOnFin G U).degree i = ((inducedOnFin G U).neighborFinset i).card := rfl
    _ = (((inducedOnFin G U).neighborFinset i).image (enumerate U)).card :=
      (Finset.card_image_of_injective _ (enumerate U).injective).symm
    _ ≤ (G.neighborFinset (enumerate U i)).card := Finset.card_le_card hsub

theorem cor5_s : Cor5Claim := by
  classical
  intro h4 ε hε
  obtain ⟨N, hN⟩ := h4 (ε / 2) (by positivity)
  refine ⟨⌈(N : ℝ) / ε⌉₊, ?_⟩
  intro n G hM
  set m := edgeCount G with hm
  have hmR : ((⌈(N : ℝ) / ε⌉₊ : ℕ) : ℝ) ≤ (m : ℝ) := by exact_mod_cast hM
  have hNm : (N : ℝ) ≤ ε * m := by
    have h1 : (N : ℝ) / ε ≤ m := (Nat.le_ceil _).trans hmR
    rw [div_le_iff₀ hε] at h1; linarith
  have hm0 : (0 : ℝ) ≤ m := Nat.cast_nonneg _
  have hdeg : ∑ v, G.degree v = 2 * m := by
    rw [hm]; unfold edgeCount; exact SimpleGraph.sum_degrees_eq_twice_card_edges G
  set U := Finset.univ.filter (fun v => 0 < G.degree v) with hU
  have hcardU : (U.card : ℝ) ≤ 2 * m := by
    have : U.card ≤ ∑ v, G.degree v := by
      calc U.card = ∑ v ∈ U, 1 := by simp
        _ ≤ ∑ v ∈ U, G.degree v := Finset.sum_le_sum (fun v hv => by
            have : 0 < G.degree v := by simpa [hU] using hv
            omega)
        _ ≤ ∑ v, G.degree v := Finset.sum_le_sum_of_subset (Finset.subset_univ _)
    rw [hdeg] at this
    exact_mod_cast this
  have hw : (0 : ℝ) ≤ (7 / 48 + ε) * m := by positivity
  apply pw_extend G hw
  by_cases hbig : N ≤ U.card
  · apply hasPathwidth_mono (hN U.card hbig (inducedOnFin G U))
    have hsum : ∑ i : Fin U.card, (inducedOnFin G U).degree i ≤ 2 * m := by
      have : ∑ i : Fin U.card, (inducedOnFin G U).degree i ≤ ∑ v, G.degree v := by
        calc ∑ i : Fin U.card, (inducedOnFin G U).degree i
            ≤ ∑ i : Fin U.card, G.degree (enumerate U i) :=
              Finset.sum_le_sum (fun i _ => deg_induced_le G U i)
          _ = ∑ v ∈ Finset.univ.map (enumerate U), G.degree v := by
              rw [Finset.sum_map]
          _ ≤ ∑ v, G.degree v := Finset.sum_le_sum_of_subset (Finset.subset_univ _)
      omega
    have hsumR : (∑ i : Fin U.card, ((inducedOnFin G U).degree i : ℝ)) ≤ 2 * m := by
      exact_mod_cast hsum
    have hdw : degreeWeight (inducedOnFin G U) thm4Coeff ≤ 7 / 48 * m := by
      unfold degreeWeight
      calc _ ≤ ∑ i : Fin U.card, 7 / 96 * (((inducedOnFin G U).degree i : ℕ) : ℝ) :=
            Finset.sum_le_sum (fun i _ => coeff_le _)
        _ = 7 / 96 * ∑ i : Fin U.card, (((inducedOnFin G U).degree i : ℕ) : ℝ) := by
            rw [← Finset.mul_sum]
        _ ≤ 7 / 96 * (2 * m) := by gcongr
        _ = 7 / 48 * m := by ring
    nlinarith
  · push_neg at hbig
    apply hasPathwidth_mono (trivial_pathwidth_bound (inducedOnFin G U))
    have : (U.card : ℝ) ≤ N := by exact_mod_cast hbig.le
    nlinarith

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.cor5_s