theorem jl_probabilistic_existence : ∃ c > 0, ∀ (m d : ℕ), 1 ≤ d → ∀ ε > 0, ε ≤ 1 → ∀ N ≥ 2, ↑N ^ 2 * (2 * Real.exp (-c * ε ^ 2 * ↑d)) < 1 → ∀ (X : Finset (EuclideanSpace ℝ (Fin m))), X.card = N → ∃ (f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin d)), ∀ x ∈ X, ∀ y ∈ X, (1 - ε) * ‖x - y‖ ≤ ‖f x - f y‖ ∧ ‖f x - f y‖ ≤ (1 + ε) * ‖x - y‖

Probabilistic core of the Johnson–Lindenstrauss lemma. There exists $c > 0$ such that whenever the union-bound quantity $N^{2}\,(2\,e^{-c\varepsilon^{2}d})$ is strictly less than $1$, any $N$-point subset $X \subseteq \mathbb{R}^m$ admits a map $f : \mathbb{R}^m \to \mathbb{R}^d$ that preserves all pairwise distances up to a factor of $1 \pm \varepsilon$.

theorem jl_map_existence : ∃ C > 0, ∀ ε > 0, ε ≤ 1 → ∀ (m d : ℕ), 1 ≤ d → ∀ N ≥ 2, ↑d > C * ε⁻¹ ^ 2 * Real.log ↑N → ∀ (X : Finset (EuclideanSpace ℝ (Fin m))), X.card = N → ∃ (f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin d)), ∀ x ∈ X, ∀ y ∈ X, (1 - ε) * ‖x - y‖ ≤ ‖f x - f y‖ ∧ ‖f x - f y‖ ≤ (1 + ε) * ‖x - y‖

Johnson–Lindenstrauss map existence (intermediate form). There exists a constant $C > 0$ such that for any $\varepsilon \in (0, 1]$, dimension $d$ with $d > C\varepsilon^{-2}\log N$, and any $N$-point set $X \subseteq \mathbb{R}^m$, there is a map $f : \mathbb{R}^m \to \mathbb{R}^d$ with $(1 - \varepsilon)\|x - y\| \le \|f(x) - f(y)\| \le (1 + \varepsilon)\|x - y\|$ for all $x, y \in X$.

theorem JohnsonLindenstrauss.johnson_lindenstrauss : ∃ C > 0, ∀ ε > 0, ∀ (m N : ℕ), N ≥ 2 → ∀ (X : Finset (EuclideanSpace ℝ (Fin m))), X.card = N → ∀ (d : ℕ), ↑d > C * ε⁻¹ ^ 2 * Real.log ↑N → ∃ (f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin d)), ∀ x ∈ X, ∀ y ∈ X, (1 - ε) * ‖x - y‖ ≤ ‖f x - f y‖ ∧ ‖f x - f y‖ ≤ (1 + ε) * ‖x - y‖

Johnson–Lindenstrauss lemma (Theorem 9.4.22, Johnson–Lindenstrauss 1982). There exists a constant $C > 0$ such that for every $\varepsilon > 0$, every finite set $X \subseteq \mathbb{R}^m$ of size $N \ge 2$, and every target dimension $d > C\varepsilon^{-2}\log N$, there is a map $f : \mathbb{R}^m \to \mathbb{R}^d$ preserving all pairwise distances within a factor of $1 \pm \varepsilon$.