OAI/NumberTheory/Ostmann/Characters/SquarefreeCoefficientBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_reciprocal_exponential_cutoff line 13
2. theorem OAI.Ostmann.squarefree_coefficient_budget line 51

   Source documentation

   The exponent 1/10^6 is the paper's moment scale; the denominator budget is measured against T^(1-10^-7), the scale of K.

   theorem squarefree_coefficient_budget (C ε : ℝ) (hε : 0 < ε) :
       ∀ᶠ T : ℝ in atTop, ∀ (N : ℕ) (S : Finset ℕ) (u : ℝ),
         (N : ℝ) ≤ Real.exp (C * T) →
         (∀ s ∈ S, Squarefree s ∧ s ≤ N) →
         0 ≤ u → u ≤ 4 * T ^ (1 / 1000000 : ℝ) →
         (∑ s ∈ S, u ^ s.primeFactors.card / (s : ℝ)) ≤
           Real.exp (ε * T ^ (9999999 / 10000000 : ℝ)) := by
   …