OAI/NumberTheory/EgyptianFractions/CountingTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.loglog_lower_of_two_pow_two_pow line 9

   Source documentation

   Taking two logarithms of a natural doubly exponential lower bound.

   theorem loglog_lower_of_two_pow_two_pow {t N : ℕ} (hN : 2 ^ (2 ^ t) ≤ N) :
       (t : ℝ) * Real.log 2 + Real.log (Real.log 2) ≤ Real.log (Real.log (N : ℝ)) := by
   …

2. theorem OAI.Problem337.counting_lower_transfer line 22

   Source documentation

   A supply of exponential counts at logarithmically short lengths transfers by padding monotonicity to a linear double-log lower bound at every long length.

   theorem counting_lower_transfer (f : ℕ → ℕ) {B : ℝ} (hB : 0 < B)
       (hmono : ∀ i j : ℕ, 2 ≤ i → i ≤ j → f i ≤ f j)
       (hsupply : ∀ᶠ r : ℕ in atTop, ∃ ell : ℕ, 2 ≤ ell ∧
         (ell : ℝ) ≤ B * Real.log (r : ℝ) ∧ 2 ^ (r - 1) ≤ f ell) :
       ∀ᶠ k : ℕ in atTop,
         (1 / (2 * B)) * (k : ℝ) ≤ Real.log (Real.log (f k : ℝ)) := by
   …