OAI/NumberTheory/EgyptianFractions/GreedyBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.exists_logarithmic_greedy_budget line 10

   Source documentation

   A natural greedy step budget logarithmic in S, sufficient for a target unreduced denominator exp (D*S).

   theorem exists_logarithmic_greedy_budget (D S : ℝ)
       (hS : Real.exp 1 ≤ S) (hDS : D ≤ S * Real.log 2) :
       ∃ N : ℕ,
         ((N + 1 : ℕ) : ℝ) ≤ (2 / Real.log 2 + 2) * Real.log S ∧
         Real.exp (D * S) * (1 / 2 : ℝ) ^ (2 ^ N) ≤ 1 := by
   …

   Mentions: OAI.Problem337.D

2. theorem OAI.Problem337.eventually_logarithmic_greedy_budget line 55

   Source documentation

   The budget above is uniformly O(log(log b)) for polynomial target unreduced denominators, without choosing any numerical cutoff.

   theorem eventually_logarithmic_greedy_budget (D : ℝ) :
       ∃ b0 : ℕ, ∀ b : ℕ, b0 ≤ b →
         ∃ N : ℕ,
           ((N + 1 : ℕ) : ℝ) ≤
             (2 / Real.log 2 + 2) * Real.log (Real.log (b : ℝ)) ∧
           Real.exp (D * Real.log (b : ℝ)) * (1 / 2 : ℝ) ^ (2 ^ N) ≤ 1 := by
   …

   Mentions: OAI.Problem337.D