Metric geometry

Geometry of general metric spaces: curvature bounds via comparison, length spaces, isometric embeddings and low-distortion embeddings.

TheoremJohnson–Lindenstrauss lemma#✓fully proved

There is a constant \(C > 0\) with the following property. Let \(\varepsilon > 0\), let \(m\) and \(N \ge 2\) be natural numbers, let \(X\) be a set of exactly \(N\) points of \(\mathbb{R}^m\) with the Euclidean norm, and let \(d\) be a natural number with \(d > C \varepsilon^{-2} \log N\). Then there is a map \(f : \mathbb{R}^m \to \mathbb{R}^d\) such that \((1 - \varepsilon) \|x - y\| \le \|f(x) - f(y)\| \le (1 + \varepsilon) \|x - y\|\) for all \(x, y \in X\), where \(\mathbb{R}^d\) also carries the Euclidean norm.

The map \(f\) is not required to be linear, and \(\varepsilon \ge 1\) is allowed (there the zero map works). The proof takes \(C = 64\) and uses a Gaussian random projection with a union bound over pairs of points.

theorem johnson_lindenstrauss :
    ∃ C : ℝ, 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‖
Sources
  • W. B. Johnson and J. Lindenstrauss, "Extensions of Lipschitz mappings into a Hilbert space," Contemporary Mathematics 26, Conference on Modern Analysis and Probability, American Mathematical Society (1984), 189--206, DOI 10.1090/conm/026/737400. ATLAS source-to-API map, item N147; ATLAS adds the hypothesis that N is at least 2.
Uses 2
Proof usesExponential moments of the square of a standard normal · Moment generating function of the square of a standard normal

TheoremMicroscopic weighting is not equivalent to finite concentration#●ready to prove

It is not true that every nonempty finite metric space \(X\) has a microscopic weighting if and only if it has finite concentration. Here, for real \(t\), \(Z_t\) is the \(X \times X\) matrix with entries \(e^{-t\,d(x,y)}\) and \(w_t = Z_t^{-1}\mathbf{1}\) is its weighting, where \(\mathbf{1}\) is the all-ones vector and the inverse of a singular matrix is taken to be \(0\). The space \(X\) has a microscopic weighting if \(w_t\) converges to some \(w \colon X \to \mathbb{R}\) as \(t \to 0^+\). It has finite concentration if there are \(g \colon X \to \mathbb{R}\) with \(\sum_{x \in X} g(x) = 1\) and \(c \in \mathbb{R}\) such that \(\sum_{y \in X} d(x,y)\,g(y) = c\) for every \(x \in X\).

Kenta Kitamura (assisted by ChatGPT) gave an explicit 10-point metric space with finite concentration but no microscopic weighting.

public theorem_wanted microscopicWeightingIff_refuted : ¬ microscopicWeightingIff
Sources
  • Kenta Kitamura, microscopic-weighting-counterexample, Lean formalization of the 10-point counterexample, https://github.com/KitaKen1/microscopic-weighting-counterexample/blob/eff8979/lean/MicroscopicWeightingCounterexampleFC.lean#L886-L894.

TheoremNo compact set is congruent to a proper subset of itself#●ready to prove

Let \(K\) be a compact subset of a metric space \(X\). Then there is no map \(f : X \to X\) with \(d(f(x), f(y)) = d(x, y)\) for all \(x, y \in X\) such that \(f(K) \subseteq K\) and \(f(K) \neq K\).

The underlying fact is that an isometric embedding of a compact metric space into itself is surjective.

theorem_wanted noCompactSetCongruentToProperSubset :
    ∀ (α : Type) [MetricSpace α] {K : Set α}, IsCompact K →
      ¬ ∃ (f : α → α), (∀ x y, dist (f x) (f y) = dist x y) ∧ f '' K ⊆ K ∧ f '' K ≠ K
Sources
  • S. Banach and S. Ulam, Problem 3 of the Scottish Book, stated and proved in the Scottish Book typescript.
1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.