MRTSmoothEuler.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The finite-prime smooth Euler product on Re(s)=1. Finite prime support makes the series absolutely convergent even on this line; the geometric local factors therefore give the actual analytic series to which the pretentious-distance estimate applies.

lemma OAI.TwoPointCorrelations.mrt_line_one_euler_term line 18
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothEuler.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_LSeries_term_pow line 30
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothEuler.lean:30 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_LSeries_term_coprime_mul line 43
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothEuler.lean:43 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_prime_euler_norm_lt_one line 53
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothEuler.lean:53 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_smooth_euler_product line 63

Source documentation

The actual smooth L-series is absolutely summable and equals its finite Euler product on the boundary line Re(s)=1.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothEuler.lean:63 (same declaration text).

theorem mrt_smooth_euler_product (F : ℕ → ℂ) (hF1 : F 1 = 1)
    (hF : ∀ m n, 0 < m → 0 < n → F (m * n) = F m * F n)
    (hFb : OneBounded F) (N : ℕ) (t : ℝ) :
    Summable (fun n : Nat.smoothNumbers (N + 1) =>
      ‖LSeries.term F (1 + (t : ℂ) * Complex.I) n‖) ∧
    HasSum (fun n : Nat.smoothNumbers (N + 1) =>
      LSeries.term F (1 + (t : ℂ) * Complex.I) n)
      (∏ p ∈ primesUpTo N, (1 - mrtPrimeEulerTerm F t p)⁻¹) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.primesUpTo, OAI.TwoPointCorrelations.mrtPrimeEulerTerm

theorem OAI.TwoPointCorrelations.mrt_smooth_euler_distance_bound line 100

Source documentation

The distance saving applies to the analytic smooth series itself, with the same finite prime-square error as its Euler product.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTSmoothEuler.lean:100 (same declaration text).

theorem mrt_smooth_euler_distance_bound (F : ℕ → ℂ) (hF1 : F 1 = 1)
    (hF : ∀ m n, 0 < m → 0 < n → F (m * n) = F m * F n)
    (hFb : OneBounded F) (N : ℕ) (t : ℝ) :
    ‖∑' n : Nat.smoothNumbers (N + 1), LSeries.term F (1 + (t : ℂ) * Complex.I) n‖ ≤
      Real.exp ((∑ p ∈ primesUpTo N, (1 : ℝ) / p) -
        squaredDistance F (mrtArchimedeanTwist t) N +
        ∑ p ∈ primesUpTo N, (1 : ℝ) / (p : ℝ) ^ 2) := by
…

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