The Johnson–Lindenstrauss embedding-existence theorem

The distributional norm-preservation bound (JL.NormPreservation) controls the distortion of a single fixed vector. The JL lemma upgrades this to a single realization of the random projection that simultaneously preserves all pairwise distances of a finite point set, via the probabilistic method: a union bound over the < n² pairs shows the total failure probability is < 1, so a good realization exists.

exists_avoiding is the abstract probabilistic-method core; johnson_lindenstrauss specializes it to pairwise-distance preservation. The per-pair concentration hypothesis hpair is exactly the norm-preservation bound applied to each difference vector Q a - Q b (Gaussian rotation invariance turns each into the chi-squared law), and hcard is the union-bound counting condition implied by k ≥ ⌈8 · log n / (ε² − ε³)⌉.

theorem JL.exists_avoiding {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} (s : Finset ι) (B : ι → Set Ω) (hsum : ∑ i ∈ s, μ.real (B i) < 1) : ∃ (ω : Ω), ∀ i ∈ s, ω ∉ B i

Probabilistic method / union bound. In a probability space, if the total measure of a finite family of "bad" events is < 1, then some point avoids all of them.

theorem JL.johnson_lindenstrauss {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {ε C : ℝ} (r : Fin n → Fin n → Ω → ℝ) (D : Fin n → Fin n → ℝ) (hpair : ∀ (a b : Fin n), a ≠ b → μ.real {ω : Ω | ε * D a b ≤ |r a b ω - D a b|} ≤ C) (hC : 0 ≤ C) (hcard : ↑n ^ 2 * C < 1) : ∃ (ω : Ω), ∀ (a b : Fin n), a ≠ b → |r a b ω - D a b| < ε * D a b

Johnson–Lindenstrauss (existence form). Given target squared distances D a b and the realized squared projected distances r a b ω, if every pair's distortion exceeds ε · D a b with probability at most C, and the union-bound condition n² · C < 1 holds, then there is a single realization ω that preserves all pairwise (squared) distances within a factor 1 ± ε.