ModFiveLFunctions.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The three analytic functions needed for the fixed modulus-five input.

Every nonprincipal character modulo five is determined here by its value at two, which is one of -1, I, or -I. Its L-function is an explicit finite linear combination of the existing Hurwitz zeta functions. The final identity identifies the corresponding Mangoldt Dirichlet series with the negative logarithmic derivative on the half-plane of absolute convergence. No quantitative zero-free estimate is assumed or asserted.

lemma OAI.TwoPointCorrelations.sum_zmod_five line 23
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:22 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_character_four line 32
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_character_three line 37
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:36 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_character_fourth_pow line 42
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:41 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_character_sum_values line 46
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:45 (same declaration text).
lemma OAI.TwoPointCorrelations.modFive_nonprincipal_at_two line 53
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:52 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_nonprincipal_parameter line 61
Source documentation
The nonprincipal characters require only these three possible values.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:60 (same declaration text).
```
theorem modFive_nonprincipal_parameter (χ : DirichletCharacter ℂ 5) (hχ : χ ≠ 1) :
    χ (2 : ZMod 5) = -1 ∨ χ (2 : ZMod 5) = Complex.I ∨
      χ (2 : ZMod 5) = -Complex.I := by
…
```
def OAI.TwoPointCorrelations.modFiveHurwitzCombination line 76
Source documentation
An explicit analytic function for each of the three parameters.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:75 (same declaration text).
```
noncomputable def modFiveHurwitzCombination (z s : ℂ) : ℂ :=
…
```
theorem OAI.TwoPointCorrelations.modFive_LFunction_eq line 83
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:82 (same declaration text).
def OAI.TwoPointCorrelations.modFiveMangoldtTwist line 92
Source documentation
The Dirichlet-series coefficients whose partial sums are required.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:91 (same declaration text).
```
noncomputable def modFiveMangoldtTwist (χ : DirichletCharacter ℂ 5) (n : ℕ) : ℂ :=
…
```
lemma OAI.TwoPointCorrelations.modFiveTwistedPsi_eq line 95
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:94 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_twisted_LSeries_eq line 101
Source documentation
Identification with existing analytic functions on re s > 1.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:100 (same declaration text).
```
theorem modFive_twisted_LSeries_eq (χ : DirichletCharacter ℂ 5) {s : ℂ}
    (hs : 1 < s.re) :
    LSeries (modFiveMangoldtTwist χ) s =
      -deriv (modFiveHurwitzCombination (χ (2 : ZMod 5))) s /
        modFiveHurwitzCombination (χ (2 : ZMod 5)) s := by
…
```
Mentions: OAI.TwoPointCorrelations.modFiveMangoldtTwist, OAI.TwoPointCorrelations.modFiveHurwitzCombination
theorem OAI.TwoPointCorrelations.modFive_nonprincipal_differentiable line 112
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:111 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_nonprincipal_nonzero line 120
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLFunctions.lean:119 (same declaration text).