CubicPathwidth.T4.SeqH

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

import CubicPathwidth.T4.Defs

/-!
# (E1) for the bootstrap sequence `sigma`: `seqClaim_h : SeqClaim`

Write `u_d = 1 - sigma d`. With `k : ℕ` the basic facts are:
* `seqH_rec`: `(k+7) σ_{k+7} = (k+5) σ_{k+6} + σ_{k+5} + 1` (the defining recurrence);
* `seqH_D`: `(k+6) u_{k+6} + u_{k+5} = 129/32` (conserved deficit);
* `seqH_inv`: `0 < u_{k+5}`, `(k+10) u_{k+5} ≤ (k+13) u_{k+6}`,
  `(k+9) u_{k+6} ≤ (k+8) u_{k+5}` (joint induction on `k`);
* `seqH_hdec`: the increments `h_d = σ_d - σ_{d-1}` are nonincreasing for `d ≥ 4`;
* `seqH_runMin`: `runMin sigma d = h_d` for `d ≥ 4`.
-/

namespace CubicPathwidth
namespace T4

lemma seqH_rec (k : ℕ) :
    ((k : ℝ) + 7) * sigma (k + 7) = ((k : ℝ) + 5) * sigma (k + 6) + sigma (k + 5) + 1 := by
  have hk : (k : ℝ) + 7 ≠ 0 := by positivity
  have e : sigma (k + 7)
      = (((k : ℝ) + 5) * sigma (k + 6) + sigma (k + 5) + 1) / ((k : ℝ) + 7) := rfl
  rw [e]
  field_simp

lemma seqH_rec_shift (k : ℕ) :
    ((k : ℝ) + 8) * sigma (k + 8) = ((k : ℝ) + 6) * sigma (k + 7) + sigma (k + 6) + 1 := by
  have R := seqH_rec (k + 1)
  rw [show k + 1 + 7 = k + 8 by omega, show k + 1 + 6 = k + 7 by omega,
    show k + 1 + 5 = k + 6 by omega] at R
  push_cast at R
  linear_combination R

lemma seqH_D (k : ℕ) :
    ((k : ℝ) + 6) * (1 - sigma (k + 6)) + (1 - sigma (k + 5)) = 129 / 32 := by
  induction k with
  | zero => norm_num [sigma]
  | succ j ih =>
    have h := seqH_rec j
    rw [show j + 1 + 6 = j + 7 by omega, show j + 1 + 5 = j + 6 by omega]
    push_cast
    linear_combination ih - h

lemma seqH_inv (k : ℕ) :
    0 < 1 - sigma (k + 5) ∧
    ((k : ℝ) + 10) * (1 - sigma (k + 5)) ≤ ((k : ℝ) + 13) * (1 - sigma (k + 6)) ∧
    ((k : ℝ) + 9) * (1 - sigma (k + 6)) ≤ ((k : ℝ) + 8) * (1 - sigma (k + 5)) := by
  induction k with
  | zero => norm_num [sigma]
  | succ j ih =>
    obtain ⟨ha, hL, hU⟩ := ih
    have F := seqH_rec j
    rw [show j + 1 + 5 = j + 6 by omega, show j + 1 + 6 = j + 7 by omega]
    push_cast
    have hj : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j
    have hb : 0 < 1 - sigma (j + 6) := by nlinarith [mul_nonneg hj ha.le]
    have E2 : ((j : ℝ) + 7) * (((j : ℝ) + 14) * (1 - sigma (j + 7))
        - ((j : ℝ) + 11) * (1 - sigma (j + 6)))
        = ((j : ℝ) + 14) * (1 - sigma (j + 5)) - (7 - (j : ℝ)) * (1 - sigma (j + 6)) := by
      linear_combination (-((j : ℝ) + 14)) * F
    have K : 0 ≤ ((j : ℝ) + 14) * (1 - sigma (j + 5)) - (7 - (j : ℝ)) * (1 - sigma (j + 6)) := by
      rcases le_total (j : ℝ) 7 with h7 | h7
      · have P : 0 ≤ ((j : ℝ) + 9) * (((j : ℝ) + 14) * (1 - sigma (j + 5))
            - (7 - (j : ℝ)) * (1 - sigma (j + 6))) := by
          nlinarith [mul_nonneg (sub_nonneg.2 h7) (sub_nonneg.2 hU),
            mul_nonneg (mul_nonneg hj hj) ha.le, mul_nonneg hj ha.le]
        exact (mul_nonneg_iff_of_pos_left (by linarith)).1 P
      · nlinarith [mul_nonneg (sub_nonneg.2 h7) hb.le, mul_nonneg hj ha.le]
    have E1 : ((j : ℝ) + 7) * (((j : ℝ) + 9) * (1 - sigma (j + 6))
        - ((j : ℝ) + 10) * (1 - sigma (j + 7)))
        = ((j : ℝ) + 13) * (1 - sigma (j + 6)) - ((j : ℝ) + 10) * (1 - sigma (j + 5)) := by
      linear_combination ((j : ℝ) + 10) * F
    refine ⟨hb, ?_, ?_⟩
    · have P : 0 ≤ ((j : ℝ) + 7) * (((j : ℝ) + 14) * (1 - sigma (j + 7))
          - ((j : ℝ) + 11) * (1 - sigma (j + 6))) := by
        rw [E2]; exact K
      have Q := (mul_nonneg_iff_of_pos_left (by linarith : (0 : ℝ) < (j : ℝ) + 7)).1 P
      nlinarith
    · have P : 0 ≤ ((j : ℝ) + 7) * (((j : ℝ) + 9) * (1 - sigma (j + 6))
          - ((j : ℝ) + 10) * (1 - sigma (j + 7))) := by
        rw [E1]; nlinarith
      have Q := (mul_nonneg_iff_of_pos_left (by linarith : (0 : ℝ) < (j : ℝ) + 7)).1 P
      nlinarith

lemma seqH_U (k : ℕ) :
    ((k : ℝ) + 10) * (1 - sigma (k + 7)) ≤ ((k : ℝ) + 9) * (1 - sigma (k + 6)) := by
  have h := (seqH_inv (k + 1)).2.2
  rw [show k + 1 + 6 = k + 7 by omega, show k + 1 + 5 = k + 6 by omega] at h
  push_cast at h
  nlinarith

lemma seqH_hdec (k : ℕ) :
    sigma (k + 8) - sigma (k + 7) ≤ sigma (k + 7) - sigma (k + 6) := by
  have R := seqH_rec_shift k
  have U := seqH_U k
  have key : ((k : ℝ) + 8) * (sigma (k + 8) - sigma (k + 7))
      ≤ ((k : ℝ) + 8) * (sigma (k + 7) - sigma (k + 6)) := by
    nlinarith
  exact le_of_mul_le_mul_left key (by positivity)

lemma seqH_hstep (j : ℕ) :
    sigma (j + 5) - sigma (j + 4) ≤ sigma (j + 4) - sigma (j + 3) := by
  rcases Nat.lt_or_ge j 3 with h | h
  · interval_cases j <;> norm_num [sigma]
  · obtain ⟨k, rfl⟩ : ∃ k, j = k + 3 := ⟨j - 3, by omega⟩
    have H := seqH_hdec k
    rw [show k + 3 + 5 = k + 8 by omega, show k + 3 + 4 = k + 7 by omega,
      show k + 3 + 3 = k + 6 by omega]
    exact H

lemma seqH_runMin (k : ℕ) : runMin sigma (k + 4) = sigma (k + 4) - sigma (k + 3) := by
  induction k with
  | zero => norm_num [runMin, incr, sigma, min_def]
  | succ j ih =>
    show min (runMin sigma (j + 4)) (incr sigma (j + 5)) = sigma (j + 5) - sigma (j + 4)
    rw [ih]
    exact min_eq_right (seqH_hstep j)

lemma seqH_identity (d : ℕ) (hd : 6 ≤ d) :
    1 - sigma d = ((d : ℝ) - 1) * runMin sigma d + runMin sigma (d - 1) := by
  obtain ⟨k, rfl⟩ : ∃ k, d = k + 6 := ⟨d - 6, by omega⟩
  have R1 := seqH_runMin (k + 2)
  have R2 := seqH_runMin (k + 1)
  rw [show k + 2 + 4 = k + 6 by omega, show k + 2 + 3 = k + 5 by omega] at R1
  rw [show k + 1 + 4 = k + 5 by omega, show k + 1 + 3 = k + 4 by omega] at R2
  rw [show k + 6 - 1 = k + 5 by omega, R1, R2]
  push_cast
  rcases k with _ | j
  · norm_num [sigma]
  · have D1 := seqH_D (j + 1)
    have D0 := seqH_D j
    rw [show j + 1 + 6 = j + 7 by omega, show j + 1 + 5 = j + 6 by omega] at D1
    rw [show j + 1 + 6 = j + 7 by omega, show j + 1 + 5 = j + 6 by omega,
      show j + 1 + 4 = j + 5 by omega]
    push_cast at D1 ⊢
    linear_combination D1 - D0

lemma seqH_mono (d : ℕ) (hd : 3 ≤ d) : sigma (d - 1) ≤ sigma d := by
  rcases (show d = 3 ∨ d = 4 ∨ d = 5 ∨ d = 6 ∨ 7 ≤ d by omega) with h | h | h | h | h
  · subst h; norm_num [sigma]
  · subst h; norm_num [sigma]
  · subst h; norm_num [sigma]
  · subst h; norm_num [sigma]
  · obtain ⟨k, rfl⟩ : ∃ k, d = k + 7 := ⟨d - 7, by omega⟩
    rw [show k + 7 - 1 = k + 6 by omega]
    have hA := (seqH_inv k).1
    have hB := (seqH_inv k).2.1
    have E : ((k : ℝ) + 7) * (sigma (k + 7) - sigma (k + 6))
        = 2 * (1 - sigma (k + 6)) - (1 - sigma (k + 5)) := by
      linear_combination seqH_rec k
    have P : 0 ≤ 2 * (1 - sigma (k + 6)) - (1 - sigma (k + 5)) := by
      nlinarith [mul_nonneg (Nat.cast_nonneg k : (0 : ℝ) ≤ k) hA.le, (Nat.cast_nonneg k : (0 : ℝ) ≤ k)]
    have Q : 0 ≤ ((k : ℝ) + 7) * (sigma (k + 7) - sigma (k + 6)) := by rw [E]; exact P
    have Q' := (mul_nonneg_iff_of_pos_left (by positivity : (0 : ℝ) < (k : ℝ) + 7)).1 Q
    linarith

lemma seqH_le_one (d : ℕ) : sigma d ≤ 1 := by
  rcases Nat.lt_or_ge d 5 with h | h
  · interval_cases d <;> norm_num [sigma]
  · obtain ⟨k, rfl⟩ : ∃ k, d = k + 5 := ⟨d - 5, by omega⟩
    linarith [(seqH_inv k).1]

lemma seqH_tail (j : ℕ) : sigma (j + 11) - sigma (j + 10) ≤ 1 / 32 := by
  induction j with
  | zero => norm_num [sigma]
  | succ i ih =>
    have H := seqH_hdec (i + 4)
    rw [show i + 4 + 8 = i + 12 by omega, show i + 4 + 7 = i + 11 by omega,
      show i + 4 + 6 = i + 10 by omega] at H
    rw [show i + 1 + 11 = i + 12 by omega, show i + 1 + 10 = i + 11 by omega]
    linarith

lemma seqH_coeff (d : ℕ) : sigma d ≤ thm4Coeff d := by
  rcases Nat.lt_or_ge d 11 with h | h
  · interval_cases d <;> norm_num [sigma, thm4Coeff]
  · obtain ⟨k, rfl⟩ : ∃ k, d = k + 11 := ⟨d - 11, by omega⟩
    have hT := seqH_tail k
    have hD := seqH_D (k + 5)
    rw [show k + 5 + 6 = k + 11 by omega, show k + 5 + 5 = k + 10 by omega] at hD
    push_cast at hD
    have h1 : ¬ (k + 11 ≤ 2) := by omega
    have h2 : ¬ (k + 11 ≤ 6) := by omega
    have h3 : ¬ (k + 11 ≤ 10) := by omega
    have hc : thm4Coeff (k + 11) = 1 - 4 / ((k : ℝ) + 11 + 1) := by
      unfold thm4Coeff
      norm_num [h1, h2, h3]
    rw [hc]
    have key : 4 / ((k : ℝ) + 11 + 1) ≤ 1 - sigma (k + 11) := by
      rw [div_le_iff₀ (by positivity)]
      nlinarith
    linarith

theorem seqClaim_h : SeqClaim := by
  refine ⟨⟨⟨by norm_num [sigma], by norm_num [sigma], by norm_num [sigma]⟩,
    seqH_mono, seqH_identity, seqH_le_one⟩, seqH_coeff⟩

end T4
end CubicPathwidth

#print axioms CubicPathwidth.T4.seqClaim_h