OAI/NumberTheory/TwoPointCorrelations/HalaszSmoothSeries.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The smooth Euler series used in the triple-convolution Perron formula. The finite prime factors and the smooth factor are absolutely convergent on the line Re(s)=1.

  1. def OAI.TwoPointCorrelations.halaszSmoothFunction line 16

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:16 (same declaration text).

  2. def OAI.TwoPointCorrelations.halaszFiniteCoefficient line 19

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:19 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_smooth_term line 22

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:22 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_smooth_LSeries line 28

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:28 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_smooth_LSeries_summable line 34

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:34 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_smooth_function_eq line 50

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:50 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.halasz_finite_term line 54

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:54 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.halasz_finite_LSeries_summable line 59

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:59 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.halasz_finite_LSeries line 65

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:65 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.halasz_smooth_triple_perron line 73

    Source documentation

    Triangular Perron inversion of the genuine prime-prime-smooth convolution on Re(s)=1.

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszSmoothSeries.lean:73 (same declaration text).

    theorem halasz_smooth_triple_perron (f : ℕ → ℂ) (hf1 : f 1 = 1)
    (hf : ∀ m n, 0 < m → 0 < n → f (m * n) = f m * f n)
    (hbound : OneBounded f) (N : ℕ) (P Q : Finset ℕ) (a b : ℕ → ℂ)
    {x : ℝ} (hx : 0 < x) (hxnat : ∀ n : ℕ, x ≠ (n : ℝ)) :
    (∑ n ∈ Icc 1 ⌊x⌋₊,
      ((halaszFiniteCoefficient P a) ⍟
        ((halaszFiniteCoefficient Q b) ⍟ (halaszSmoothFunction f N))) n *
          ((1 - (n : ℝ) / x : ℝ) : ℂ)) =
      VerticalIntegral' (fun s =>
        (∑ p ∈ P, LSeries.term a s p) * (∑ q ∈ Q, LSeries.term b s q) *
          LSeries (halaszSmoothFunction f N) s * modFivePerronKernel x s) 1 := by
…

    Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszFiniteCoefficient, OAI.TwoPointCorrelations.halaszSmoothFunction, OAI.TwoPointCorrelations.modFivePerronKernel