OAI/NumberTheory/Ostmann/Characters/CharacterFourthBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted character fourth-moment bound

Equation tree-fourth-moment follows from character orthogonality and counting coincidences of two monic split quadratics.

  1. theorem OAI.Ostmann.weightedCharacterSum_fourth_bound line 20

    Source documentation

    The fourth-moment bound, with the manuscript's normalization.

    theorem weightedCharacterSum_fourth_bound {p : ℕ} [Fact p.Prime]
    (w : ZMod p → ℝ) (hw : ∀ b, 0 ≤ w b) :
    (∑ χ : MulChar (ZMod p) ℂ, ∑ a : ZMod p, ‖weightedCharacterSum w χ a‖ ^ 4) /
      (Fintype.card (ZMod p)ˣ : ℝ) ≤
        2 * (p : ℝ) * (∑ b : ZMod p, w b ^ 2) ^ 2 + (∑ b : ZMod p, w b) ^ 4 := by
…

    Mentions: OAI.Ostmann.weightedCharacterSum