Gaussian kernel, tail, and translated interval mass for convex folding

Definition

Komlos_gaussian_fold_analysis

by Wenqian · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

banaszczykgaussian-measure

For real $x$ and $r$ , define the unnormalized Gaussian density, its upper tail, and its translated interval integral by

g(x)=e^{-x^2/2},\qquad T(x)=\int_x^\infty g(t)\,dt,\qquad A_r(x)=\int_x^{x+r}g(t)\,dt.

For $r\ge0$ , $A_r(x)$ is the unnormalized mass of an interval of length $r$ . These quantities describe the one-dimensional integrals in the planar comparison used in Banaszczyk's folding argument. For negative $r$ , the interval integral has its usual oriented meaning.

Definition code

import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv

open Set MeasureTheory
open scoped intervalIntegral
set_option autoImplicit false

namespace GaussianFoldAnalysis
noncomputable def kernel (x : ℝ) : ℝ := Real.exp (-x ^ 2 / 2)
noncomputable def tail (x : ℝ) : ℝ := ∫ t in Ioi x, kernel t
noncomputable def intervalMass (r x : ℝ) : ℝ := ∫ t in x..x + r, kernel t
end GaussianFoldAnalysis

Source

Shashwat Garg, Algorithms for Combinatorial Discrepancy, TU Eindhoven PhD thesis (2018), Chapter 3, proof of Lemma 19 and Lemmas 20-21, printed pp. 22-24. https://pure.tue.nl/ws/files/107722737/20181010_Garg.pdf . The notation g,T,A packages the Gaussian integrands and intervals appearing there; no normalizing factor is included.

View graph