OAI/NumberTheory/Ostmann/Characters/CharacterFourthMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A weighted fourth moment of multiplicative character sums

The full character sum selects equality of two nonzero products. Together with the split-quadratic collision count, this gives equation tree-fourth-moment of the manuscript.

  1. theorem OAI.Ostmann.mellin_field_dual_orthogonality line 21
  2. def OAI.Ostmann.weightedCharacterSum line 34
  3. theorem OAI.Ostmann.weightedCharacterSum_fourth_expansion line 38
  4. theorem OAI.Ostmann.weightedCharacterSum_fourth_character_sum line 73

    Source documentation

    Character orthogonality leaves exactly the nonzero product collisions.

    theorem weightedCharacterSum_fourth_character_sum {p : ℕ} [Fact p.Prime]
    (w : ZMod p → ℝ) (a : ZMod p) :
    (∑ χ : MulChar (ZMod p) ℂ, ‖weightedCharacterSum w χ a‖ ^ 4) =
      (Fintype.card (ZMod p)ˣ : ℝ) *
        ∑ b₁ : ZMod p, ∑ b₂ : ZMod p, ∑ b₃ : ZMod p, ∑ b₄ : ZMod p,
          if (a - b₁) * (a - b₂) = (a - b₃) * (a - b₄) ∧
              (a - b₁) * (a - b₂) ≠ 0 then w b₁ * w b₂ * w b₃ * w b₄ else 0 := by
…

    Mentions: OAI.Ostmann.weightedCharacterSum