OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceLogMetric.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.metric_bound_of_sequence_exponential_coordinates line 14

   Source documentation

   A subexponential logarithmic radius contributes an arbitrarily small linear error; the fixed exponential rate remains explicit.

   theorem metric_bound_of_sequence_exponential_coordinates
       {V G : Type*} [PseudoMetricSpace G] [One G]
       (Exp : V → G) (size : V → ℝ) (hsize : ∀ v, 0 ≤ size v)
       {D : ℝ} (hD : 0 ≤ D)
       (hmetric : ∀ v, dist 1 (Exp v) ≤ D * Real.log (2 + size v))
       (scale R : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (hscale0 : ∀ n, 0 ≤ scale n) (hR0 : ∀ n, 0 ≤ R n)
       (hR : HasSubexponentialUpperBoundSeq scale R) :
       ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop, ∀ δ : ℝ, 0 ≤ δ → ∀ v : V,
         size v ≤ R n * Real.exp (δ * scale n) →
         dist 1 (Exp v) ≤ D * (δ + ε) * scale n := by
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq