CubicPathwidth.T4.BasicPsi

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

import CubicPathwidth.T4.ProcessDefs

/-!
# The potential `ψ⁻` (paragraph "The potential" of Lemma 9.3 (`lem:bootstrap`))

Helper facts for `CubicPathwidth/T4/Basic.lean`:

* facts about `incr` and `runMin` for a sequence with `BootProps b`
  (`runMin b d ≤ incr b 3 = b 3`, `0 ≤ runMin b d`, and `runMin b d ≤ b d` for `d ≥ 3`);
* the decomposition of `ψ` and `ψ⁻` over the torso components;
* `psiClaim : PsiClaim` (E3a).
-/

noncomputable section

namespace CubicPathwidth
namespace T4
namespace BasicAux

open T2 SectionDecomposition

variable {n : ℕ}

/-! ## Sequence facts -/

theorem incr_nonneg {b : ℕ → ℝ} (hb : BootProps b) {d : ℕ} (hd : 3 ≤ d) :
    0 ≤ incr b d := by
  unfold incr
  linarith [hb.mono d hd]

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

theorem runMin_add_three_le (b : ℕ → ℝ) (d : ℕ) : runMin b (d + 3) ≤ incr b 3 := by
  induction d with
  | zero => simp [runMin]
  | succ k ih =>
    have e : k + 1 + 3 = k + 4 := by omega
    rw [e, runMin]
    exact (min_le_left _ _).trans ih

/-- Every running minimum is at most `h_3 = b_3 - b_2`. -/
theorem runMin_le_incr_three (b : ℕ → ℝ) (d : ℕ) : runMin b d ≤ incr b 3 := by
  rcases Nat.lt_or_ge d 3 with h | h
  · interval_cases d <;> simp [runMin]
  · obtain ⟨e, rfl⟩ : ∃ e, d = e + 3 := ⟨d - 3, by omega⟩
    exact runMin_add_three_le b e

/-- For `d ≥ 3` the running minimum is at most the increment `h_d`. -/
theorem runMin_le_incr {b : ℕ → ℝ} {d : ℕ} (hd : 3 ≤ d) : runMin b d ≤ incr b d := by
  obtain ⟨e, rfl⟩ : ∃ e, d = e + 3 := ⟨d - 3, by omega⟩
  cases e with
  | zero => simp [runMin]
  | succ k =>
    have e1 : k + 1 + 3 = k + 4 := by omega
    rw [e1, runMin]
    exact min_le_right _ _

theorem runMin_nonneg {b : ℕ → ℝ} (hb : BootProps b) (d : ℕ) : 0 ≤ runMin b d := by
  have h3 : 0 ≤ incr b 3 := incr_nonneg hb le_rfl
  rcases Nat.lt_or_ge d 3 with h | h
  · interval_cases d <;> simpa [runMin] using h3
  · obtain ⟨e, rfl⟩ : ∃ e, d = e + 3 := ⟨d - 3, by omega⟩
    clear h
    induction e with
    | zero => simpa [runMin] using h3
    | succ k ih =>
      have e1 : k + 1 + 3 = k + 4 := by omega
      rw [e1, runMin]
      exact le_min ih (incr_nonneg hb (by omega))

/-- For `d ≥ 3`, `H_d ≤ h_d ≤ b_d`: the value `b_d` dominates the running minimum. -/
theorem runMin_le_self {b : ℕ → ℝ} (hb : BootProps b) {d : ℕ} (hd : 3 ≤ d) :
    runMin b d ≤ b d := by
  have h1 := runMin_le_incr (b := b) hd
  have h2 := hb.nonneg (d - 1)
  unfold incr at h1
  linarith

/-! ## Splitting sums over torso components -/

/-- `∑_{v ∈ U} f v` splits over the connected components of `U`. -/
theorem sum_components (G : SimpleGraph (Fin n)) (U : Finset (Fin n)) (f : Fin n → ℝ) :
    ∑ v ∈ U, f v = ∑ C ∈ components G U, ∑ v ∈ C, f v := by
  have hd : (↑(components G U) : Set (Finset (Fin n))).PairwiseDisjoint id :=
    fun C hC D hD hne => components_disjoint G hC hD hne
  conv_lhs => rw [← components_cover G U]
  exact Finset.sum_biUnion hd

theorem psi_eq_sum (b : ℕ → ℝ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) :
    psi b G F B = ∑ C ∈ tcomps G F B, ∑ v ∈ C, b (tdeg G F B v) := by
  unfold psi tcomps
  exact sum_components (tgraph G F B) B (fun v => b (tdeg G F B v))

theorem psiMinus_eq_sum (b : ℕ → ℝ) (G : SimpleGraph (Fin n)) (F B : Finset (Fin n)) :
    psiMinus b G F B = ∑ C ∈ tcomps G F B,
      ((∑ v ∈ C, b (tdeg G F B v)) - runMin b (cmin G F B C)) := by
  unfold psiMinus
  rw [psi_eq_sum, Finset.sum_sub_distrib]

/-! ## Each torso component contributes a nonnegative term -/

theorem tcomp_props {G : SimpleGraph (Fin n)} {F B C : Finset (Fin n)}
    (hC : C ∈ tcomps G F B) : C ⊆ B ∧ C.Nonempty := by
  obtain ⟨hsub, -, hconn⟩ := mem_components (tgraph G F B) hC
  exact ⟨hsub, hconn.1⟩

theorem cmin_eq {G : SimpleGraph (Fin n)} {F B C : Finset (Fin n)} (hne : C.Nonempty) :
    cmin G F B C = C.inf' hne (tdeg G F B) := by
  unfold cmin
  simp only [hne, dite_true]

/-- The term `ψ(C) - H_{δ(C)}` of a torso component `C` is at least `0`, when every
torso degree in `B` is at least `3`. -/
theorem term_le_sum {b : ℕ → ℝ} (hb : BootProps 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) :
    runMin b (cmin G F B C) ≤ ∑ v ∈ C, b (tdeg G F B v) := by
  obtain ⟨hCB, hne⟩ := 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 [cmin_eq hne, hveq]
  have h3 : 3 ≤ cmin G F B C := by
    rw [cmin_eq hne]
    exact Finset.le_inf' hne _ (fun w hw => hmin w (hCB hw))
  rw [hc] at h3 ⊢
  calc runMin b (tdeg G F B v) ≤ b (tdeg G F B v) := runMin_le_self hb h3
    _ ≤ ∑ w ∈ C, b (tdeg G F B w) :=
      Finset.single_le_sum (fun w _ => hb.nonneg _) hv

/-- Each torso component contributes at most `ψ⁻` (its term is a nonnegative summand). -/
theorem term_le_psiMinus {b : ℕ → ℝ} (hb : BootProps 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)) - runMin b (cmin G F B C) ≤ psiMinus b G F B := by
  rw [psiMinus_eq_sum]
  exact Finset.single_le_sum (fun C' hC' => sub_nonneg.mpr (term_le_sum hb hC' hmin)) hC

/-! ## `PsiClaim` (E3a) -/

/-- (E3a) `0 ≤ ψ⁻ ≤ ψ` when every core vertex has torso degree at least `3`. -/
theorem psiClaim : PsiClaim := by
  intro b hb n G F B hmin
  rw [psiMinus_eq_sum, 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 [runMin_nonneg hb (cmin G F B C)]

end BasicAux
end T4
end CubicPathwidth
Back to top