Gaussian forms and threshold crossings

The sample space of the Gaussian layout is ι → ℝ with independent standard Gaussian coordinates (gaussPi ι). A coefficient vector α gives the score form α ω = ∑ i, α i * ω i, and Between t x y says that the threshold t separates the scores x and y, the lower one strictly below t. In the Gaussian layout of Frontier.Layouts.Gaussian, a vertex straddles t exactly when t separates two of the scores of its edges.

Under gaussPi ι the vector ω is a standard Gaussian vector of EuclideanSpace ℝ ι and form α ω is its inner product with α. Hence form α is a centered Gaussian of variance ‖α‖ ^ 2 (gaussPi_map_form), and two forms with orthogonal coefficients are jointly Gaussian and uncorrelated, so independent (gaussPi_map_form_pair).

Main results

• gaussPi_window_le: a unit form lands in a window of width δ with probability at most δ / √(2π), the peak density times the width.
• gaussPi_tail_le: Chebyshev's bound 1 / T ^ 2 on the tail of a unit form.
• gaussPi_between_le_arccos: Sheppard's bound. A threshold separates two unit forms with correlation ρ with probability at most arccos ρ / π. At threshold 0 this is Sheppard's formula for the probability that two correlated Gaussians differ in sign.

The proof of Sheppard's bound has four steps.

1. Change of variables. For coefficients of equal norm, U = form (α + β) and V = form (β - α) are independent, and a crossing at t forces |U - 2t| ≤ |V|.
2. Anderson's inequality on the line (gaussianReal_Icc_le). A centered Gaussian gives the interval [c - w, c + w] at most the mass of [-w, w]. Conditioning on V removes the shift 2t.
3. Planar angle law (gaussPi_abs_le_mul_abs). Rescaling U and V to standard Gaussians Z_1, Z_2 turns |U| ≤ |V| into |Z_1| ≤ k |Z_2| with k = ‖β - α‖ / ‖α + β‖. In polar coordinates this event constrains only the angle, to two arcs of total length 4 arctan k, so it has probability (2/π) arctan k.
4. Half-angle identity (two_mul_arctan_tanHalf). For unit vectors at angle θ, with ρ = cos θ, the ratio k is tanHalf ρ = tan (θ/2), and 2 arctan (tan (θ/2)) = θ.

@[reducible, inline]

noncomputable abbrev Complexity.Frontier.Gaussian.gaussPi (ι : Type) [Fintype ι] : MeasureTheory.Measure (ι → ℝ)

The standard Gaussian product measure on ι → ℝ.

Equations

• Complexity.Frontier.Gaussian.gaussPi ι = MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1

instance Complexity.Frontier.Gaussian.instIsProbabilityMeasureForallRealGaussPi (ι : Type) [Fintype ι] : MeasureTheory.IsProbabilityMeasure (gaussPi ι)

noncomputable def Complexity.Frontier.Gaussian.form {ι : Type} [Fintype ι] (α ω : ι → ℝ) : ℝ

The linear form ω ↦ ∑ i, α i * ω i: the score of a vertex with coefficient vector α.

Equations

• Complexity.Frontier.Gaussian.form α ω = ∑ i : ι, α i * ω i

def Complexity.Frontier.Gaussian.Between (t x y : ℝ) : Prop

The threshold t separates x and y: it lies strictly above one and weakly below the other.

Equations

• Complexity.Frontier.Gaussian.Between t x y = (x < t ∧ t ≤ y ∨ y < t ∧ t ≤ x)

noncomputable def Complexity.Frontier.Gaussian.tanHalf (x : ℝ) : ℝ

The crossing ratio √(1 - x) / √(1 + x). For unit vectors at angle θ, with inner product x = cos θ, it is tan (θ / 2).

Equations

• Complexity.Frontier.Gaussian.tanHalf x = √(1 - x) / √(1 + x)

Real Gaussians

Laws of Gaussian forms

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

A Gaussian form is a measurable function of the sample.

theorem Complexity.Frontier.Gaussian.gaussPi_map_form {ι : Type} [Fintype ι] (a : ι → ℝ) : MeasureTheory.Measure.map (form a) (gaussPi ι) = ProbabilityTheory.gaussianReal 0 (∑ i : ι, a i ^ 2).toNNReal

The law of a Gaussian form: form a is a centered Gaussian of variance ‖a‖ ^ 2.

theorem Complexity.Frontier.Gaussian.gaussPi_map_form_pair {ι : Type} [Fintype ι] (a b : ι → ℝ) (hab : ∑ i : ι, a i * b i = 0) : MeasureTheory.Measure.map (fun (ω : ι → ℝ) => (form a ω, form b ω)) (gaussPi ι) = (ProbabilityTheory.gaussianReal 0 (∑ i : ι, a i ^ 2).toNNReal).prod (ProbabilityTheory.gaussianReal 0 (∑ i : ι, b i ^ 2).toNNReal)

Orthogonal forms are independent: two Gaussian forms with orthogonal coefficients have joint law the product of their marginal laws.

Windows and tails

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

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

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

Tail bound. By Chebyshev's inequality, a unit Gaussian form has absolute value at least T with probability at most 1 / T ^ 2.

The planar angle law

theorem Complexity.Frontier.Gaussian.gaussPi_abs_le_mul_abs (k : ℝ) (hk : 0 ≤ k) : (gaussPi (Fin 2)).real {ω : Fin 2 → ℝ | |ω 0| ≤ k * |ω 1|} = 2 / Real.pi * Real.arctan k

Planar angle law. For independent standard Gaussians Z_1 and Z_2, the event |Z_1| ≤ k |Z_2| has probability (2/π) arctan k.

Anderson's inequality on the line

theorem Complexity.Frontier.Gaussian.gaussianReal_Icc_le (v : NNReal) (c w : ℝ) : (ProbabilityTheory.gaussianReal 0 v) (Set.Icc (c - w) (c + w)) ≤ (ProbabilityTheory.gaussianReal 0 v) (Set.Icc (-w) w)

Anderson's inequality on the line. A centered Gaussian gives an interval of radius w the most mass when it is centered at the mean.

Sheppard's bound

theorem Complexity.Frontier.Gaussian.gaussPi_between_le_arctan {ι : 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 * Real.arctan (√(∑ i : ι, (β i - α i) ^ 2) / √(∑ i : ι, (α i + β i) ^ 2))

Sheppard's bound for equal norms. For coefficient vectors of equal norm with nonzero sum, a threshold separates the two Gaussian forms with probability at most (2/π) arctan (‖β - α‖ / ‖α + β‖).

theorem Complexity.Frontier.Gaussian.two_mul_arctan_tanHalf {x : ℝ} (hx : -1 < x) (hx1 : x ≤ 1) : 2 * Real.arctan (tanHalf x) = Real.arccos x

Half-angle identity. 2 arctan (tan (θ/2)) = θ, in the form 2 arctan (tanHalf x) = arccos x.

theorem Complexity.Frontier.Gaussian.gaussPi_between_le_arccos {ι : Type} [Fintype ι] {α β : ι → ℝ} (hα : ∑ i : ι, α i ^ 2 = 1) (hβ : ∑ i : ι, β i ^ 2 = 1) (hx : -1 < ∑ i : ι, α i * β i) (t : ℝ) : (gaussPi ι).real {ω : ι → ℝ | Between t (form α ω) (form β ω)} ≤ Real.arccos (∑ i : ι, α i * β i) / Real.pi

Sheppard's bound. A threshold separates two unit Gaussian forms with probability at most arccos ρ / π, where ρ = ∑ i, α i * β i is their correlation.