CubicPathwidth.PwSeq.BootSeq

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

import CubicPathwidth.PwSeq.Defs
import CubicPathwidth.T4.BasicPsi
import CubicPathwidth.T4.BasicGlue
import CubicPathwidth.T4.DeletionXKey

/-!
# Sequence and potential facts for `BootPropsK k b` (helper for `Bootstrap.lean`)

Generalized copies of the `BootProps`-dependent helper lemmas of
`T4/ProcessDefs.lean`, `T4/BasicPsi.lean`, `T4/BasicGlue.lean` and
`T4/DeletionXArith.lean`: they use only the fields `zero` and `mono` (and
`runMin_nonneg`), so they hold verbatim for `BootPropsK k b`.

New here: `basicK` (`def:basic` for base degree `k`) and `minDegree_coreTorso`, the fact
that the relabelled torso component `coreTorso G (F \ (B \ C)) C` of a torso component
`C` has the torso degrees on `C` as its degrees, so it inherits minimum degree `3`.
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq
namespace Boot

open T2 T4 SectionDecomposition

variable {n : ℕ}

/-! ## Sequence facts -/

theorem monotone {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) : Monotone b := by
  apply monotone_nat_of_le_succ
  intro d
  rcases Nat.lt_or_ge d 2 with h | h
  · interval_cases d
    · rw [hb.zero.1, hb.zero.2.1]
    · rw [hb.zero.2.1, hb.zero.2.2]
  · have := hb.mono (d + 1) (by omega)
    simpa using this

theorem nonneg {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) (d : ℕ) : 0 ≤ b d := by
  have := monotone hb (Nat.zero_le d)
  rw [hb.zero.1] at this
  exact this

theorem incr_three {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) : T4.incr b 3 = b 3 := by
  simp [T4.incr, hb.zero.2.2]

theorem incr_le {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) (j : ℕ) : T4.incr b j ≤ b j := by
  unfold T4.incr
  have := nonneg hb (j - 1)
  linarith

theorem runMin_le_b {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) {j : ℕ} (hj : 3 ≤ j) :
    T4.runMin b j ≤ b j := (DelX.runMin_le_incr b hj).trans (incr_le hb j)

/-- `ψ` does not increase when the core shrinks and torso degrees do not increase. -/
theorem psi_le_psi {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) {G : SimpleGraph (Fin n)}
    {F B F' B' : Finset (Fin n)} (hsub : B' ⊆ B)
    (hdeg : ∀ v ∈ B', tdeg G F' B' v ≤ tdeg G F B v) :
    psi b G F' B' ≤ psi b G F B := by
  unfold psi
  calc ∑ v ∈ B', b (tdeg G F' B' v) ≤ ∑ v ∈ B', b (tdeg G F B v) :=
        Finset.sum_le_sum fun v hv => monotone hb (hdeg v hv)
    _ ≤ ∑ v ∈ B, b (tdeg G F B v) :=
        Finset.sum_le_sum_of_subset_of_nonneg hsub (fun v _ _ => nonneg hb _)

/-! ## The potential `ψ⁻` -/

/-- The term `ψ(C) - H_{δ(C)}` of a torso component `C` is at least `0`. -/
theorem term_le_sum {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) {G : SimpleGraph (Fin n)}
    {F B C : Finset (Fin n)} (hC : C ∈ tcomps G F B) (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) :
    T4.runMin b (cmin G F B C) ≤ ∑ v ∈ C, b (tdeg G F B v) := by
  obtain ⟨hCB, hne⟩ := BasicAux.tcomp_props hC
  obtain ⟨v, hv, hveq⟩ := Finset.exists_mem_eq_inf' hne (tdeg G F B)
  have hc : cmin G F B C = tdeg G F B v := by rw [BasicAux.cmin_eq hne, hveq]
  have h3 : 3 ≤ cmin G F B C := by
    rw [BasicAux.cmin_eq hne]
    exact Finset.le_inf' hne _ (fun w hw => hmin w (hCB hw))
  rw [hc] at h3 ⊢
  calc T4.runMin b (tdeg G F B v) ≤ b (tdeg G F B v) := runMin_le_b hb h3
    _ ≤ ∑ w ∈ C, b (tdeg G F B w) :=
      Finset.single_le_sum (fun w _ => nonneg hb _) hv

/-- Each torso component contributes at most `ψ⁻`. -/
theorem term_le_psiMinus {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b)
    {G : SimpleGraph (Fin n)} {F B C : Finset (Fin n)} (hC : C ∈ tcomps G F B)
    (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) :
    (∑ v ∈ C, b (tdeg G F B v)) - T4.runMin b (cmin G F B C) ≤ psiMinus b G F B := by
  rw [BasicAux.psiMinus_eq_sum]
  exact Finset.single_le_sum (fun C' hC' => sub_nonneg.mpr (term_le_sum hb hC' hmin)) hC

/-- `0 ≤ ψ⁻ ≤ ψ` when every core vertex has torso degree at least `3`. -/
theorem psi_bounds {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b) (G : SimpleGraph (Fin n))
    (F B : Finset (Fin n)) (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) :
    0 ≤ psiMinus b G F B ∧ psiMinus b G F B ≤ psi b G F B := by
  rw [BasicAux.psiMinus_eq_sum, BasicAux.psi_eq_sum]
  constructor
  · exact Finset.sum_nonneg fun C hC => sub_nonneg.mpr (term_le_sum hb hC hmin)
  · apply Finset.sum_le_sum
    intro C _
    linarith [hb.runMin_nonneg (cmin G F B C)]

/-! ## The relabelled torso component -/

open scoped Classical in

/-- The weight of the relabelled component is at most `∑_{v ∈ U} b (tdeg v)`. -/
theorem degreeWeight_coreTorso_le {k : ℕ} {b : ℕ → ℝ} (hb : BootPropsK k b)
    (G : SimpleGraph (Fin n)) (F B U : Finset (Fin n)) (hU : U ⊆ B) :
    degreeWeight (coreTorso G (F \ (B \ U)) U) b ≤ ∑ v ∈ U, b (tdeg G F B v) := by
  rw [← BasicAux.sum_enumerate U (fun v => b (tdeg G F B v))]
  unfold degreeWeight
  apply Finset.sum_le_sum
  intro i _
  exact monotone hb (BasicAux.degree_coreTorso_le G F B U hU i)

open scoped Classical in

/-- If `U` is closed under torso edges, a vertex of the induced torso on `U` has its
full torso degree. -/
theorem tdeg_le_degree_inducedOnFin (G' : SimpleGraph (Fin n)) (U : Finset (Fin n))
    (hcl : ∀ u ∈ U, ∀ v, G'.Adj u v → v ∈ U) (i : Fin U.card) :
    G'.degree (enumerate U i) ≤ (inducedOnFin G' U).degree i := by
  classical
  have hsub : G'.neighborFinset (enumerate U i) ⊆
      ((inducedOnFin G' U).neighborFinset i).image (enumerate U) := by
    intro u hu
    have hadj : G'.Adj (enumerate U i) u := (G'.mem_neighborFinset _ _).mp hu
    have hiU : enumerate U i ∈ U := (mem_iff_enumerate U _).mpr ⟨i, rfl⟩
    obtain ⟨j, rfl⟩ := (mem_iff_enumerate U u).mp (hcl _ hiU u hadj)
    exact Finset.mem_image.mpr ⟨j, ((inducedOnFin G' U).mem_neighborFinset i j).mpr hadj, rfl⟩
  calc G'.degree (enumerate U i) = (G'.neighborFinset (enumerate U i)).card := rfl
    _ ≤ (((inducedOnFin G' U).neighborFinset i).image (enumerate U)).card :=
        Finset.card_le_card hsub
    _ = ((inducedOnFin G' U).neighborFinset i).card :=
        Finset.card_image_of_injective _ (enumerate U).injective
    _ = (inducedOnFin G' U).degree i := rfl

open scoped Classical in

/-- The relabelled torso component of a torso component `C` inherits minimum degree `3`
from the torso: its degrees are the torso degrees on `C`, since `C` is closed under
torso edges. -/
theorem minDegree_coreTorso {G : SimpleGraph (Fin n)} {F B C : Finset (Fin n)}
    (hC : C ∈ tcomps G F B) (hmin : ∀ v ∈ B, 3 ≤ tdeg G F B v) :
    HasMinDegreeAtLeast 3 (coreTorso G (F \ (B \ C)) C) := by
  obtain ⟨hCB, _⟩ := BasicAux.tcomp_props hC
  have hcl : ∀ u ∈ C, ∀ v, (tgraph G F B).Adj u v → v ∈ C := fun u hu v hadj =>
    (mem_components (tgraph G F B) hC).2.1 u hu v
      ((BasicAux.tgraph_adj_iff G F B u v).1 hadj).2.2.1 hadj
  have hgraph := BasicAux.coreTorso_eq_induced G F B C hCB
  unfold HasMinDegreeAtLeast
  intro i
  have hiC : enumerate C i ∈ C := (mem_iff_enumerate C _).mpr ⟨i, rfl⟩
  have h1 := hmin _ (hCB hiC)
  rw [BasicAux.tdeg_eq_degree] at h1
  have h2 := tdeg_le_degree_inducedOnFin (tgraph G F B) C hcl i
  have h3 : (coreTorso G (F \ (B \ C)) C).degree i = (inducedOnFin (tgraph G F B) C).degree i :=
    degree_congr hgraph i
  omega

/-! ## Basic torso components, base degree `k` -/

/-- Definition 9.8 (`def:basic`) with base degree `k` (`T4.Basic` is the case `k = 5`): either the maximum
torso degree on `C` is at most `k`, or deleting one vertex `v ∈ C` and reducing removes
all of `C` from the core. -/
def BasicK (k : ℕ) (G : SimpleGraph (Fin n)) (F B C : Finset (Fin n)) : Prop :=
  (∀ v ∈ C, tdeg G F B v ≤ k) ∨
    ∃ v ∈ C, ∃ B'' : Finset (Fin n), Reach G (F, B) (F.erase v, B'') ∧ Disjoint B'' C

end Boot
end PwSeq
end CubicPathwidth