MellinPrimeSamplingArithmetic.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Prime sampling with the divisor errors discharged

theorem OAI.JointDickman.mellin_prime_sampling_arithmetic line 12

Source documentation

Sparse-prime sampling with explicit divisor-sum error bounds.

theorem mellin_prime_sampling_arithmetic (B : ℝ) (hB : 1 ≤ B) :
    ∃ C A δ V : ℝ, 0 < C ∧ 0 < A ∧ 0 < δ ∧ δ ≤ 1 ∧
      ∀ (q Z : ℕ) (P Q : Finset ℕ) (N : ℝ) (S : Finset ℝ),
      16 ≤ q → 2 ≤ Z → Z ≤ q → V ≤ (q:ℝ)^9 →
      (q:ℝ)^10 ≤ N → N ≤ (q:ℝ)^11 →
      (∀ p ∈ P, p.Prime ∧ p ≤ Z) →
      (∀ p ∈ Q, p.Prime ∧ Z < p ∧ N ≤ (p:ℝ) ∧ (p:ℝ) ≤ 2*N) →
      (∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|) →
      (∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ (q:ℝ)^B) →
      ∀ a : ℕ → ℂ,
      (∑ t ∈ S, ‖mrtExponentialPolynomial Q a (fun n => -Real.log (n:ℝ)) t‖^2) ≤
        8*(32*C*N*(∏ p ∈ P, (1-1/(p:ℝ))) + (Z+1:ℕ)*
…