RescaledMetricSmallness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Vanishing normalized coordinates give sublinear metric displacement

theorem OAI.PolycyclicRecognition.repr_shift_exponentialRescaleBasis line 19
Source documentation
Shifting the logarithmic scale changes each coordinate by one fixed factor. This identity does not require the costs to be positive.
```
theorem repr_shift_exponentialRescaleBasis
    (b : Basis J ℝ L) (cost : J → ℝ) (r a : ℝ) (x : L) (j : J) :
    (exponentialRescaleBasis b cost (r + a)).repr x j =
      Real.exp (-a * cost j) * (exponentialRescaleBasis b cost r).repr x j := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.norm_shift_exponentialRescaleBasis_le line 30

Source documentation

All coordinates obey one common bound for a fixed shift.

theorem norm_shift_exponentialRescaleBasis_le [Fintype J]
    (b : Basis J ℝ L) (cost : J → ℝ) (r a : ℝ) (x : L) :
    ‖(exponentialRescaleBasis b cost (r + a)).equivFun x‖ ≤
      (∑ j, Real.exp (-a * cost j)) * ‖(exponentialRescaleBasis b cost r).equivFun x‖ := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.metric_sublinear_of_rescaled_coordinates_tendsto_zero line 49

Source documentation

A unit-chart metric estimate at every large scale implies that every sequence with normalized coordinates tending to zero has sublinear length. The proof uses a fixed smaller scale before passing to the limit.

theorem metric_sublinear_of_rescaled_coordinates_tendsto_zero
    {G ι : Type*} [Group G] [PseudoMetricSpace G] [Fintype J]
    (b : Basis J ℝ L) (cost : J → ℝ) (Exp : L → G)
    {C : ℝ} (_hC : 0 ≤ C)
    (hmetric : ∀ s : ℝ, 0 ≤ s → ∀ x : L,
      ‖(exponentialRescaleBasis b cost s).equivFun x‖ ≤ 1 →
        dist 1 (Exp x) ≤ C * Real.exp s)
    {l : Filter ι} (scale : ι → ℝ) (hscale : Tendsto scale l atTop)
    (x : ι → L)
    (hsmall : Tendsto (fun i => (exponentialRescaleBasis b cost (scale i)).equivFun (x i))
      l (𝓝 0)) :
    Tendsto (fun i => dist 1 (Exp (x i)) / Real.exp (scale i)) l (𝓝 0) := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis