Gaussian rotation invariance: the projection ↔ chi-squared link

This file closes the substantive gap between the abstract chi-squared concentration of JL.NormPreservation and the actual Gaussian random projection jlMap of JL.Projection.

The key probabilistic fact is Gaussian rotation invariance: if the entries of the matrix A : Matrix (Fin k) (Fin n) ℝ are i.i.d. N(0,1), then for a fixed unit vector u (∑ⱼ uⱼ² = 1) the k row–vector products Aᵢ · u are themselves i.i.d. N(0,1). Concretely, the i.i.d. Gaussian matrix measure pushes forward under A ↦ A.mulVec u to gaussianVec k:

(gaussianMatrix k n).map (fun A i ↦ ∑ⱼ Aᵢⱼ uⱼ) = gaussianVec k.

The single-coordinate version (map_dotProduct_gaussianReal) is proven through mathlib's multivariate-Gaussian machinery (ProbabilityTheory.stdGaussian, its invariance and dual variance lemmas); the k-fold independence is assembled with Measure.pi_map_pi.

Combining this with the deterministic identity ‖jlMap A x‖² = (1/k)·∑ᵢ(Aᵢ·x)² (jlMap_sq_norm) transports jl_norm_preservation to a genuine concentration bound on the projected squared norm ∑ᵢ (jlMap A w i)² of any fixed w ≠ 0 (jlMap_concentration).

Single-coordinate rotation invariance

theorem JL.map_dotProduct_gaussianReal {n : ℕ} (u : Fin n → ℝ) (hu : ∑ j : Fin n, u j ^ 2 = 1) : MeasureTheory.Measure.map (fun (row : Fin n → ℝ) => ∑ j : Fin n, row j * u j) (gaussianVec n) = ProbabilityTheory.gaussianReal 0 1

Single-coordinate Gaussian rotation invariance. For a unit vector u (∑ⱼ uⱼ² = 1), the linear form row ↦ ∑ⱼ rowⱼ · uⱼ pushes the i.i.d. standard Gaussian product measure forward to the standard normal N(0,1).

The i.i.d. Gaussian matrix and the multi-row link

noncomputable def JL.gaussianMatrix (k n : ℕ) : MeasureTheory.Measure (Fin k → Fin n → ℝ)

The i.i.d. N(0,1) matrix measure on Fin k → Fin n → ℝ: every entry is an independent standard Gaussian.

Equations

• JL.gaussianMatrix k n = MeasureTheory.Measure.pi fun (x : Fin k) => JL.gaussianVec n

instance JL.instIsProbabilityMeasureForallFinForallRealGaussianMatrix (k n : ℕ) : MeasureTheory.IsProbabilityMeasure (gaussianMatrix k n)

theorem JL.gaussianMatrix_map_dotProduct {k n : ℕ} (u : Fin n → ℝ) (hu : ∑ j : Fin n, u j ^ 2 = 1) : MeasureTheory.Measure.map (fun (A : Fin k → Fin n → ℝ) (i : Fin k) => ∑ j : Fin n, A i j * u j) (gaussianMatrix k n) = gaussianVec k

Projection ↔ chi-squared link. For a unit vector u, the i.i.d. Gaussian matrix pushes forward under A ↦ A.mulVec u to gaussianVec k: the k row–vector products are i.i.d. N(0,1).

Projection-level norm-preservation

theorem JL.jlMap_concentration {k n : ℕ} (hk : 0 < k) (w : Fin n → ℝ) (hw : ∑ j : Fin n, w j ^ 2 ≠ 0) {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1) : (gaussianMatrix k n).real {A : Fin k → Fin n → ℝ | ε * ∑ j : Fin n, w j ^ 2 ≤ |∑ i : Fin k, jlMap k n A w i ^ 2 - ∑ j : Fin n, w j ^ 2|} ≤ 2 * Real.exp (-(ε ^ 2 - ε ^ 3) * ↑k / 4)

Distributional norm preservation of the Gaussian projection. For any fixed nonzero vector w, the squared norm ∑ᵢ (jlMap A w i)² of its Gaussian projection deviates from ‖w‖² = ∑ⱼ wⱼ² by a relative factor ε with probability at most 2·exp(-(ε² - ε³) k / 4). This is jl_norm_preservation transported to the real projection via Gaussian rotation invariance.