Threshold decay of Gaussian crossings

A threshold t separates two unit Gaussian forms with correlation ρ with probability at most exp (-t²/2) · arccos ρ / π. This multiplies Sheppard's bound gaussPi_between_le_arccos by the Gaussian factor exp (-t²/2), so thresholds far from the median are crossed rarely.

• prod_gaussianReal_abs_sub_le_abs_exp: for independent centered Gaussians X and Y of variances s > 0 and r, the event |X - c| ≤ |Y| has probability at most (2/π) arctan (√r / √s) exp (-c² / (2 (s + r))). In polar coordinates the event occupies, at each radius R, at most two arcs of total length 4 arctan (√r / √s), and none when R < |c| / √(s + r); the radial tail beyond that radius carries the factor exp (-c² / (2 (s + r))).
• gaussPi_between_le_arctan_exp: for coefficient vectors of equal norm with nonzero sum, a threshold t separates the two forms with probability at most (2/π) arctan (‖β - α‖ / ‖α + β‖) exp (-t² / (2 ‖α‖²)). The forms form (α + β) and form (β - α) are independent, and a crossing forces the first to lie within the absolute value of the second around 2t.
• gaussPi_between_le_exp_arccos: the bound exp (-t²/2) arccos ρ / π for unit forms.

theorem Algebraic.Cutwidth.Gaussian.prod_gaussianReal_abs_sub_le_abs_exp (s r : NNReal) (hs : s ≠ 0) (c : ℝ) : ((ProbabilityTheory.gaussianReal 0 s).prod (ProbabilityTheory.gaussianReal 0 r)) {p : ℝ × ℝ | |p.1 - c| ≤ |p.2|} ≤ ENNReal.ofReal (2 / Real.pi * Real.arctan (√↑r / √↑s) * Real.exp (-c ^ 2 / (2 * (↑s + ↑r))))

Decay of the crossing event. For independent centered Gaussians X and Y of variances s > 0 and r, the event |X - c| ≤ |Y| has probability at most (2/π) arctan (√r / √s) exp (-c² / (2 (s + r))).

theorem Algebraic.Cutwidth.Gaussian.gaussPi_between_le_arctan_exp {ι : 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)) * Real.exp (-t ^ 2 / (2 * ∑ i : ι, α i ^ 2))

Threshold decay of crossings. For coefficient vectors of equal norm with nonzero sum, a threshold t separates the two Gaussian forms with probability at most (2/π) arctan (‖β - α‖ / ‖α + β‖) exp (-t² / (2 ‖α‖²)).

theorem Algebraic.Cutwidth.Gaussian.gaussPi_between_le_exp_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.exp (-t ^ 2 / 2) * (Real.arccos (∑ i : ι, α i * β i) / Real.pi)

Threshold decay of crossings for unit forms. A threshold t separates two unit Gaussian forms of correlation ρ with probability at most exp (-t²/2) arccos ρ / π.