OAI/NumberTheory/Ostmann/ZeroDensity/PrincipalFourthMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing the principal character from the fourth moment

Its contribution cancels the leading fourth power of the total mass. This leaves the second-moment term required by the two-bad quartet case.

  1. theorem OAI.Ostmann.weightedCharacterSum_principal line 21
  2. theorem OAI.Ostmann.fourth_tangent line 35
  3. theorem OAI.Ostmann.principal_fourth_moment_lower line 39
  4. theorem OAI.Ostmann.nonprincipal_fourth_moment_bound line 53

    Source documentation

    The leading J⁴ cancels after removing the principal character.

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

    Mentions: OAI.Ostmann.weightedCharacterSum