CubicPathwidth.T3.PhiTail5

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

import CubicPathwidth.T2.PhiTail
import CubicPathwidth.T2.FcubicBounds

/-!
# Numerical tail bounds for `5 Φ(-3)`

Sharper numerics than `4 Φ(-3) ≤ 1/50`: from `Φ(-3) ≤ (√(2π))⁻¹ e^{-9/2} / 3`
with `√(2π) ≥ 5/2` and `e^{9/2} ≥ 38`, one gets `Φ(-3) ≤ 1/285`, hence
`5 Φ(-3) ≤ 1/57 ≤ 1/50 ≤ Fcubic`.
-/

noncomputable section

namespace CubicPathwidth
namespace T3

/-- `5 Φ(-3) ≤ 1/50`. -/
theorem five_Phi_neg_three_le : 5 * T2.Phi (-3) ≤ 1 / 50 := by
  have hA := T2.Phi_neg_three_le_aux
  have hs : (5 / 2 : ℝ) ≤ Real.sqrt (2 * Real.pi) := by
    apply Real.le_sqrt_of_sq_le
    nlinarith [Real.pi_gt_d2]
  have hinv : (Real.sqrt (2 * Real.pi))⁻¹ ≤ 2 / 5 := by
    have h := inv_anti₀ (by norm_num : (0 : ℝ) < 5 / 2) hs
    have e : ((5 : ℝ) / 2)⁻¹ = 2 / 5 := by norm_num
    linarith
  have hE : (38 : ℝ) ≤ Real.exp (9 / 2) := by
    have h1 : (3 / 2 : ℝ) ≤ Real.exp (1 / 2) := by
      have := Real.add_one_le_exp (1 / 2 : ℝ)
      linarith
    have h2 : Real.exp (9 / 2) = Real.exp (1 / 2) ^ 9 := by
      rw [← Real.exp_nat_mul]; norm_num
    have h3 : (3 / 2 : ℝ) ^ 9 ≤ Real.exp (1 / 2) ^ 9 :=
      pow_le_pow_left₀ (by norm_num) h1 9
    rw [h2]
    norm_num at h3 ⊢
    linarith
  have hneg : Real.exp (-(9 / 2)) ≤ 1 / 38 := by
    rw [Real.exp_neg]
    have := inv_anti₀ (by norm_num : (0 : ℝ) < 38) hE
    simpa [one_div] using this
  have hpos : 0 ≤ Real.exp (-(9 / 2)) := (Real.exp_pos _).le
  have hcpos : 0 ≤ (Real.sqrt (2 * Real.pi))⁻¹ := by positivity
  have h1 : (Real.sqrt (2 * Real.pi))⁻¹ * Real.exp (-(9 / 2)) ≤ (2 / 5) * (1 / 38) :=
    mul_le_mul hinv hneg hpos (by norm_num)
  have h2 : (Real.sqrt (2 * Real.pi))⁻¹ * Real.exp (-(9 / 2)) / 3 ≤
      (2 / 5) * (1 / 38) / 3 :=
    div_le_div_of_nonneg_right h1 (by norm_num)
  linarith

/-- `5 Φ(-3) ≤ Fcubic`. -/
theorem tail_P : 5 * T2.Phi (-3) ≤ T2.Fcubic :=
  le_trans five_Phi_neg_three_le T2.Fcubic_ge

/-- `5 Φ(-3) ≤ 291/2000`. -/
theorem tail_R : 5 * T2.Phi (-3) ≤ 291 / 2000 := by
  linarith [five_Phi_neg_three_le]

/-- `5 Φ(-3) ≤ 5/32`. -/
theorem tail_S : 5 * T2.Phi (-3) ≤ 5 / 32 := by
  linarith [five_Phi_neg_three_le]

end T3
end CubicPathwidth

#print axioms CubicPathwidth.T3.five_Phi_neg_three_le
Back to top