OAI/NumberTheory/TwoPointCorrelations/ModFiveAbelContinuation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Continue the bounded-partial-sum Abel integral to re s > 0.

The Mellin differentiation theorem gives holomorphy without differentiating an improperly convergent Dirichlet series. The identity principle then identifies it with the existing entire Dirichlet L-function. In particular each of the three modulus-five functions has a uniform linear growth bound on re s ≥ 1/2.

  1. def OAI.TwoPointCorrelations.modFiveAbelInput line 22

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:22 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFiveAbelInput_measurable line 25

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:25 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFiveAbelInput_norm line 29

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:29 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFiveAbelInput_locallyIntegrable line 37

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:37 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.modFiveAbelInput_bigO_atTop line 43

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:43 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFiveAbelInput_bigO_zero line 48

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:48 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFiveAbelIntegral_eq_mellin line 56

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:56 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.modFiveAbelIntegral_differentiableAt line 73

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:73 (same declaration text).

  9. theorem OAI.TwoPointCorrelations.modFiveAbelIntegral_eq_LFunction_of_pos line 90

    Source documentation

    The bounded-partial-sum integral is the existing L-function on the entire half-plane of convergence of that integral.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:90 (same declaration text).

    theorem modFiveAbelIntegral_eq_LFunction_of_pos (χ : DirichletCharacter ℂ 5)
    (hχ : χ ≠ 1) {s : ℂ} (hs : 0 < s.re) :
    modFiveAbelIntegral χ s = DirichletCharacter.LFunction χ s := by
…

    Mentions: OAI.TwoPointCorrelations.modFiveAbelIntegral

  10. theorem OAI.TwoPointCorrelations.modFive_LFunction_norm_le line 109

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:109 (same declaration text).

  11. theorem OAI.TwoPointCorrelations.modFive_LFunction_norm_halfPlane line 115

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveAbelContinuation.lean:115 (same declaration text).