Threshold crossings of Gaussian forms: proofs

Under gaussPi ι, the vector toLp 2 ω has the standard Gaussian law on EuclideanSpace ℝ ι, and form a ω is the inner product with toLp 2 a. Hence form a has law gaussianReal 0 (∑ i, a i ^ 2), and two forms with orthogonal coefficients are jointly Gaussian and uncorrelated, so independent: their joint law is the product of the two marginals.

The crossing bound conditions on the second form. A real Gaussian density is at most 1 / √(2πv), so an interval of length 2|y| has probability at most 2|y| / √(2πv); the mean absolute value of gaussianReal 0 v is √(2v/π).

Real Gaussian estimates

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussianPDFReal_le_inv_sqrt (m : ℝ) (v : NNReal) (x : ℝ) : ProbabilityTheory.gaussianPDFReal m v x ≤ (√(2 * Real.pi * ↑v))⁻¹

The density of gaussianReal m v is at most its value at the mean.

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussianReal_le_mul_volume (m : ℝ) {v : NNReal} (hv : v ≠ 0) (S : Set ℝ) : (ProbabilityTheory.gaussianReal m v) S ≤ ENNReal.ofReal (√(2 * Real.pi * ↑v))⁻¹ * MeasureTheory.volume S

A nondegenerate real Gaussian gives each set at most the peak density times its Lebesgue measure.

theorem Algebraic.Cutwidth.Gaussian.Internal.integral_Ioi_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) : ∫ (x : ℝ) in Set.Ioi 0, x * Real.exp (-b * x ^ 2) = (2 * b)⁻¹

The half-line integral of x * exp (-b x²).

theorem Algebraic.Cutwidth.Gaussian.Internal.integral_abs_gaussianReal (v : NNReal) : ∫ (x : ℝ), |x| ∂ProbabilityTheory.gaussianReal 0 v = √(2 * ↑v / Real.pi)

The mean absolute value of a centered real Gaussian of variance v is √(2v/π).

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

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

theorem Algebraic.Cutwidth.Gaussian.Internal.crossing_const_eq {r s : ℝ} (hr : 0 ≤ r) (hs : 0 < s) : (√(2 * Real.pi * s))⁻¹ * (2 * √(2 * r / Real.pi)) = 2 / Real.pi * (√r / √s)

The constant in the crossing bound.

Laws of Gaussian forms

theorem Algebraic.Cutwidth.Gaussian.Internal.form_eq_inner {ι : Type} [Fintype ι] (a ω : ι → ℝ) : form a ω = ((innerSL ℝ) (WithLp.toLp 2 a)) (WithLp.toLp 2 ω)

A form is the inner product of the coefficient and sample vectors.

theorem Algebraic.Cutwidth.Gaussian.Internal.measurable_form {ι : Type} [Fintype ι] (a : ι → ℝ) : Measurable (form a)

theorem Algebraic.Cutwidth.Gaussian.Internal.map_innerSL_stdGaussian {ι : Type} [Fintype ι] (u : EuclideanSpace ℝ ι) : MeasureTheory.Measure.map (⇑((innerSL ℝ) u)) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)) = ProbabilityTheory.gaussianReal 0 (‖u‖ ^ 2).toNNReal

Under the standard Gaussian, the inner product with u has law gaussianReal 0 ‖u‖².

theorem Algebraic.Cutwidth.Gaussian.Internal.cov_innerSL_stdGaussian {ι : Type} [Fintype ι] (u v : EuclideanSpace ℝ ι) : ProbabilityTheory.covariance (⇑((innerSL ℝ) u)) (⇑((innerSL ℝ) v)) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)) = inner ℝ u v

Under the standard Gaussian, inner products have covariance ⟪u, v⟫.

theorem Algebraic.Cutwidth.Gaussian.Internal.map_pair_stdGaussian {ι : Type} [Fintype ι] (u v : EuclideanSpace ℝ ι) (huv : inner ℝ u v = 0) : MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ ι) => (((innerSL ℝ) u) x, ((innerSL ℝ) v) x)) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)) = (ProbabilityTheory.gaussianReal 0 (‖u‖ ^ 2).toNNReal).prod (ProbabilityTheory.gaussianReal 0 (‖v‖ ^ 2).toNNReal)

Inner products with orthogonal vectors are independent under the standard Gaussian, so their joint law is the product of their marginals.

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussPi_map_form {ι : Type} [Fintype ι] (a : ι → ℝ) : MeasureTheory.Measure.map (form a) (gaussPi ι) = ProbabilityTheory.gaussianReal 0 (∑ i : ι, a i ^ 2).toNNReal

The law of a Gaussian form.

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussPi_map_form_pair {ι : Type} [Fintype ι] (a b : ι → ℝ) (hab : ∑ i : ι, a i * b i = 0) : MeasureTheory.Measure.map (fun (ω : ι → ℝ) => (form a ω, form b ω)) (gaussPi ι) = (ProbabilityTheory.gaussianReal 0 (∑ i : ι, a i ^ 2).toNNReal).prod (ProbabilityTheory.gaussianReal 0 (∑ i : ι, b i ^ 2).toNNReal)

Two Gaussian forms with orthogonal coefficients are independent: their joint law is the product of their marginal laws.

The three bounds

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussPi_between_le {ι : 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 * (√(∑ i : ι, (β i - α i) ^ 2) / √(∑ i : ι, (α i + β i) ^ 2))

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussPi_window_le {ι : Type} [Fintype ι] (α : ι → ℝ) (hα : ∑ i : ι, α i ^ 2 = 1) (s : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) : (gaussPi ι).real {ω : ι → ℝ | s ≤ form α ω ∧ form α ω < s + δ} ≤ δ / √(2 * Real.pi)

theorem Algebraic.Cutwidth.Gaussian.Internal.gaussPi_tail_le {ι : Type} [Fintype ι] (α : ι → ℝ) (hα : ∑ i : ι, α i ^ 2 = 1) {T : ℝ} (hT : 0 < T) : (gaussPi ι).real {ω : ι → ℝ | T ≤ |form α ω|} ≤ 1 / T ^ 2