SequenceSubexponentialRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common vanishing rate for subexponential coordinate bounds

theorem OAI.PolycyclicRecognition.exists_sequence_subexponential_rate line 16

Source documentation

A subexponential upper bound can be expressed by one nonnegative vanishing exponential rate, including every initial scale.

theorem exists_sequence_subexponential_rate
    (scale R : ℕ → ℝ) (hs : ∀ n, 0 < scale n)
    (hR : HasSubexponentialUpperBoundSeq scale R) :
    ∃ ε : ℕ → ℝ, (∀ n, 0 ≤ ε n) ∧ Tendsto ε atTop (𝓝 0) ∧
      ∀ n, R n ≤ Real.exp (scale n * ε n) := by
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq