Sheppard's bound for threshold crossings of correlated Gaussians

Let X be a standard Gaussian vector of a finite-dimensional real inner product space, and let u, v be vectors of equal norm at angle θ. When the common norm is positive, ⟪u, X⟫ and ⟪v, X⟫ are Gaussians of equal variance with correlation cos θ. Sheppard's bound (measureReal_stdGaussian_mem_uIoc_le_angle): a threshold t lies between ⟪u, X⟫ and ⟪v, X⟫ with probability at most θ / π. For vectors of positive norm the bound is attained at t = 0: that is Sheppard's formula [She99] for the probability that two correlated Gaussians differ in sign. For u = v = 0 the crossing event is empty while Mathlib's angle 0 0 is π / 2, so the bound is then strict. Only the bound is proved here.

The proof has four steps.

1. Change of variables. The vectors u + v and v - u are orthogonal, so U = ⟪u + v, X⟫ and V = ⟪v - u, X⟫ are independent centered Gaussians, and a crossing at t forces |U - 2 t| ≤ |V|.
2. Anderson's inequality on the line (ProbabilityTheory.gaussianReal_Icc_le). Conditioning on V, the shift 2 t only decreases the probability.
3. The planar angle law (gaussianReal_prod_setOf_abs_le_mul_abs). For independent standard Gaussians Z₁, Z₂, the event |Z₁| ≤ k |Z₂| constrains only the angle of (Z₁, Z₂) in polar coordinates, to two arcs of total length 4 arctan k, so it has probability (2 / π) arctan k. Rescaling, |U| ≤ |V| has probability (2 / π) arctan (‖v - u‖ / ‖u + v‖) (measureReal_stdGaussian_mem_uIoc_le_arctan).
4. The half-angle formula (InnerProductGeometry.angle_eq_two_mul_arctan). For vectors of equal norm at angle θ < π, the ratio ‖v - u‖ / ‖u + v‖ is tan (θ / 2).

The event that t lies between x and y, the lower one strictly below t, is t ∈ Set.uIoc x y.

Main results

• ProbabilityTheory.gaussianReal_prod_setOf_abs_le_mul_abs: the planar angle law.
• ProbabilityTheory.gaussianReal_prod_setOf_abs_le_mul_abs_of_ne_zero: the planar angle law for centered Gaussians of any variances.
• InnerProductGeometry.angle_eq_two_mul_arctan: the half-angle formula for vectors of equal norm.
• ProbabilityTheory.measureReal_stdGaussian_mem_uIoc_le_arctan, ProbabilityTheory.measureReal_stdGaussian_mem_uIoc_le_angle: Sheppard's bound.
• measurableSet_setOf_mem_uIoc: the event that a threshold lies between two measurable functions is measurable.

References

• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation

theorem measurableSet_setOf_mem_uIoc {Ω : Type u_1} [MeasurableSpace Ω] {f g : Ω → ℝ} (hf : Measurable f) (hg : Measurable g) (t : ℝ) : MeasurableSet {ω : Ω | t ∈ Set.uIoc (f ω) (g ω)}

The event that a threshold lies between two measurable real functions is measurable.

theorem InnerProductGeometry.angle_eq_two_mul_arctan {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {u v : V} (huv : ‖u‖ = ‖v‖) (hne : u + v ≠ 0) : angle u v = 2 * Real.arctan (‖v - u‖ / ‖u + v‖)

The half-angle formula. Two vectors of equal norm whose sum is nonzero make the angle 2 arctan (‖v - u‖ / ‖u + v‖).

The planar angle law

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

The planar angle law. For independent standard Gaussians Z₁ and Z₂, the event |Z₁| ≤ k |Z₂| has probability (2 / π) arctan k.

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

The planar angle law for any variances. For independent centered Gaussians X and Y of variances s ≠ 0 and r, the event |X| ≤ k |Y| has probability (2 / π) arctan (k √r / √s).

Sheppard's bound

theorem ProbabilityTheory.measureReal_stdGaussian_mem_uIoc_le_arctan {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u v : E} (huv : ‖u‖ = ‖v‖) (hne : u + v ≠ 0) (t : ℝ) : (stdGaussian E).real {x : E | t ∈ Set.uIoc (inner ℝ u x) (inner ℝ v x)} ≤ 2 / Real.pi * Real.arctan (‖v - u‖ / ‖u + v‖)

Sheppard's bound, arctan form. If u and v have equal norms and nonzero sum, a threshold lies between ⟪u, X⟫ and ⟪v, X⟫, for a standard Gaussian vector X, with probability at most (2 / π) arctan (‖v - u‖ / ‖u + v‖).

theorem ProbabilityTheory.measureReal_stdGaussian_mem_uIoc_le_angle {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u v : E} (huv : ‖u‖ = ‖v‖) (t : ℝ) : (stdGaussian E).real {x : E | t ∈ Set.uIoc (inner ℝ u x) (inner ℝ v x)} ≤ InnerProductGeometry.angle u v / Real.pi

Sheppard's bound. If u and v have equal norms, a threshold lies between ⟪u, X⟫ and ⟪v, X⟫, for a standard Gaussian vector X, with probability at most angle u v / π.