OAI/GroupTheory/PolycyclicRecognition/Algebra/LogPolynomialBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.log_two_add_polynomial_le line 13

   Source documentation

   A fixed polynomial growth factor contributes at most a fixed multiple of log (2 + r), including the degree-zero case.

   theorem log_two_add_polynomial_le {A r : ℝ} (hA : 0 ≤ A) (hr : 0 ≤ r) (b : ℕ) :
       Real.log (2 + A * (1 + r) ^ b) ≤
         ((b : ℝ) + Real.log (2 + A) / Real.log 2) * Real.log (2 + r) := by
   …