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.

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