MRTSmoothDistance.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Mertens turns the exact smooth Euler product into the usual log N * exp(-distance) estimate, uniformly in the bounded coefficient.

lemma OAI.TwoPointCorrelations.mrt_sievePrimesUpTo_nat line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothDistance.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_prime_inverse_square_sum line 20
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothDistance.lean:20 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_smooth_distance_bound line 33

Source documentation

The absolute Euler-product constant is independent of the coefficient, height and smooth cutoff.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothDistance.lean:33 (same declaration text).

theorem mrt_smooth_distance_bound : ∃ C : ℝ, 0 < C ∧
    ∀ (F : ℕ → ℂ), F 1 = 1 →
      (∀ m n, 0 < m → 0 < n → F (m * n) = F m * F n) → OneBounded F →
      ∀ (N : ℕ), 2 ≤ N → ∀ t : ℝ,
      ‖∑' n : Nat.smoothNumbers (N + 1), LSeries.term F (1 + (t : ℂ) * Complex.I) n‖ ≤
        C * Real.log N * Real.exp (-squaredDistance F (mrtArchimedeanTwist t) N) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist