OAI/NumberTheory/EgyptianFractions/CountingUpper.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.counting_loglog_upper_of_box line 10

   Source documentation

   The elementary box estimate already gives a linear upper bound on the double logarithm, including the zero and singleton cases.

   theorem counting_loglog_upper_of_box (f : ℕ → ℕ)
       (hbox : ∀ k : ℕ, f k ≤ k ^ (2 ^ k - 1))
       (k : ℕ) (hk : 2 ≤ k) :
       Real.log (Real.log (f k : ℝ)) ≤ 3 * (k : ℝ) := by
   …