OAI/NumberTheory/JointDickman/Counting/HyperbolaBlockBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.prime_subset_log_sum_le line 10
2. lemma OAI.JointDickman.rounded_hyperbola_norm_le line 23
3. theorem OAI.JointDickman.prime_hyperbola_block_bound line 52

   Source documentation

   A block with arbitrary integer upper endpoints is controlled by H rectangles and a rounding error of width floor(U/H)+1.

   theorem prime_hyperbola_block_bound : ∃ C : ℝ, 0 < C ∧
       ∀ (P : Finset ℕ) (M : ℕ → ℕ) (b c : ℕ → ℂ) (Z U H Q q a : ℕ),
       0 < H → 2 ≤ Q → 0 < q → a.Coprime q →
       (∀ p ∈ P, p.Prime ∧ p ≤ Q) → (∀ p ∈ P, Z ≤ M p ∧ M p ≤ U) →
       (∀ p ∈ P, ‖b p‖ ≤ Real.log p) → (∀ m, ‖c m‖ ≤ 1) →
       ‖∑ p ∈ P, ∑ m ∈ Ioc Z (M p), b p*c m*additivePhase ((a:ℝ)/q*p*m)‖ ≤
         ((U/H+1:ℕ):ℝ)*Real.log 4*Q + (H:ℝ)*Real.sqrt
           (C*((Q:ℝ)*Real.log Q*(U:ℝ)^2 + Q*(U:ℝ)^2*Q*(1+Real.log q)/q +
             Q*U*Q + Q*U*q*(1+Real.log Q))) := by
   …

   Mentions: OAI.JointDickman.additivePhase