OAI/NumberTheory/JointDickman/Amplification/PolylogMultiplicativeSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.prime_log_bilinear_as_product line 10
2. lemma OAI.JointDickman.prime_log_coefficient_bound line 23
3. theorem OAI.JointDickman.prime_log_bilinear_polylog_bound line 29
4. theorem OAI.JointDickman.squarefree_rational_polylog_sum_bound line 46

   Source documentation

   A sufficient rational-frequency special case for the application. This is proved from the bilinear decomposition, rather than assumed as MV77.

   theorem squarefree_rational_polylog_sum_bound : ∃ C : ℝ, 0 < C ∧
       ∀ (f : ArithmeticFunction ℝ), f.IsMultiplicative → (∀ n, |f n| ≤ 1) →
       (∀ n, ¬Squarefree n → f n=0) → ∀ (N B q a : ℕ),
       2 ≤ B → B^20 ≤ N → 0 < q → a.Coprime q → Real.log N ≤ 3*(B:ℝ) →
       (B:ℝ)^12 ≤ q → (q:ℝ) ≤ N/(B:ℝ)^8 →
       ‖∑ n ∈ Ioc 0 N, (f n:ℂ)*additivePhase ((n:ℝ)*((a:ℝ)/q))‖ ≤
         C*N*(1+Real.log B)/Real.log N := by
   …

   Mentions: OAI.JointDickman.additivePhase