OAI/NumberTheory/EgyptianFractions/MainLowerAppend.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.MainLower.denominator_le_of_sum line 12

   Source documentation

   Appending the remainder denominator and sorting reduces the lower-bound argument to a coordinate bound for possibly repeated unit fractions.

   theorem denominator_le_of_sum
       (hbound : ∀ s : ℕ, ∀ d : Fin s → ℕ,
         (∀ i, 1 ≤ d i) → Monotone d →
         (∑ i : Fin s, (1 : ℚ) / (d i : ℚ)) = 1 →
         ∀ i : Fin s, d i ≤ s ^ (2 ^ i.val))
       {b k : ℕ} (hb : 2 ≤ b) (n : Fin k → ℕ)
       (hn : ∀ i, 1 ≤ n i)
       (hsum : (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) =
         ((b - 1 : ℕ) : ℚ) / (b : ℚ)) :
       b ≤ (k + 1) ^ (2 ^ k) := by
   …

2. theorem OAI.Problem337.MainLower.log_log_le_twice line 55

   Source documentation

   A convenient absolute constant for the elementary lower bound.

   theorem log_log_le_twice {b k : ℕ} (hb : 2 ≤ b)
       (hbk : b ≤ (k + 1) ^ (2 ^ k)) :
       Real.log (Real.log (b : ℝ)) ≤ 2 * (k : ℝ) := by
   …