theorem RandomProjection.log2_lt_one_aux : Real.log 2 < 1

Numerical fact $\log 2 < 1$, used as a constant bound in the recentering arguments.

theorem RandomProjection.one_le_two_mul_exp_neg_aux {r : ℝ} (hr : r ≤ Real.log 2) : 1 ≤ 2 * Real.exp (-r)

For $r \le \log 2$, we have $1 \le 2 \exp(-r)$. Used to handle the trivial part of sub-Gaussian tail bounds when the threshold is small.

theorem RandomProjection.tail_recenter_toReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m : ℕ} (hm : 0 < m) {Y : Ω → ℝ} {med center : ℝ} (hmed : ∀ s ≥ 0, (μ {ω : Ω | |Y ω - med| ≥ s}).toReal ≤ 2 * Real.exp (-(↑m * s ^ 2) / 4)) : ∃ c > 0, ∀ t ≥ 0, (μ {ω : Ω | |Y ω - center| ≥ t}).toReal ≤ 2 * Real.exp (-c * ↑m * t ^ 2)

Recentering lemma in the toReal formulation: given a sub-Gaussian tail bound around the median, produce a sub-Gaussian tail bound around an arbitrary center center, with some positive constant $c$ depending on the gap and the dimension.

noncomputable def RandomProjection.normProj (m d : ℕ) (hd : d ≤ m) (z : EuclideanSpace ℝ (Fin m)) : ℝ

Norm of the projection of $z \in \mathbb{R}^m$ onto the first $d$ coordinates, $\| (z_1, \dots, z_d) \|_2$.

theorem RandomProjection.normProj_lipschitz {m d : ℕ} (hd : d ≤ m) (x y : EuclideanSpace ℝ (Fin m)) : |normProj m d hd x - normProj m d hd y| ≤ ‖x - y‖

The projection norm is $1$-Lipschitz: $|\,\|Px\| - \|Py\|\,| \le \|x - y\|$.

theorem RandomProjection.random_projection_concentration {m d : ℕ} (hd : d ≤ m) (hm : 0 < m) {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Z : Ω → EuclideanSpace ℝ (Fin m)} (hLevy : ∀ (f : EuclideanSpace ℝ (Fin m) → ℝ), (∀ (x y : EuclideanSpace ℝ (Fin m)), |f x - f y| ≤ ‖x - y‖) → ∃ (med : ℝ), ∀ s ≥ 0, (μ {ω : Ω | |f (Z ω) - med| ≥ s}).toReal ≤ 2 * Real.exp (-(↑m * s ^ 2) / 4)) : ∃ c > 0, ∀ t ≥ 0, (μ {ω : Ω | |normProj m d hd (Z ω) - √(↑d / ↑m)| ≥ t}).toReal ≤ 2 * Real.exp (-c * ↑m * t ^ 2)

Lemma 9.4.24 (random projection / Johnson-Lindenstrauss concentration). Under a Lévy sub-Gaussian concentration assumption for $1$-Lipschitz functions of a random $Z \in \mathbb{R}^m$, the projection norm $\|P_d Z\|$ concentrates around $\sqrt{d/m}$ with sub-Gaussian tails: $\mu(|\,\|P_d Z\| - \sqrt{d/m}\,| \ge t) \le 2 \exp(-c m t^2)$ for some $c > 0$.

theorem NearlyEquidistantPoints.exp_two_log_two : Real.exp (2 * Real.log 2) = 4

Identity $\exp(2 \log 2) = 4$.

theorem NearlyEquidistantPoints.exp_half_ge (e : ℝ) (he : e ≥ 2 * Real.log 2) : Real.exp e / 2 ≥ Real.exp (e / 2)

For $e \ge 2 \log 2$, we have $\exp(e)/2 \ge \exp(e/2)$.

theorem NearlyEquidistantPoints.floor_exp_ge_two_of_log2_le {e : ℝ} (he : Real.log 2 ≤ e) : 2 ≤ ⌊Real.exp e⌋₊

If $e \ge \log 2$, then $\lfloor \exp(e) \rfloor \ge 2$.

theorem NearlyEquidistantPoints.nearly_equidistant_points (hJL : ∃ C > 0, ∀ (ε : ℝ), 0 < ε → ∀ (m N d : ℕ) (X : Fin N → EuclideanSpace ℝ (Fin m)), ↑d > C * ε⁻¹ ^ 2 * Real.log ↑N → ∃ (f : Fin N → EuclideanSpace ℝ (Fin d)), ∀ (i j : Fin N), i ≠ j → (1 - ε) * dist (X i) (X j) ≤ dist (f i) (f j) ∧ dist (f i) (f j) ≤ (1 + ε) * dist (X i) (X j)) (hSimplex : ∀ (N : ℕ), 2 ≤ N → ∃ (X : Fin N → EuclideanSpace ℝ (Fin (N - 1))), ∀ (i j : Fin N), i ≠ j → dist (X i) (X j) = 1) : ∃ c > 0, ∀ (ε : ℝ), 0 < ε → ∀ (d : ℕ), 0 < d → ∃ (N : ℕ) (S : Fin N → EuclideanSpace ℝ (Fin d)), ↑N ≥ Real.exp (c * ε ^ 2 * ↑d) ∧ ∀ (i j : Fin N), i ≠ j → 1 - ε ≤ dist (S i) (S j) ∧ dist (S i) (S j) ≤ 1 + ε

Nearly-equidistant points in $\mathbb{R}^d$. Combining Johnson-Lindenstrauss with the standard simplex construction, one can embed exponentially many points $S_1, \dots, S_N$ in $\mathbb{R}^d$ with all pairwise distances in $[1 - \varepsilon, 1 + \varepsilon]$, where $N \ge \exp(c \varepsilon^2 d)$.