The end-to-end Gaussian Johnson–Lindenstrauss theorem

This file assembles the complete Johnson–Lindenstrauss statement for an arbitrary finite point set in a Euclidean space, with the target dimension k explicitly bounded (not merely assumed via an abstract counting hypothesis):

For any m points p : Fin m → EuclideanSpace ℝ (Fin d) and any 0 < ε < 1, if the projection dimension satisfies 4 · log (2 m²) < (ε² − ε³) · k, then there EXISTS a Gaussian random projection matrix A : Fin k → Fin d → ℝ such that every pairwise squared distance is preserved within a relative factor 1 ± ε.

The proof combines:

• jlMap_concentration (JL.Rotation): the per-vector concentration bound for the real Gaussian projection, obtained through Gaussian rotation invariance;
• card_condition: the elementary derivation that the dimension bound on k discharges the union-bound counting condition m² · C < 1 with C = 2·exp(-(ε²−ε³)k/4);
• johnson_lindenstrauss (JL.Lemma): the abstract probabilistic-method union bound, which is kept as a standalone lemma.

theorem JL.card_condition {m k : ℕ} {ε : ℝ} (hdim : 4 * Real.log (2 * ↑m ^ 2) < (ε ^ 2 - ε ^ 3) * ↑k) : ↑m ^ 2 * (2 * Real.exp (-(ε ^ 2 - ε ^ 3) * ↑k / 4)) < 1

Dimension bound discharges the counting condition. If 4·log(2 m²) < (ε²−ε³)·k, then the union-bound condition m²·C < 1 holds for the JL failure probability C = 2·exp(-(ε²−ε³)k/4).

theorem JL.johnson_lindenstrauss_pointset {m d k : ℕ} (hk : 0 < k) (p : Fin m → EuclideanSpace ℝ (Fin d)) {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1) (hp : ∀ (a b : Fin m), a ≠ b → p a ≠ p b) (hdim : 4 * Real.log (2 * ↑m ^ 2) < (ε ^ 2 - ε ^ 3) * ↑k) : ∃ (A : Fin k → Fin d → ℝ), ∀ (a b : Fin m), a ≠ b → |∑ i : Fin k, jlMap k d A (fun (j : Fin d) => (p a - p b).ofLp j) i ^ 2 - ‖p a - p b‖ ^ 2| < ε * ‖p a - p b‖ ^ 2

Johnson–Lindenstrauss (end-to-end Gaussian form). For an arbitrary set of m distinct points in EuclideanSpace ℝ (Fin d), any 0 < ε < 1, and any target dimension k with 4·log(2 m²) < (ε²−ε³)·k, there exists a Gaussian projection matrix A : Fin k → Fin d → ℝ whose induced map jlMap k d A preserves all pairwise squared distances to within a factor 1 ± ε.