OAI/NumberTheory/TwoPointCorrelations/ModFiveCharacterSums.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Bounded character sums and the exact Abel integral for modulus five.

Periodicity and the vanishing sum over one period give an absolute bound four, independent of the character and of the cutoff. This is the first analytic estimate for the three nonprincipal L-functions.

  1. lemma OAI.TwoPointCorrelations.modFive_character_shift line 20

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:20 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_character_period_sum line 24

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:24 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_character_full_periods line 31

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:31 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFive_character_prefix_remainder line 41

    Source documentation

    A complete number of periods can be removed exactly.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:41 (same declaration text).

    lemma modFive_character_prefix_remainder (χ : DirichletCharacter ℂ 5)
    (hχ : χ ≠ 1) (N : ℕ) :
    (∑ n ∈ range N, χ (n : ZMod 5)) =
      ∑ n ∈ range (N % 5), χ (n : ZMod 5) := by
…
  5. theorem OAI.TwoPointCorrelations.modFive_character_prefix_norm line 49

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:49 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFive_character_Icc_eq line 59

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:59 (same declaration text).

  7. theorem OAI.TwoPointCorrelations.modFive_character_Icc_norm line 66

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:66 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.modFive_character_sum_bigO line 72

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:72 (same declaration text).

  9. theorem OAI.TwoPointCorrelations.modFive_LFunction_Abel line 80

    Source documentation

    The exact integral on the initial half-plane. Bounded partial sums will allow continuation of its right side to the larger half-plane re s > 0.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveCharacterSums.lean:80 (same declaration text).

    theorem modFive_LFunction_Abel (χ : DirichletCharacter ℂ 5) (hχ : χ ≠ 1)
    {s : ℂ} (hs : 1 < s.re) :
    DirichletCharacter.LFunction χ s =
      s * ∫ t in Set.Ioi (1 : ℝ),
        (∑ n ∈ Icc 1 ⌊t⌋₊, χ (n : ZMod 5)) * (t : ℂ) ^ (-(s + 1)) := by
…