MellinPrimeSampling.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sparse prime sampling from concrete divisor-sum discrepancies

The constant is unconditional: it comes from the proved upper sieve. Only the explicitly displayed finite logarithmic kernels remain to be estimated in applications.

theorem OAI.JointDickman.mellin_prime_sampling line 17

Source documentation

A separated sample set gains the prime density, provided its actual smooth divisor sums have the stated error.

theorem mellin_prime_sampling : ∃ C : ℝ, 0 < C ∧
    ∀ (K Z : ℕ) (P Q : Finset ℕ) (N : ℝ) (S : Finset ℝ) (δ : ℝ),
      2 ≤ Z → 0 < N → 0 ≤ δ →
      (∀ p ∈ P, p.Prime ∧ p ≤ Z) →
      Q ⊆ Icc 1 K → (∀ q ∈ Q, q.Prime ∧ Z < q) →
      (∀ q ∈ Q, N ≤ (q : ℝ) ∧ (q : ℝ) ≤ 2*N) →
      (∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|) →
      (∀ D ∈ P.powerset.filter (fun D => (∏ p ∈ D, p) ≤ Z),
        ∀ t ∈ S, ∀ u ∈ S,
          ‖mellinSieveDiscreteKernel K (∏ p ∈ D, p) N (t-u) -
            mellinSieveMainKernel N (t-u)/((∏ p ∈ D, p : ℕ) : ℂ)‖ ≤ δ) →
      ∀ a : ℕ → ℂ,
…

Mentions: OAI.JointDickman.mellinSieveDiscreteKernel, OAI.JointDickman.mellinSieveMainKernel