OAI/NumberTheory/Jacobsthal/Conclusions/IteratedLogFinite.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogFinite.of_eventually line 12

   Source documentation

   Absorb the bounded range without changing any interval quantifier.

   theorem of_eventually
       (hlarge : ∃ C : ℝ, 0 < C ∧ ∀ᶠ k : ℕ in atTop,
         ∃ m : ℕ, Targets.IsJacobsthalBound k m ∧
           (m : ℝ) ≤ C * (k : ℝ) ^ 2 / (loglog k) ^ 2) :
       Targets.JacobsthalIteratedLog := by
   …

   Mentions: OAI.Erdos970.NumberTheoryLean.Targets.IsJacobsthalBound, OAI.Erdos970.NumberTheoryLean.Targets.JacobsthalIteratedLog