CubicPathwidth.Sw4.ZeroVertexNum

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

import CubicPathwidth.Sw4Spec
import CubicPathwidth.C3.Constants
import CubicPathwidth.T2.FcubicBounds
import Mathlib.Analysis.Real.Pi.Bounds
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

/-!
# Numerics for the zero-vertex lemma (Lemma A.12, `lem:switch4-zero`)

* `c3_le : c₃ ≤ 0.1401846` (used by the type `(3; 1, 2)`);
* `r34_sq_bounds : 0.8233 ≤ r₃₄² ≤ 5/6`, hence `r₃₄ ≤ r*`;
* `kappa_r34_le : κ(r₃₄) ≤ c₃ + 3 s` (used by the type `(3; 0, 3)`).

The cosine bounds come from `Real.cos_bound` at `x / 8` and three doublings
`cos 2x = 2 cos² x - 1`; no decimal oracle is used.
-/

noncomputable section

namespace CubicPathwidth
namespace Sw4

/-! ## Upper bounds for the cosine -/

theorem cos_base {x : ℝ} (h0 : 0 ≤ x) (h1 : x ≤ 1) :
    Real.cos x ≤ 1 - x ^ 2 / 2 + x ^ 4 * (5 / 96) := by
  have h := Real.cos_bound (x := x) (by rw [abs_of_nonneg h0]; exact h1)
  have h2 : |x| ^ 4 = x ^ 4 := by rw [abs_of_nonneg h0]
  have := (abs_le.mp h).2
  rw [h2] at this
  linarith

theorem cos_step {x u : ℝ} (hx0 : 0 ≤ x) (hx : x ≤ 1 / 2) (hu : Real.cos x ≤ u) :
    Real.cos (2 * x) ≤ 2 * u ^ 2 - 1 := by
  have hc : 0 ≤ Real.cos x :=
    Real.cos_nonneg_of_mem_Icc ⟨by linarith [Real.pi_pos], by linarith [Real.pi_gt_three]⟩
  rw [Real.cos_two_mul]
  nlinarith

/-- Upper bound for `cos x`: Taylor bound at `x / 8` and three doublings. -/
def cosUp (x : ℝ) : ℝ :=
  2 * (2 * (2 * (1 - (x / 8) ^ 2 / 2 + (x / 8) ^ 4 * (5 / 96)) ^ 2 - 1) ^ 2 - 1) ^ 2 - 1

theorem cos_le_cosUp {x : ℝ} (h0 : 0 ≤ x) (h1 : x ≤ 1) : Real.cos x ≤ cosUp x := by
  have e0 := cos_base (x := x / 8) (by positivity) (by linarith)
  have e1 := cos_step (x := x / 8) (by positivity) (by linarith) e0
  have e2 := cos_step (x := 2 * (x / 8)) (by positivity) (by linarith) e1
  have e3 := cos_step (x := 2 * (2 * (x / 8))) (by positivity) (by linarith) e2
  have : 2 * (2 * (2 * (x / 8))) = x := by ring
  rw [this] at e3
  exact e3

theorem cos_lt_of {x y : ℝ} (h0 : 0 ≤ x) (h1 : x ≤ 1) (h : cosUp x < y) : Real.cos x < y :=
  lt_of_le_of_lt (cos_le_cosUp h0 h1) h

/-! ## Bounds for the arccosines -/

theorem arccos_five_sixths_lt' : Real.arccos (5 / 6) < 5865 / 10000 := by
  have hcos : Real.cos (5865 / 10000) < 5 / 6 :=
    cos_lt_of (by norm_num) (by norm_num) (by unfold cosUp; norm_num)
  have hlo : (-1 : ℝ) ≤ Real.cos (5865 / 10000) := Real.neg_one_le_cos _
  have h := Real.arccos_lt_arccos hlo hcos (by norm_num)
  rwa [Real.arccos_cos (by norm_num) (by linarith [Real.pi_gt_three])] at h

theorem arccos_lt_of_p {p : ℝ} (hp : 7348 / 10000 ≤ p) (hp1 : p ≤ 1) :
    Real.arccos p < 748 / 1000 := by
  have hcos : Real.cos (748 / 1000) < p :=
    lt_of_lt_of_le (cos_lt_of (by norm_num) (by norm_num) (by unfold cosUp; norm_num)) hp
  have hlo : (-1 : ℝ) ≤ Real.cos (748 / 1000) := Real.neg_one_le_cos _
  have h := Real.arccos_lt_arccos hlo hcos hp1
  rwa [Real.arccos_cos (by norm_num) (by linarith [Real.pi_gt_three])] at h

/-- `c₃ ≤ 0.1401846`. -/
theorem c3_le : C3.c3 ≤ 1401846 / 10000000 := by
  have hA := arccos_five_sixths_lt'
  have hpi := Real.pi_gt_d4
  have hpi0 : 0 < Real.pi := Real.pi_pos
  unfold C3.c3
  rw [div_mul_eq_mul_div, div_le_iff₀ (by positivity)]
  have hA0 : 0 ≤ Real.arccos (5 / 6) := Real.arccos_nonneg _
  nlinarith

/-! ## The floor `r₃₄` -/

theorem r34_sq_bounds : 8233 / 10000 ≤ T2.r34 ^ 2 ∧ T2.r34 ^ 2 ≤ 5 / 6 := by
  unfold T2.r34
  set x := Real.log 6 / 4 with hx
  set E := Real.exp x with hEdef
  have hE0 : 0 < E := Real.exp_pos _
  have hE4 : E ^ 4 = 6 := by
    have : E ^ 4 = Real.exp (4 * x) := by
      rw [hEdef, ← Real.exp_nat_mul]; norm_num
    rw [this, hx]
    have : 4 * (Real.log 6 / 4) = Real.log 6 := by ring
    rw [this, Real.exp_log (by norm_num)]
  have hw : E ^ 2 < 2.4495 := by
    nlinarith [sq_nonneg (E ^ 2 - 2.4495), sq_nonneg (E ^ 2)]
  have hw' : 2.449 < E ^ 2 := by
    nlinarith [sq_nonneg (E ^ 2 - 2.449), sq_nonneg (E ^ 2)]
  have hcosh : Real.cosh x = (E + E⁻¹) / 2 := by
    rw [Real.cosh_eq, Real.exp_neg]
  have hc2 : Real.cosh x ^ 2 = (E ^ 2 + 2 + E⁻¹ ^ 2) / 4 := by
    rw [hcosh]; field_simp; ring
  have hF2 : E⁻¹ ^ 2 = E ^ 2 / 6 := by
    rw [inv_pow, ← hE4]
    field_simp
  have hC : Real.cosh x ^ 2 = (E ^ 2 + 2 + E ^ 2 / 6) / 4 := by rw [hc2, hF2]
  have hCpos : 0 < Real.cosh x ^ 2 := by positivity
  rw [div_pow, one_pow]
  constructor
  · rw [le_div_iff₀ hCpos, hC]; nlinarith
  · rw [div_le_iff₀ hCpos, hC]; nlinarith

theorem r34_le_rStar : T2.r34 ≤ C3.rStar := by
  have h := r34_sq_bounds.2
  have h33 : C3.rStar ^ 2 = 8 / 9 := T2.r33_sq
  have hpos : 0 < C3.rStar := T2.r33_pos
  by_contra hc
  push Not at hc
  nlinarith

theorem r34_pos' : 0 < T2.r34 := by
  unfold T2.r34
  exact one_div_pos.mpr (Real.cosh_pos _)

/-- `κ(r₃₄) ≤ c₃ + 3 s`, where `s = 0.1529003 - c₃`. -/
theorem kappa_r34_le : C3.kappa T2.r34 ≤ C3.c3 + 3 * sM := by
  have hsq := r34_sq_bounds.1
  have hp : 7348 / 10000 ≤ C3.pairCorr T2.r34 := by
    unfold C3.pairCorr; linarith
  have hp1 : C3.pairCorr T2.r34 ≤ 1 := by
    have := r34_sq_bounds.2
    unfold C3.pairCorr; linarith
  have hB := arccos_lt_of_p hp hp1
  have hA := arccos_five_sixths_lt'
  have hpi := Real.pi_gt_d4
  have hpi0 : 0 < Real.pi := Real.pi_pos
  unfold C3.kappa C3.c3 sM C3.c3
  set A := Real.arccos (5 / 6)
  set B := Real.arccos (C3.pairCorr T2.r34)
  have key : 3 / (4 * Real.pi) * (B + 2 * A) ≤ 4587009 / 10000000 := by
    rw [div_mul_eq_mul_div, div_le_iff₀ (by positivity)]
    nlinarith
  linarith

end Sw4
end CubicPathwidth

#print axioms CubicPathwidth.Sw4.c3_le
#print axioms CubicPathwidth.Sw4.r34_le_rStar
#print axioms CubicPathwidth.Sw4.kappa_r34_le
Back to top