OAI/NumberTheory/Ostmann/Arithmetic/FrequencyBudgetRates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.cubic_log_budget line 13
2. theorem OAI.Ostmann.frequency_budget_subexponential line 37

   Source documentation

   One value of D controls every frequency divisor and every joint square modulus up to exp(2*C*m), with the total cost at most exp(epsilon*m).

   theorem frequency_budget_subexponential (C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
       ∀ᶠ m : ℝ in atTop, ∃ D : ℝ, 0 ≤ D ∧
         (∀ n : ℕ, n ≠ 0 → (n : ℝ) ≤ Real.exp (2 * C * m) →
           (n.divisors.card : ℝ) ≤ D) ∧
         (∀ N : ℕ, (N : ℝ) ≤ Real.exp (C * m) →
           8 * D ^ 4 * (1 + Real.log N) ^ 3 ≤ Real.exp (ε * m)) := by
   …