OAI/NumberTheory/TotientAsymptotic/SmoothCofactorTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TotientAsymptotic.smooth_cofactor_rankin line 11

   Source documentation

   The exponential tail needed for the actual smooth-cofactor truncation.

   theorem smooth_cofactor_rankin {N : ℕ} (hN : 2 ≤ N) (Z : ℝ) (Q : Finset ℕ)
       (hQ : ∀ n ∈ Q, 0 < n ∧ largestPrimeFactor n ≤ N ∧ Z < Real.log n) :
       (∑ n ∈ Q, (n.totient : ℝ)⁻¹) ≤
         Real.exp (-Z/(4*Real.log N))*(primeEulerProduct N)^4 := by
   …

   Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.primeEulerProduct