Sheppard's crossing bound: proofs

• Planar angle law. In polar coordinates (r, θ) the product of two standard Gaussians has density exp (-r²/2) / (2π), and for r > 0 the event |x| ≤ k |y| depends on θ alone: it holds on the two arcs of (-π, π) of half-width arctan k centered at ±π/2. The radial factor r exp (-r²/2) integrates to one, so the event has probability 4 arctan k / (2π).
• Anderson's inequality on the line. For a centered Gaussian, [c - w, c + w] has at most the mass of [-w, w]. By symmetry take c ≥ 0; the intervals share [c - w, w], and translation by 2w carries [-w, c - w] onto [w, c + w] without increasing the density.
• Sheppard's bound. The forms U = form (α + β) and V = form (β - α) are independent centered Gaussians, and a crossing forces |U - 2t| ≤ |V|. Conditioning on V, Anderson's inequality removes the shift 2t. Rescaling U and V to standard Gaussians turns |U| ≤ |V| into the planar angle event with k = ‖β - α‖ / ‖α + β‖.
• Half-angle identity. y = tanHalf x has cos (2 arctan y) = (1 - y²) / (1 + y²) = x and 0 ≤ 2 arctan y < π, so 2 arctan y = arccos x.

The planar angle law

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussianPDFReal_mul_polar (r θ : ℝ) : ProbabilityTheory.gaussianPDFReal 0 1 (r * Real.cos θ) * ProbabilityTheory.gaussianPDFReal 0 1 (r * Real.sin θ) = (2 * Real.pi)⁻¹ * Real.exp (-2⁻¹ * r ^ 2)

The standard planar Gaussian density in polar coordinates.

theorem Algebraic.Cutwidth.Gaussian.Internal.abs_cos_le_mul_abs_sin_iff {k : ℝ} (hk : 0 ≤ k) (θ : ℝ) : |Real.cos θ| ≤ k * |Real.sin θ| ↔ |Real.cos θ| ≤ Real.sin (Real.arctan k)

The angles with |cos θ| ≤ k |sin θ| are those with |cos θ| ≤ sin (arctan k).

theorem Algebraic.Cutwidth.Gaussian.Internal.angle_set_eq {k : ℝ} (hk : 0 ≤ k) : {θ : ℝ | |Real.cos θ| ≤ k * |Real.sin θ|} ∩ Set.Ioo (-Real.pi) Real.pi = Set.Icc (Real.pi / 2 - Real.arctan k) (Real.pi / 2 + Real.arctan k) ∪ Set.Icc (-(Real.pi / 2 + Real.arctan k)) (-(Real.pi / 2 - Real.arctan k))

The angles in (-π, π) with |cos θ| ≤ k |sin θ| form two arcs centered at ±π/2.

theorem Algebraic.Cutwidth.Gaussian.Internal.volume_angle_set {k : ℝ} (hk : 0 ≤ k) : MeasureTheory.volume ({θ : ℝ | |Real.cos θ| ≤ k * |Real.sin θ|} ∩ Set.Ioo (-Real.pi) Real.pi) = ENNReal.ofReal (4 * Real.arctan k)

The angles in (-π, π) with |cos θ| ≤ k |sin θ| have total length 4 arctan k.

theorem Algebraic.Cutwidth.Gaussian.Internal.lintegral_radial : ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal ((2 * Real.pi)⁻¹ * (r * Real.exp (-2⁻¹ * r ^ 2))) = ENNReal.ofReal (2 * Real.pi)⁻¹

The radial factor of the planar Gaussian integrates to one.

theorem Algebraic.Cutwidth.Gaussian.Internal.prod_gaussianReal_abs_le (k : ℝ) (hk : 0 ≤ k) : ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)) {p : ℝ × ℝ | |p.1| ≤ k * |p.2|} = ENNReal.ofReal (2 / Real.pi * Real.arctan k)

Planar angle law for the product of two standard Gaussians.

theorem Algebraic.Cutwidth.Gaussian.Internal.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 gaussPi (Fin 2).

Symmetric intervals carry the most mass

theorem Algebraic.Cutwidth.Gaussian.Internal.intervalIntegral_shift_le {f : ℝ → ℝ} (hf : Continuous f) {c w : ℝ} (hc : 0 ≤ c) (hmono : ∀ (x : ℝ), -w ≤ x → f (x + 2 * w) ≤ f x) : ∫ (x : ℝ) in c - w..c + w, f x ≤ ∫ (x : ℝ) in -w..w, f x

If translating by 2w does not increase f to the right of -w, then the interval of radius w around c ≥ 0 carries at most the mass of the centered one.

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussianPDFReal_neg (v : NNReal) (x : ℝ) : ProbabilityTheory.gaussianPDFReal 0 v (-x) = ProbabilityTheory.gaussianPDFReal 0 v x

The centered Gaussian density is even.

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussianPDFReal_add_two_mul_le (v : NNReal) {w x : ℝ} (hw : 0 ≤ w) (hx : -w ≤ x) : ProbabilityTheory.gaussianPDFReal 0 v (x + 2 * w) ≤ ProbabilityTheory.gaussianPDFReal 0 v x

The centered Gaussian density decreases under the translation by 2w to the right of -w.

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

One-dimensional Anderson inequality. For a centered Gaussian, an interval of radius w carries the most mass when it is centered at the mean.

theorem Algebraic.Cutwidth.Gaussian.Internal.prod_gaussianReal_sub_le (s r : NNReal) (c : ℝ) : ((ProbabilityTheory.gaussianReal 0 s).prod (ProbabilityTheory.gaussianReal 0 r)) {p : ℝ × ℝ | |p.1 - c| ≤ |p.2|} ≤ ((ProbabilityTheory.gaussianReal 0 s).prod (ProbabilityTheory.gaussianReal 0 r)) {p : ℝ × ℝ | |p.1| ≤ |p.2|}

Anderson's inequality for the event |X - c| ≤ |Y| with X, Y independent and X centered Gaussian.

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussianReal_map_sqrt_mul (s : NNReal) : MeasureTheory.Measure.map (fun (x : ℝ) => √↑s * x) (ProbabilityTheory.gaussianReal 0 1) = ProbabilityTheory.gaussianReal 0 s

gaussianReal 0 s is the image of the standard Gaussian under x ↦ √s x.

theorem Algebraic.Cutwidth.Gaussian.Internal.prod_gaussianReal_abs_le_abs (s r : NNReal) (hs : s ≠ 0) : ((ProbabilityTheory.gaussianReal 0 s).prod (ProbabilityTheory.gaussianReal 0 r)) {p : ℝ × ℝ | |p.1| ≤ |p.2|} = ENNReal.ofReal (2 / Real.pi * Real.arctan (√↑r / √↑s))

Planar angle law for two independent centered Gaussians of variances s > 0 and r.

Sheppard's bound

theorem Algebraic.Cutwidth.Gaussian.Internal.abs_add_sub_two_mul_le_of_between {t x y : ℝ} (h : Between t x y) : |x + y - 2 * t| ≤ |y - x|

A threshold separating two values lies within half their gap of their midpoint.

theorem Algebraic.Cutwidth.Gaussian.Internal.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 coefficient vectors of equal norm with nonzero sum.

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

2 arctan (tanHalf x) = arccos x.

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