OAI/NumberTheory/JointDickman/Arithmetic/RoughCountPrefix.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.halaszPowerPhase_eq_conj_twist line 12
2. theorem OAI.JointDickman.rough_count_prefix_away_zero line 20

   Source documentation

   Cancellation is uniform outside one fixed bounded neighborhood of zero. The coefficients may vary with the cutoff, subject to literal small-prime power agreement.

   theorem rough_count_prefix_away_zero {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1)
       {ε : ℝ} (hε : 0 < ε) : ∃ T : ℝ, 0 < T ∧
       ∀ᶠ N : ℕ in atTop, ∀ (f : ArithmeticFunction ℂ) (P : Finset ℕ),
         f.IsMultiplicative → (∀ n, ‖f n‖ ≤ 1) →
         (∀ p k : ℕ, p.Prime → (p:ℝ) ≤ (N:ℝ)^c → p^k ≤ N → f (p^k) = 1) →
         (∀ p ∈ P, p.Prime ∧ (N:ℝ)^c < (p:ℝ) ∧ (p:ℝ) ≤ N) →
         ∀ t : ℝ, T ≤ |t| → |t| ≤ 4*(Real.log N)^8 →
         ‖∑ n ∈ Icc 1 N, (f n*halaszPowerPhase t n)/
           ((finitePrimeDivisorCount P n:ℂ)+1)‖/(N:ℝ) ≤ ε := by
   …