CubicPathwidth.PwSeq.Extension

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

import CubicPathwidth.PwSeq.Defs

/-!
# Lemma 9.6 (`lem:extension`) for general `k` (obligation Q2)

Proves `TargetBootSeq` (the bootstrap sequence is the one defined by Equation (9.1) (`eq:bootstrap-rec`))
and `ExtensionClaim` (the bootstrap of a seed satisfying `SeedHyp` has the properties
`BootPropsK`). In the paper: Lemma 9.6 (`lem:extension`).

With `b = bootstrapSeq k a`, `h_d = b_d - b_{d-1}` and `H_d = min_{3 ≤ i ≤ d} h_i`, the
second component of `bootPair k a d` is `H_d` (`bootPair_snd`). For `d > k`, put
`μ = H_{d-1}` and `θ = (1 - b_{d-1} - μ)/d`; the two terms of the maximum are
`b_{d-1} + θ` and `b_{d-1} + θ + (d-1)(θ - μ)`, and `bootStep_spec` shows in both cases
`h_d ≥ 0`, `H_d ≥ 0` and `1 - b_d = (d-1) H_d + H_{d-1}`.
-/

noncomputable section

namespace CubicPathwidth
namespace PwSeq

/-! ## One step of the recurrence -/

/-- One step of the recurrence, as a statement about reals. -/
theorem bootStep_spec (d : ℕ) (hd : 3 ≤ d) (bp μ : ℝ) (hμ : 0 ≤ μ) (hb : bp + μ ≤ 1) :
    bp ≤ bootStep d bp μ ∧ 0 ≤ min μ (bootStep d bp μ - bp) ∧
      1 - bootStep d bp μ = ((d : ℝ) - 1) * min μ (bootStep d bp μ - bp) + μ := by
  have hd' : (3 : ℝ) ≤ d := by exact_mod_cast hd
  have hdpos : (0 : ℝ) < d := by linarith
  set θ : ℝ := (1 - bp - μ) / d with hθdef
  have hθ : (d : ℝ) * θ = 1 - bp - μ := by
    rw [hθdef]; field_simp
  have hθ0 : 0 ≤ θ := by
    rw [hθdef]; exact div_nonneg (by linarith) hdpos.le
  have hp : (1 + ((d : ℝ) - 1) * bp - μ) / d = bp + θ := by
    rw [hθdef]; field_simp; ring
  have hq : 1 - (d : ℝ) * μ = bp + θ + ((d : ℝ) - 1) * (θ - μ) := by
    nlinarith
  unfold bootStep
  rw [hp, hq]
  rcases le_total θ μ with h | h
  · have hm : max (bp + θ) (bp + θ + ((d : ℝ) - 1) * (θ - μ)) = bp + θ := by
      apply max_eq_left
      nlinarith
    rw [hm]
    have : min μ (bp + θ - bp) = θ := by
      rw [show bp + θ - bp = θ by ring]; exact min_eq_right h
    rw [this]
    refine ⟨by linarith, hθ0, ?_⟩
    nlinarith
  · have hm : max (bp + θ) (bp + θ + ((d : ℝ) - 1) * (θ - μ)) =
        bp + θ + ((d : ℝ) - 1) * (θ - μ) := by
      apply max_eq_right
      nlinarith
    rw [hm]
    have hge : μ ≤ bp + θ + ((d : ℝ) - 1) * (θ - μ) - bp := by
      nlinarith
    have : min μ (bp + θ + ((d : ℝ) - 1) * (θ - μ) - bp) = μ := min_eq_left hge
    rw [this]
    refine ⟨by nlinarith, hμ, ?_⟩
    nlinarith

/-! ## Running minima -/

theorem runMin_le_three (b : ℕ → ℝ) (d : ℕ) (hd : d ≤ 3) : runMin b d = incr b 3 := by
  match d, hd with
  | 0, _ => rfl
  | 1, _ => rfl
  | 2, _ => rfl
  | 3, _ => rfl

theorem runMin_succ (b : ℕ → ℝ) (d : ℕ) (hd : 3 ≤ d) :
    runMin b (d + 1) = min (runMin b d) (incr b (d + 1)) := by
  obtain ⟨m, rfl⟩ : ∃ m, d = m + 3 := ⟨d - 3, by omega⟩
  rfl

/-- For `d ≥ 3`, `runMin b d` only depends on the values of `b` at indices `≤ d`. -/
theorem runMin_congr (b c : ℕ → ℝ) (d : ℕ) (hd : 3 ≤ d) (h : ∀ i, i ≤ d → b i = c i) :
    runMin b d = runMin c d := by
  induction d, hd using Nat.le_induction with
  | base =>
    rw [runMin_le_three b 3 le_rfl, runMin_le_three c 3 le_rfl]
    simp only [incr]
    rw [h 3 le_rfl, h 2 (by omega)]
  | succ d hd ih =>
    rw [runMin_succ b d hd, runMin_succ c d hd, ih (fun i hi => h i (by omega))]
    simp only [incr]
    rw [h (d + 1) le_rfl, h (d + 1 - 1) (by omega)]

/-- If all increments `h_3, …, h_d` are nonnegative, so is `H_d` (`d ≥ 3`). -/
theorem runMin_nonneg_of (b : ℕ → ℝ) (d : ℕ) (hd : 3 ≤ d)
    (h : ∀ i, 3 ≤ i → i ≤ d → 0 ≤ incr b i) : 0 ≤ runMin b d := by
  induction d, hd using Nat.le_induction with
  | base => rw [runMin_le_three b 3 le_rfl]; exact h 3 le_rfl le_rfl
  | succ d hd ih =>
    rw [runMin_succ b d hd]
    exact le_min (ih (fun i h3 hi => h i h3 (by omega))) (h (d + 1) (by omega) le_rfl)

/-! ## Structure of `bootPair` and `bootstrapSeq` -/

section
variable (k : ℕ) (a : ℕ → ℝ)

theorem bootstrapSeq_le_two (d : ℕ) (hd : d ≤ 2) : bootstrapSeq k a d = 0 := by
  match d, hd with
  | 0, _ => rfl
  | 1, _ => rfl
  | 2, _ => rfl

theorem bootstrapSeq_three : bootstrapSeq k a 3 = a 3 := rfl

theorem bootstrapSeq_succ (m : ℕ) :
    bootstrapSeq k a (m + 4) =
      if m + 4 ≤ k then a (m + 4)
      else bootStep (m + 4) (bootPair k a (m + 3)).1 (bootPair k a (m + 3)).2 := by
  simp only [bootstrapSeq, bootPair]

theorem bootPair_succ_snd (m : ℕ) :
    (bootPair k a (m + 4)).2 =
      min (bootPair k a (m + 3)).2 (bootstrapSeq k a (m + 4) - bootstrapSeq k a (m + 3)) := by
  simp only [bootstrapSeq, bootPair]

/-- The second component of `bootPair k a d` is the running minimum of the increments. -/
theorem bootPair_snd (d : ℕ) (hd : 3 ≤ d) :
    (bootPair k a d).2 = runMin (bootstrapSeq k a) d := by
  induction d, hd using Nat.le_induction with
  | base =>
    rw [runMin_le_three _ 3 le_rfl]
    simp only [bootPair, incr, bootstrapSeq_le_two k a 2 le_rfl]
    simp [bootstrapSeq_three]
  | succ d hd ih =>
    obtain ⟨m, rfl⟩ : ∃ m, d = m + 3 := ⟨d - 3, by omega⟩
    rw [show m + 3 + 1 = m + 4 by rfl, bootPair_succ_snd, ih]
    rfl

theorem bootstrapSeq_seed (d : ℕ) (h3 : 3 ≤ d) (hdk : d ≤ k) :
    bootstrapSeq k a d = a d := by
  obtain ⟨m, rfl⟩ : ∃ m, d = m + 3 := ⟨d - 3, by omega⟩
  rcases m with _ | m
  · rfl
  · rw [show m + 1 + 3 = m + 4 by rfl, bootstrapSeq_succ]
    simp only [show m + 4 ≤ k by omega, ↓reduceIte]

theorem bootstrapSeq_gt (d : ℕ) (hdk : k < d) (hk : 3 ≤ k) :
    bootstrapSeq k a d =
      bootStep d (bootstrapSeq k a (d - 1)) (runMin (bootstrapSeq k a) (d - 1)) := by
  obtain ⟨m, rfl⟩ : ∃ m, d = m + 4 := ⟨d - 4, by omega⟩
  rw [bootstrapSeq_succ]
  simp only [show ¬ (m + 4 ≤ k) by omega, ↓reduceIte]
  rw [show m + 4 - 1 = m + 3 by rfl, bootPair_snd k a (m + 3) (by omega)]
  rfl

end

/-- (A3) `bootstrapSeq` is the sequence defined by Equation (9.1) (`eq:bootstrap-rec`). -/
theorem targetBootSeq : TargetBootSeq := by
  intro k a hk
  exact ⟨bootstrapSeq_le_two k a, fun d h3 hdk => bootstrapSeq_seed k a d h3 hdk,
    fun d hdk => bootstrapSeq_gt k a d hdk hk⟩

/-! ## The extension lemma -/

theorem extension : ExtensionClaim := by
  intro k a hseed
  obtain ⟨hk, ha3, hmono, hbud⟩ := hseed
  set b : ℕ → ℝ := bootstrapSeq k a with hbdef
  have hseedb : ∀ d, 3 ≤ d → d ≤ k → b d = a d := fun d h3 hdk =>
    bootstrapSeq_seed k a d h3 hdk
  have hb0 : ∀ d, d ≤ 2 → b d = 0 := fun d hd => bootstrapSeq_le_two k a d hd
  have hb2 : b 2 = 0 := hb0 2 le_rfl
  have hgt : ∀ d, k < d → b d = bootStep d (b (d - 1)) (runMin b (d - 1)) := fun d hdk =>
    bootstrapSeq_gt k a d hdk hk
  -- increments up to `k` are nonnegative
  have hinc : ∀ i, 3 ≤ i → i ≤ k → 0 ≤ incr b i := by
    intro i h3 hik
    simp only [incr]
    rcases Nat.eq_or_lt_of_le h3 with rfl | h4
    · rw [hseedb 3 le_rfl hik, hb2]; simpa using ha3
    · rw [hseedb i h3 hik, hseedb (i - 1) (by omega) (by omega)]
      have := hmono (i - 1) (by omega) (by omega)
      rw [show i - 1 + 1 = i by omega] at this
      linarith
  have hH0 : 0 ≤ runMin b k := runMin_nonneg_of b k hk hinc
  -- budget at `k`
  have hbk : b k + runMin b k ≤ 1 := by
    have e : runMin (seedSeq a) k = runMin b k := by
      apply runMin_congr _ _ k hk
      intro i hi
      by_cases h2 : i ≤ 2
      · simp [seedSeq, h2, bootstrapSeq_le_two k a i h2, hbdef]
      · simp only [seedSeq, h2, ↓reduceIte]
        exact (hseedb i (by omega) hi).symm
    rw [hseedb k hk le_rfl, ← e]
    exact hbud
  -- invariant for `d ≥ k`
  have hinv : ∀ d, k ≤ d → 0 ≤ runMin b d ∧ b d + runMin b d ≤ 1 := by
    intro d hd
    induction d, hd using Nat.le_induction with
    | base => exact ⟨hH0, hbk⟩
    | succ d hd ih =>
      have hd3 : 3 ≤ d := by omega
      obtain ⟨h1, h2, h3⟩ := bootStep_spec (d + 1) (by omega) (b (d + 1 - 1))
        (runMin b (d + 1 - 1)) (by simpa using ih.1) (by simpa using ih.2)
      have e : b (d + 1) = bootStep (d + 1) (b d) (runMin b d) := by
        simpa using hgt (d + 1) (by omega)
      rw [show d + 1 - 1 = d by omega, ← e] at h1 h2 h3
      have hr : runMin b (d + 1) = min (runMin b d) (b (d + 1) - b d) := by
        rw [runMin_succ b d hd3]; simp [incr]
      rw [hr]
      refine ⟨h2, ?_⟩
      have hd1 : (1 : ℝ) ≤ (d + 1 : ℕ) - 1 := by
        have : (1 : ℝ) ≤ d := by exact_mod_cast (by omega : 1 ≤ d)
        push_cast; linarith
      nlinarith [ih.1]
  -- step facts for `d > k`
  have hstep : ∀ d, k < d → b (d - 1) ≤ b d ∧
      1 - b d = ((d : ℝ) - 1) * runMin b d + runMin b (d - 1) := by
    intro d hdk
    obtain ⟨m, rfl⟩ : ∃ m, d = m + 1 := ⟨d - 1, by omega⟩
    simp only [Nat.add_sub_cancel]
    have ih := hinv m (by omega)
    obtain ⟨h1, h2, h3⟩ := bootStep_spec (m + 1) (by omega) (b m) (runMin b m) ih.1
      (by linarith [ih.2])
    have e : b (m + 1) = bootStep (m + 1) (b m) (runMin b m) := by
      simpa using hgt (m + 1) hdk
    rw [← e] at h1 h2 h3
    have hr : runMin b (m + 1) = min (runMin b m) (b (m + 1) - b m) := by
      rw [runMin_succ b m (by omega)]; simp [incr]
    rw [hr]
    refine ⟨h1, ?_⟩
    push_cast at h3 ⊢
    linarith
  have hmonoAll : ∀ d, 3 ≤ d → b (d - 1) ≤ b d := by
    intro d h3
    by_cases hdk : d ≤ k
    · have := hinc d h3 hdk
      simp only [incr] at this
      linarith
    · exact (hstep d (by omega)).1
  have hchain : ∀ i j, 3 ≤ i → i ≤ j → b i ≤ b j := by
    intro i j hi hij
    induction j, hij using Nat.le_induction with
    | base => exact le_rfl
    | succ j hj ih =>
      have := hmonoAll (j + 1) (by omega)
      simp only [Nat.add_sub_cancel] at this
      linarith
  have hHall : ∀ d, 0 ≤ runMin b d := by
    intro d
    by_cases h3 : 3 ≤ d
    · apply runMin_nonneg_of b d h3
      intro i hi _
      have := hmonoAll i hi
      simp only [incr]
      linarith
    · rw [runMin_le_three b d (by omega)]
      have := hmonoAll 3 le_rfl
      simp only [incr]
      linarith
  refine ⟨hk, ⟨hb0 0 (by omega), hb0 1 (by omega), hb2⟩, hmonoAll, ?_, ?_, ?_, fun d => ?_⟩
  · intro d hd
    simp only [← runMin_eq_t4]
    exact (hstep d (by omega)).2
  · intro d hd
    simp only [← runMin_eq_t4]
    exact (hinv d hd).2
  · intro d
    simp only [← runMin_eq_t4]
    exact hHall d
  by_cases hdk : d ≤ k
  · by_cases h2 : d ≤ 2
    · rw [hb0 d h2]; norm_num
    · have := hchain d k (by omega) hdk
      have := hbk
      have := hHall k
      linarith
  · have := (hinv d (by omega)).2
    have := hHall d
    linarith

end PwSeq
end CubicPathwidth

#print axioms CubicPathwidth.PwSeq.targetBootSeq
#print axioms CubicPathwidth.PwSeq.extension