OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialEnvelopes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.log_shift_div_tendsto_zero line 12
2. theorem OAI.PolycyclicRecognition.exists_polynomial_exp_envelope line 29

   Source documentation

   One nonnegative error function tending to zero absorbs a fixed polynomial at every sufficiently large scale. This allows the same error to be used simultaneously for all sampled chart positions.

   theorem exists_polynomial_exp_envelope {A : ℝ} (hA : 0 ≤ A) (p : ℕ) :
       ∃ ε : ℝ → ℝ, (∀ r, 0 ≤ ε r) ∧ Tendsto ε atTop (𝓝 0) ∧
         ∀ r : ℝ, 1 ≤ r → A * (1 + r) ^ p ≤ Real.exp (r * ε r) := by
   …