CubicPathwidth.T4.DeletionXArith

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

import CubicPathwidth.T4.ProcessDefs

/-!
# The arithmetic of the deletion step (helper for `DeletionX`)

The inequality `J₁ + J₂ + J₃ + J₄ ≥ H_δ` of the proof of Proposition 9.10 (`prop:deletion`), in an abstract form: `C` is a connected set of vertices with
degrees `d` in `[3, Δ]`, `w ∈ C` has degree `Δ ≥ 6`, `N` is its neighbourhood, `d'` the
degrees after deleting `w`, and `J` plays the role of `J₄` (the hypothesis `hJ` is the
Claim of the manuscript).
-/

noncomputable section

namespace CubicPathwidth
namespace T4
namespace DelX

/-! ## The running minimum -/

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

theorem runMin_succ_add_three (b : ℕ → ℝ) (d : ℕ) :
    runMin b (d + 4) = min (runMin b (d + 3)) (incr b (d + 4)) := rfl

theorem runMin_nonneg {b : ℕ → ℝ} (hb : BootProps b) (j : ℕ) : 0 ≤ runMin b j := by
  have key : ∀ d : ℕ, 0 ≤ runMin b (d + 3) := by
    intro d
    induction d with
    | zero => exact incr_nonneg hb le_rfl
    | succ d ih =>
      rw [show d + 1 + 3 = d + 4 from rfl, runMin_succ_add_three]
      exact le_min ih (incr_nonneg hb (by omega))
  rcases Nat.lt_or_ge j 3 with h | h
  · interval_cases j <;> exact incr_nonneg hb le_rfl
  · obtain ⟨d, rfl⟩ : ∃ d, j = d + 3 := ⟨j - 3, by omega⟩
    exact key d

theorem runMin_succ_le {b : ℕ → ℝ} (j : ℕ) : runMin b (j + 1) ≤ runMin b j := by
  rcases Nat.lt_or_ge j 3 with h | h
  · interval_cases j <;> exact le_rfl
  · obtain ⟨d, rfl⟩ : ∃ d, j = d + 3 := ⟨j - 3, by omega⟩
    rw [show d + 3 + 1 = d + 4 from rfl, runMin_succ_add_three]
    exact min_le_left _ _

theorem runMin_anti (b : ℕ → ℝ) {i j : ℕ} (h : i ≤ j) : runMin b j ≤ runMin b i :=
  antitone_nat_of_succ_le (fun j => runMin_succ_le (b := b) j) h

theorem runMin_three (b : ℕ → ℝ) : runMin b 3 = incr b 3 := rfl

theorem runMin_le_incr (b : ℕ → ℝ) {j : ℕ} (hj : 3 ≤ j) : runMin b j ≤ incr b j := by
  rcases Nat.eq_or_lt_of_le hj with h | h
  · rw [← h]; exact le_rfl
  · obtain ⟨d, rfl⟩ : ∃ d, j = d + 4 := ⟨j - 4, by omega⟩
    rw [runMin_succ_add_three]
    exact min_le_right _ _

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

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

/-! ## The core inequality -/

theorem deletion_core_ineq {α : Type*} [DecidableEq α] {b : ℕ → ℝ} (hb : BootProps b)
    (C N : Finset α) (w : α) (d d' : α → ℕ) (Δ δ : ℕ) (J : ℝ)
    (hΔ : 6 ≤ Δ)
    (hCd : ∀ v ∈ C, 3 ≤ d v ∧ d v ≤ Δ)
    (hwd : d w = Δ)
    (hNC : N ⊆ C.erase w) (hNcard : N.card = Δ)
    (hd'N : ∀ v ∈ N, d' v + 1 = d v)
    (hd'o : ∀ v ∈ C.erase w, v ∉ N → d' v = d v)
    (hδ : ∀ v ∈ C, δ ≤ d v) (hδ' : ∃ v ∈ C, d v = δ)
    (hreg : (∀ v ∈ C, d v = Δ) ∨ ∃ x ∈ N, d x < Δ)
    (hJ : ∀ u ∈ C.erase w, 3 ≤ d' u → runMin b (d' u) ≤ J)
    (hstar : ∃ u ∈ C.erase w, 3 ≤ d' u) :
    ((Δ : ℝ) - 1) * runMin b Δ + runMin b (Δ - 1) + runMin b δ ≤
      ∑ v ∈ N, incr b (d v) + J := by
  have hH0 := runMin_nonneg hb
  have hNne : N.Nonempty := by
    rw [← Finset.card_pos, hNcard]; omega
  obtain ⟨v₁, hv₁N, hv₁min⟩ := Finset.exists_min_image N d hNne
  have hv₁C : v₁ ∈ C := Finset.mem_of_mem_erase (hNC hv₁N)
  have hv₁w : v₁ ≠ w := Finset.ne_of_mem_erase (hNC hv₁N)
  have hdN : ∀ v ∈ N, 3 ≤ d v ∧ d v ≤ Δ := fun v hv =>
    hCd v (Finset.mem_of_mem_erase (hNC hv))
  have hterm : ∀ v ∈ N.erase v₁, 0 ≤ incr b (d v) - runMin b Δ := by
    intro v hv
    have h1 := hdN v (Finset.mem_of_mem_erase hv)
    have h2 := runMin_anti b h1.2
    have h3 := runMin_le_incr b h1.1
    linarith
  set R := ∑ v ∈ N.erase v₁, (incr b (d v) - runMin b Δ) with hR
  have hRnn : 0 ≤ R := Finset.sum_nonneg hterm
  have hsum : ∑ v ∈ N, incr b (d v) =
      incr b (d v₁) + R + ((Δ : ℝ) - 1) * runMin b Δ := by
    rw [← Finset.add_sum_erase N _ hv₁N]
    rw [hR, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_erase_of_mem hv₁N, hNcard,
      nsmul_eq_mul]
    have : ((Δ - 1 : ℕ) : ℝ) = (Δ : ℝ) - 1 := by
      rw [Nat.cast_sub (by omega)]; simp
    rw [this]
    ring
  rw [hsum]
  suffices key : runMin b (Δ - 1) + runMin b δ ≤ incr b (d v₁) + R + J by linarith
  have hd₁ := hdN v₁ hv₁N
  have hd₁h : runMin b (d v₁) ≤ incr b (d v₁) := runMin_le_incr b hd₁.1
  rcases hreg with hall | ⟨x, hxN, hxlt⟩
  · -- Case 1: regular
    have hδΔ : δ = Δ := by
      obtain ⟨v, hv, hvd⟩ := hδ'
      rw [← hvd]; exact hall v hv
    have hd1 : d v₁ = Δ := hall v₁ hv₁C
    have hd'1 : d' v₁ = Δ - 1 := by
      have := hd'N v₁ hv₁N; omega
    have hJ1 := hJ v₁ (hNC hv₁N) (by omega)
    rw [hd'1] at hJ1
    rw [hδΔ]
    rw [hd1] at hd₁h ⊢
    linarith
  · -- Case 2: not regular
    have hxC : x ∈ C := Finset.mem_of_mem_erase (hNC hxN)
    have hd1lt : d v₁ < Δ := lt_of_le_of_lt (hv₁min x hxN) hxlt
    have hJ1 : runMin b (Δ - 1) ≤ incr b (d v₁) :=
      (runMin_anti b (by omega : d v₁ ≤ Δ - 1)).trans hd₁h
    by_cases h2a : ∃ u ∈ C.erase w, 3 ≤ d' u ∧ d' u ≤ δ
    · obtain ⟨u, hu, hu3, huδ⟩ := h2a
      have := (runMin_anti b huδ).trans (hJ u hu hu3)
      linarith
    · push Not at h2a
      obtain ⟨u₀, hu₀C, hu₀d⟩ := hδ'
      have hδlt : δ < Δ := lt_of_le_of_lt (hδ x hxC) hxlt
      have hu₀w : u₀ ≠ w := by
        intro h; rw [h, hwd] at hu₀d; omega
      have hu₀E : u₀ ∈ C.erase w := Finset.mem_erase.mpr ⟨hu₀w, hu₀C⟩
      have hδ3 : 3 ≤ δ := hu₀d ▸ (hCd u₀ hu₀C).1
      have hδeq : δ = 3 := by
        by_contra hne
        have h4 : 4 ≤ δ := by omega
        by_cases hn : u₀ ∈ N
        · have := hd'N u₀ hn
          have := h2a u₀ hu₀E (by omega)
          omega
        · have := hd'o u₀ hu₀E hn
          have := h2a u₀ hu₀E (by omega)
          omega
      have hu₀N : u₀ ∈ N := by
        by_contra hn
        have := hd'o u₀ hu₀E hn
        have := h2a u₀ hu₀E (by omega)
        omega
      have hd1eq : d v₁ = 3 := by
        have := hv₁min u₀ hu₀N
        have := hd₁.1
        omega
      have hHδ : runMin b δ = incr b (d v₁) := by
        rw [hδeq, hd1eq, runMin_three]
      suffices key2 : runMin b (Δ - 1) ≤ R + J by linarith
      by_cases hx4 : ∃ x ∈ N, 4 ≤ d x
      · obtain ⟨x, hxN, hx4⟩ := hx4
        have h1 := hd'N x hxN
        have h2 := hdN x hxN
        have := hJ x (hNC hxN) (by omega)
        have h3 := runMin_anti b (by omega : d' x ≤ Δ - 1)
        linarith
      · push Not at hx4
        have hall3 : ∀ x ∈ N, d x = 3 := fun x hx => by
          have := hx4 x hx
          have := (hdN x hx).1
          omega
        have hcard : 0 < (N.erase v₁).card := by
          rw [Finset.card_erase_of_mem hv₁N, hNcard]; omega
        obtain ⟨v₂, hv₂⟩ := Finset.card_pos.mp hcard
        have hv₂N : v₂ ∈ N := Finset.mem_of_mem_erase hv₂
        have hRge : incr b (d v₂) - runMin b Δ ≤ R :=
          Finset.single_le_sum hterm hv₂
        rw [hall3 v₂ hv₂N] at hRge
        obtain ⟨u, hu, hu3⟩ := hstar
        have hun : u ∉ N := by
          intro hn
          have := hd'N u hn
          have := hall3 u hn
          omega
        have hdu := hd'o u hu hun
        have hCu := hCd u (Finset.mem_of_mem_erase hu)
        have hJu := hJ u hu hu3
        rw [hdu] at hJu
        have h5 := runMin_anti b hCu.2
        have h6 := runMin_anti b (by omega : 3 ≤ Δ - 1)
        rw [runMin_three] at h6
        linarith

end DelX
end T4
end CubicPathwidth