Sheppard's crossing bound

A threshold separates two unit Gaussian 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; this file proves the inequality at every threshold. It sharpens gaussPi_between_le, replacing the ratio y = ‖β - α‖ / ‖α + β‖ in its bound (2/π) y with arctan y ≤ y.

• gaussPi_abs_le_mul_abs: for independent standard Gaussians Z₁ and Z₂, the event |Z₁| ≤ k |Z₂| has probability (2/π) arctan k.
• gaussPi_between_le_arctan: for coefficient vectors of equal norm with nonzero sum, a threshold separates the two forms with probability at most (2/π) arctan (‖β - α‖ / ‖α + β‖). The forms form (α + β) and form (β - α) are independent, and a crossing forces the first to lie within the absolute value of the second around twice the threshold. A centered Gaussian gives a symmetric interval at least the mass of any translate, so the threshold may be taken to be zero, leaving the planar angle law.
• two_mul_arctan_tanHalf: 2 arctan (tanHalf x) = arccos x.
• gaussPi_between_le_arccos: the bound arccos ρ / π for unit forms.

theorem Algebraic.Cutwidth.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₁| ≤ k |Z₂| has probability (2/π) arctan k.

theorem Algebraic.Cutwidth.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 at every threshold. For coefficient vectors of equal norm with nonzero sum, a threshold separates the two Gaussian forms with probability at most (2/π) arctan (‖β - α‖ / ‖α + β‖).

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

2 arctan (tan (θ/2)) = θ in the form 2 arctan (tanHalf x) = arccos x.

theorem Algebraic.Cutwidth.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 for unit forms. A threshold separates two unit Gaussian forms with probability at most arccos ρ / π, where ρ is their correlation.