OAI/NumberTheory/EgyptianFractions/MainLowerVerified.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.main_double_log_lower_bound line 12

   Source documentation

   The elementary lower half of the main order theorem, with an explicit absolute constant, independent of the short-expansion upper construction.

   theorem main_double_log_lower_bound (b : ℕ) (hb : 2 ≤ b) :
       (1 / 2 : ℝ) * Real.log (Real.log (b : ℝ)) ≤ (maxEgyptianLength b : ℝ) := by
   …

   Mentions: OAI.Problem337.maxEgyptianLength