CubicPathwidth.Sw4.FrontierVertexNum

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

import CubicPathwidth.C3.StarFrontier
import CubicPathwidth.C3.Constants
import CubicPathwidth.T2.PhiTail
import CubicPathwidth.T2.GoodLabelsCountA
import CubicPathwidth.Sw4Spec

/-!
# Numerics for the frontier vertex bound (`lem:switch4-means`, large thresholds)

For `τ > 35/32` the frontier probability is at most `Φ(-τ) ≤ Φ(-35/32)`, and
`Φ(-35/32) < c₃` (`≈ 0.13703 < 0.13982`). Both sides are bounded by elementary series:

* `Φ(-x) = 1/2 - ∫₀ˣ φ`, `φ(t) ≥ (2π)^{-1/2} (1 - t²/2 + t⁴/8 - t⁶/48 - 5t⁸/1536)` from
  `Real.exp_bound`, giving `Φ(-35/32) ≤ 0.1377`;
* `c₃ > 0.138`, from `cos 0.58 > 5/6` (via `sin_bound`) and `π < 3.1416`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace Sw4
namespace FV

open T2

/-! ## Lower bound for the Gaussian density -/

theorem exp_neg_ge {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) :
    1 - u + u ^ 2 / 2 - u ^ 3 / 6 - 5 / 96 * u ^ 4 ≤ Real.exp (-u) := by
  have hx : |(-u)| ≤ 1 := by rw [abs_neg, abs_of_nonneg hu0]; exact hu1
  have h := Real.exp_bound hx (n := 4) (by norm_num)
  rw [abs_neg, abs_of_nonneg hu0] at h
  have h2 := (abs_le.mp h).1
  simp [Finset.sum_range_succ, Nat.factorial] at h2
  nlinarith [h2]

/-- Polynomial minorant of `exp (-t²/2)` on `[0, 35/32]`. -/
def poly (t : ℝ) : ℝ := 1 - t ^ 2 / 2 + t ^ 4 / 8 - t ^ 6 / 48 - 5 * t ^ 8 / 1536

theorem poly_le_exp {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 35 / 32) :
    poly t ≤ Real.exp (-t ^ 2 / 2) := by
  have hu0 : 0 ≤ t ^ 2 / 2 := by positivity
  have hu1 : t ^ 2 / 2 ≤ 1 := by nlinarith
  have h := exp_neg_ge hu0 hu1
  have e : -t ^ 2 / 2 = -(t ^ 2 / 2) := by ring
  rw [e]
  unfold poly
  nlinarith [h]

theorem integral_poly (x : ℝ) :
    ∫ t in (0 : ℝ)..x, poly t =
      x - x ^ 3 / 6 + x ^ 5 / 40 - x ^ 7 / 336 - 5 * x ^ 9 / 13824 := by
  unfold poly
  have hd : ∀ y ∈ Set.uIcc (0 : ℝ) x, HasDerivAt
      (fun t : ℝ => t - t ^ 3 / 6 + t ^ 5 / 40 - t ^ 7 / 336 - 5 * t ^ 9 / 13824)
      (1 - y ^ 2 / 2 + y ^ 4 / 8 - y ^ 6 / 48 - 5 * y ^ 8 / 1536) y := by
    intro y _
    have h := ((((hasDerivAt_id y).sub ((hasDerivAt_pow 3 y).div_const 6)).add
      ((hasDerivAt_pow 5 y).div_const 40)).sub ((hasDerivAt_pow 7 y).div_const 336)).sub
      ((hasDerivAt_pow 9 y).const_mul 5 |>.div_const 13824)
    convert h using 1
    · ext t; simp
    · simp; ring
  rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hd
    (by apply Continuous.intervalIntegrable; fun_prop)]
  simp

/-- The mass of `[0, 35/32)` under the standard normal law. -/
theorem real_Ico_ge :
    (Real.sqrt (2 * Real.pi))⁻¹ * (∫ t in (0 : ℝ)..(35 / 32), poly t) ≤
      (gaussianReal 0 1).real (Set.Ico 0 (35 / 32)) := by
  rw [Measure.real, gaussianReal_apply_eq_integral 0 one_ne_zero,
    ENNReal.toReal_ofReal (setIntegral_nonneg measurableSet_Ico
      (fun x _ => gaussianPDFReal_nonneg 0 1 x))]
  have hcont : Continuous poly := by unfold poly; fun_prop
  have h1 : (Real.sqrt (2 * Real.pi))⁻¹ * (∫ t in (0 : ℝ)..(35 / 32), poly t) =
      ∫ t in Set.Ico (0 : ℝ) (35 / 32), (Real.sqrt (2 * Real.pi))⁻¹ * poly t := by
    rw [integral_const_mul, intervalIntegral.integral_of_le (by norm_num),
      integral_Ico_eq_integral_Ioo, integral_Ioc_eq_integral_Ioo]
  rw [h1]
  refine setIntegral_mono_on (((hcont.const_mul _).integrableOn_Icc).mono_set Set.Ico_subset_Icc_self)
    (integrable_gaussianPDFReal 0 1).integrableOn measurableSet_Ico ?_
  intro t ht
  have hc : 0 ≤ (Real.sqrt (2 * Real.pi))⁻¹ := by positivity
  have := mul_le_mul_of_nonneg_left (poly_le_exp ht.1 ht.2.le) hc
  simpa [gaussianPDFReal] using this

/-- `Φ(-35/32) ≤ 0.1377`. -/
theorem Phi_neg_le : Phi (-(35 / 32)) ≤ 1377 / 10000 := by
  have hn : NullSingletonClass (gaussianReal 0 1) := nullSingletonClass_gaussianReal (by norm_num)
  have h0 : (gaussianReal 0 1).real (Set.Ici 0) = 1 / 2 := C3.Ideal.gaussianReal_Ici_zero
  have hsub : Set.Ici (35 / 32 : ℝ) ⊆ Set.Ici 0 := Set.Ici_subset_Ici.mpr (by norm_num)
  have hd := measureReal_sdiff (μ := gaussianReal 0 1) hsub measurableSet_Ici
  rw [Set.Ici_sdiff_Ici, h0] at hd
  have hP : Phi (-(35 / 32)) = 1 / 2 - (gaussianReal 0 1).real (Set.Ico 0 (35 / 32)) := by
    rw [← GLC.Phi_neg_eq_Ici]; linarith
  rw [hP]
  have hI := real_Ico_ge
  rw [integral_poly] at hI
  have hs : Real.sqrt (2 * Real.pi) < 25067 / 10000 := by
    rw [Real.sqrt_lt' (by norm_num)]
    have := Real.pi_lt_d4
    norm_num at this ⊢
    nlinarith
  have hs0 : 0 < Real.sqrt (2 * Real.pi) := by positivity
  have hinv : 10000 / 25067 < (Real.sqrt (2 * Real.pi))⁻¹ := by
    rw [lt_inv_comm₀ (by norm_num) hs0]
    simpa using hs
  have hI0 : (0 : ℝ) < 35 / 32 - (35 / 32) ^ 3 / 6 + (35 / 32) ^ 5 / 40 - (35 / 32) ^ 7 / 336 -
      5 * (35 / 32) ^ 9 / 13824 := by norm_num
  have key := mul_le_mul_of_nonneg_right hinv.le hI0.le
  norm_num at key hI ⊢
  linarith

/-- `cos (29/50) > 5/6`. -/
theorem cos_gt : (5 / 6 : ℝ) < Real.cos (58 / 100) := by
  have hb := Real.sin_bound (x := (29 / 100 : ℝ)) (by norm_num [abs_of_pos])
  have hs0 : 0 ≤ Real.sin (29 / 100) := Real.sin_nonneg_of_nonneg_of_le_pi (by norm_num)
    (by linarith [Real.pi_gt_three])
  have hle := (abs_le.mp hb).2
  norm_num [abs_of_pos] at hle
  have h2 : Real.cos (58 / 100) = 1 - 2 * Real.sin (29 / 100) ^ 2 := by
    have := Real.cos_two_mul (29 / 100 : ℝ)
    rw [Real.cos_sq'] at this
    rw [show (58 / 100 : ℝ) = 2 * (29 / 100) by norm_num, this]
    ring
  rw [h2]
  nlinarith

theorem arccos_gt : (58 / 100 : ℝ) < Real.arccos (5 / 6) := by
  have h := Real.arccos_lt_arccos (by norm_num : (-1 : ℝ) ≤ 5 / 6) cos_gt (Real.cos_le_one _)
  rwa [Real.arccos_cos (by norm_num) (by linarith [Real.pi_gt_three])] at h

/-- `0.138 < c₃`. -/
theorem c3_gt : (138 / 1000 : ℝ) < C3.c3 := by
  have hpi := Real.pi_lt_d4
  have hp0 := Real.pi_pos
  have h := arccos_gt
  unfold C3.c3
  rw [div_mul_eq_mul_div, lt_div_iff₀ (by positivity)]
  norm_num at hpi
  nlinarith

/-- `c₃ ≤ 0.2627`. -/
theorem c3_le_aM : C3.c3 ≤ aM := by
  have h := C3.arccos_five_sixths_lt
  have hp := Real.pi_gt_three
  have hp0 := Real.pi_pos
  unfold C3.c3 aM
  rw [div_mul_eq_mul_div, div_le_iff₀ (by positivity)]
  nlinarith [Real.arccos_nonneg (5 / 6)]

theorem Phi_neg_lt_c3 : Phi (-(35 / 32)) < C3.c3 := by
  have := Phi_neg_le
  have := c3_gt
  linarith

end FV
end Sw4
end CubicPathwidth