Prove2Me

(28), p. 11 — Gaussian tail bound

Proved
QuantumLinSys.Fourier.eq_28

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

gaussian-tailharmonic-analysisp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For every zK≥0z_K\ge0, the upper tail of the standard Gaussian satisfies

12π∫zK∞e−z2/2 dz≤12e−zK2/2.\frac1{\sqrt{2\pi}}\int_{z_K}^{\infty} e^{-z^2/2}\,dz \le \frac12 e^{-z_K^2/2}.

This is the tail estimate used in the truncation analysis of Lemma 12.

Formalization Note The nonnegative cutoff is the regime of the cited Gaussian-tail inequality; it is needed because the displayed bound is false for a negative cutoff. The Gaussian integrand is integrable.

Preamble
import Mathlib
import Definitions.Def_QuantumLinSys_Fourier_Setting
Formal statement
namespace QuantumLinSys.Fourier

/-- The one-sided Gaussian tail estimate (28), p. 11. -/
theorem eq_28 (zK : ℝ) (hz : 0 ≤ zK) :
    1 / Real.sqrt (2 * Real.pi) *
      ∫ z in Set.Ioi zK, Real.exp (-z ^ 2 / 2) ≤
        1 / 2 * Real.exp (-zK ^ 2 / 2) := by sorry

end QuantumLinSys.Fourier
Source
Childs, Kothari and Somma, Quantum algorithm for systems of linear equations with exponentially improved dependence on precision, arXiv:1511.02306v2, p. 11, display (28)
Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph