Threshold crossings of Gaussian forms

Three probability bounds for linear forms in independent standard Gaussians.

• gaussPi_between_le: for coefficient vectors α and β of equal norm, a threshold separates form α and form β with probability at most (2/π) ‖β - α‖ / ‖α + β‖. The forms form (α + β) and form (β - α) are independent Gaussians, and the crossing forces the first to lie within the absolute value of the second around twice the threshold. The bound multiplies the peak density of the first by the mean absolute value of the second.
• gaussPi_window_le: a unit form lands in a half-open window of width δ with probability at most δ / √(2π), the peak density times the width.
• gaussPi_tail_le: Chebyshev's tail bound 1 / T² for a unit form.

theorem Algebraic.Cutwidth.Gaussian.measurable_form {ι : Type} [Fintype ι] (α : ι → ℝ) : Measurable (form α)

A Gaussian form is a measurable function of the sample.

theorem Algebraic.Cutwidth.Gaussian.gaussPi_between_le {ι : Type} [Fintype ι] (α β : ι → ℝ) (hnorm : ∑ i : ι, α i ^ 2 = ∑ i : ι, β i ^ 2) (hsum : 0 < ∑ i : ι, (α i + β i) ^ 2) (t : ℝ) : (gaussPi ι).real {ω : ι → ℝ | Between t (form α ω) (form β ω)} ≤ 2 / Real.pi * (√(∑ i : ι, (β i - α i) ^ 2) / √(∑ i : ι, (α i + β i) ^ 2))

Threshold crossing. For coefficient vectors of equal norm whose sum is nonzero, the probability that a threshold separates the two Gaussian forms is at most (2/π) ‖β - α‖ / ‖α + β‖.

theorem Algebraic.Cutwidth.Gaussian.gaussPi_window_le {ι : Type} [Fintype ι] (α : ι → ℝ) (hα : ∑ i : ι, α i ^ 2 = 1) (s : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) : (gaussPi ι).real {ω : ι → ℝ | s ≤ form α ω ∧ form α ω < s + δ} ≤ δ / √(2 * Real.pi)

A unit Gaussian form lands in a window of width δ with probability at most δ / √(2π).

theorem Algebraic.Cutwidth.Gaussian.gaussPi_tail_le {ι : Type} [Fintype ι] (α : ι → ℝ) (hα : ∑ i : ι, α i ^ 2 = 1) {T : ℝ} (hT : 0 < T) : (gaussPi ι).real {ω : ι → ℝ | T ≤ |form α ω|} ≤ 1 / T ^ 2

Chebyshev's tail bound for a unit Gaussian form.