RescalingSampleLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Subsequence limits of the sampled rescaling metrics

Uniformly bounded countable samples have a convergent distance matrix. Its triangle inequalities give an actual pseudometric, whose completion will supply the pointed limit after the finite-net estimates are applied.

theorem OAI.RegularPointCoordinates.exists_rescaling_sample_limit line 24

Source documentation

A countable family of rescaled sample distances has an actual pseudometric subsequential limit. Only upper bounds on the samples are required at this stage.

theorem exists_rescaling_sample_limit (r : ℕ → ℝ) (hr : ∀ i, 0 < r i)
    (points : ℕ → ι → X) (B : ι → ℝ)
    (hbound : ∀ k a b, dist (points k a) (points k b) / r k ≤ B a + B b) :
    ∃ phi : ℕ → ℕ, StrictMono phi ∧ ∃ d : PseudoMetricSpace ι,
      ∀ a b, Tendsto (fun k => dist (points (phi k) a) (points (phi k) b) / r (phi k))
        atTop (𝓝 (@dist ι d.toDist a b)) := by
…