CubicPathwidth.T2.PhiTail

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

import CubicPathwidth.T2.Defs
import CubicPathwidth.C3.GaussianTools
import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
import Mathlib.Analysis.Complex.ExponentialBounds

/-!
# Numerical tail bound `4 Φ(-3) ≤ 1/50`

Route: the exponential tilt `φ(x) ≤ (√(2π))⁻¹ e^{9/2} e^{3x}` holds for every real `x`
(it is `(x+3)² ≥ 0` in the exponent). Integrating over `(-∞, -3]` gives
`Φ(-3) ≤ (√(2π))⁻¹ e^{-9/2} / 3`, which is below `1/200`.
-/

noncomputable section
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace T2

/-- Exponential tilt bound on the standard normal density. -/
theorem gaussianPDFReal_le_tilt (x : ℝ) :
    gaussianPDFReal 0 1 x ≤
      (Real.sqrt (2 * Real.pi))⁻¹ * (Real.exp (9 / 2) * Real.exp (3 * x)) := by
  have hc : 0 ≤ (Real.sqrt (2 * Real.pi))⁻¹ := by positivity
  have hexp : Real.exp (-x ^ 2 / 2) ≤ Real.exp (9 / 2) * Real.exp (3 * x) := by
    rw [← Real.exp_add]
    apply Real.exp_le_exp.mpr
    nlinarith [sq_nonneg (x + 3)]
  have := mul_le_mul_of_nonneg_left hexp hc
  simpa [gaussianPDFReal] using this

/-- The standard normal lower-tail bound `Φ(-3) ≤ (√(2π))⁻¹ e^{-9/2} / 3`. -/
theorem Phi_neg_three_le_aux :
    Phi (-3) ≤ (Real.sqrt (2 * Real.pi))⁻¹ * Real.exp (-(9 / 2)) / 3 := by
  unfold Phi
  rw [Measure.real, gaussianReal_apply_eq_integral 0 one_ne_zero,
    ENNReal.toReal_ofReal (setIntegral_nonneg measurableSet_Iic
      (fun x _ => gaussianPDFReal_nonneg 0 1 x))]
  have hint : IntegrableOn (fun x : ℝ => (Real.sqrt (2 * Real.pi))⁻¹ *
      (Real.exp (9 / 2) * Real.exp (3 * x))) (Set.Iic (-3)) :=
    ((integrableOn_exp_mul_Iic (by norm_num : (0 : ℝ) < 3) (-3)).const_mul
      (Real.exp (9 / 2))).const_mul _
  calc (∫ x in Set.Iic (-3), gaussianPDFReal 0 1 x)
      ≤ ∫ x in Set.Iic (-3), (Real.sqrt (2 * Real.pi))⁻¹ *
          (Real.exp (9 / 2) * Real.exp (3 * x)) :=
        setIntegral_mono_on (integrable_gaussianPDFReal 0 1).integrableOn hint
          measurableSet_Iic (fun x _ => gaussianPDFReal_le_tilt x)
    _ = (Real.sqrt (2 * Real.pi))⁻¹ * (Real.exp (9 / 2) *
          (Real.exp (3 * (-3)) / 3)) := by
        rw [integral_const_mul, integral_const_mul, integral_exp_mul_Iic (by norm_num)]
    _ = (Real.sqrt (2 * Real.pi))⁻¹ * Real.exp (-(9 / 2)) / 3 := by
        have h : Real.exp (9 / 2) * Real.exp (3 * (-3)) = Real.exp (-(9 / 2)) := by
          rw [← Real.exp_add]; ring_nf
        calc _ = (Real.sqrt (2 * Real.pi))⁻¹ * (Real.exp (9 / 2) * Real.exp (3 * (-3))) / 3 := by
              ring
          _ = _ := by rw [h]

/-- `4 Φ(-3) ≤ 1/50`. -/
theorem four_Phi_neg_three_le : 4 * Phi (-3) ≤ 1 / 50 := by
  have hA := Phi_neg_three_le_aux
  have hs : (2 : ℝ) ≤ Real.sqrt (2 * Real.pi) := by
    apply Real.le_sqrt_of_sq_le
    nlinarith [Real.pi_gt_three]
  have hinv : (Real.sqrt (2 * Real.pi))⁻¹ ≤ 1 / 2 := by
    have := inv_anti₀ (by norm_num : (0 : ℝ) < 2) hs
    simpa [one_div] using this
  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 hbound : (Real.sqrt (2 * Real.pi))⁻¹ * Real.exp (-(9 / 2)) / 3 ≤ 1 / 200 := by
    have h1 : (Real.sqrt (2 * Real.pi))⁻¹ * Real.exp (-(9 / 2)) ≤ (1 / 2) * (1 / 38) :=
      mul_le_mul hinv hneg hpos (by norm_num)
    have h2 : (Real.sqrt (2 * Real.pi))⁻¹ * Real.exp (-(9 / 2)) / 3 ≤
        (1 / 2) * (1 / 38) / 3 := by
      apply div_le_div_of_nonneg_right h1 (by norm_num)
    linarith
  linarith

end T2
end CubicPathwidth
Back to top