Threshold decay of Gaussian crossings: proofs

• Angular window. Write a point of the plane as (R cos ψ, R sin ψ) with R > 0 and ψ ∈ (-π, π), and put θ = |ψ|. Then cos ψ = cos θ and |sin ψ| = sin θ, so for φ ≥ 0 the event |cos φ x - c| ≤ sin φ |y| reads R cos (θ + φ) ≤ c ≤ R cos (θ - φ). Hence |c| ≤ R, and with m = arccos (c / R), monotonicity of arccos gives |θ - m| ≤ φ. So at each radius the event occupies at most two arcs of length 2φ, and none below radius |c|.
• Radial tail. R exp (-R²/2) has antiderivative -exp (-R²/2), so its integral over R > a is exp (-a²/2).
• Decay of the angle law. In polar coordinates the standard planar Gaussian has density exp (-R²/2) / (2π). Bounding the angular slice by 4φ above radius |c| and integrating the radial tail gives (2/π) φ exp (-c²/2).
• Crossings. As in Sheppard's bound, U = form (α + β) and V = form (β - α) are independent and a crossing forces |U - 2t| ≤ |V|. Rescaling to standard Gaussians puts this event in the above form with tan φ = ‖β - α‖ / ‖α + β‖ and threshold 2t / √(‖α + β‖² + ‖β - α‖²); no Anderson step is needed.

The angular window

theorem Algebraic.Cutwidth.Gaussian.Internal.abs_sin_eq_sin_abs {ψ : ℝ} (h : |ψ| ≤ Real.pi) : |Real.sin ψ| = Real.sin |ψ|

On [-π, π], |sin ψ| = sin |ψ|.

theorem Algebraic.Cutwidth.Gaussian.Internal.abs_sub_arccos_le {θ φ y : ℝ} (hθ0 : 0 ≤ θ) (hθπ : θ ≤ Real.pi) (hφ : 0 ≤ φ) (h1 : Real.cos (θ + φ) ≤ y) (h2 : y ≤ Real.cos (θ - φ)) : |θ - Real.arccos y| ≤ φ

If cos (θ + φ) ≤ y ≤ cos (θ - φ) with θ ∈ [0, π] and φ ≥ 0, then θ lies within φ of arccos y.

theorem Algebraic.Cutwidth.Gaussian.Internal.polar_event {φ c R ψ : ℝ} (hφ : 0 ≤ φ) (hR : 0 < R) (hψ : |ψ| ≤ Real.pi) (h : |Real.cos φ * (R * Real.cos ψ) - c| ≤ Real.sin φ * |R * Real.sin ψ|) : |c| ≤ R ∧ ||ψ| - Real.arccos (c / R)| ≤ φ

At radius R > 0 and angle ψ ∈ [-π, π], the event |cos φ x - c| ≤ sin φ |y| forces |c| ≤ R and puts |ψ| within φ of arccos (c / R).

theorem Algebraic.Cutwidth.Gaussian.Internal.volume_polar_event_le {φ c R : ℝ} (hφ : 0 ≤ φ) (hR : 0 < R) : MeasureTheory.volume ({ψ : ℝ | |Real.cos φ * (R * Real.cos ψ) - c| ≤ Real.sin φ * |R * Real.sin ψ|} ∩ Set.Ioo (-Real.pi) Real.pi) ≤ (Set.Ici |c|).indicator (fun (x : ℝ) => ENNReal.ofReal (4 * φ)) R

At radius R > 0, the angles in (-π, π) of the event |cos φ x - c| ≤ sin φ |y| have total length at most 4φ, and there are none unless |c| ≤ R.

The radial tail

theorem Algebraic.Cutwidth.Gaussian.Internal.integral_Ioi_mul_exp_neg_half_sq (a : ℝ) : ∫ (R : ℝ) in Set.Ioi a, R * Real.exp (-2⁻¹ * R ^ 2) = Real.exp (-2⁻¹ * a ^ 2)

The radial tail ∫_{R > a} R exp (-R²/2) dR = exp (-a²/2).

theorem Algebraic.Cutwidth.Gaussian.Internal.lintegral_radial_Ici {a : ℝ} (ha : 0 ≤ a) : ∫⁻ (R : ℝ) in Set.Ici a, ENNReal.ofReal ((2 * Real.pi)⁻¹ * (R * Real.exp (-2⁻¹ * R ^ 2))) = ENNReal.ofReal ((2 * Real.pi)⁻¹ * Real.exp (-2⁻¹ * a ^ 2))

The radial factor of the planar Gaussian beyond radius a ≥ 0.

Decay of the planar angle law

theorem Algebraic.Cutwidth.Gaussian.Internal.prod_gaussianReal_cos_sin_le {φ : ℝ} (hφ : 0 ≤ φ) (c : ℝ) : ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)) {p : ℝ × ℝ | |Real.cos φ * p.1 - c| ≤ Real.sin φ * |p.2|} ≤ ENNReal.ofReal (2 / Real.pi * φ * Real.exp (-2⁻¹ * c ^ 2))

Decay of the planar angle law. For independent standard Gaussians and φ ≥ 0, the event |cos φ Z₁ - c| ≤ sin φ |Z₂| has probability at most (2/π) φ exp (-c²/2).

theorem Algebraic.Cutwidth.Gaussian.Internal.cos_sin_arctan_sqrt_div {s r : ℝ} (hs : 0 < s) (hr : 0 ≤ r) : Real.cos (Real.arctan (√r / √s)) = √s / √(s + r) ∧ Real.sin (Real.arctan (√r / √s)) = √r / √(s + r)

The angle arctan (√r / √s) has cosine √s / √(s + r) and sine √r / √(s + r).

theorem Algebraic.Cutwidth.Gaussian.Internal.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.Internal.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.

theorem Algebraic.Cutwidth.Gaussian.Internal.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 ρ / π.