OAI/NumberTheory/Ostmann/Characters/RatioParseval.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Parseval in the ratio of two nonzero arguments with fixed difference

  1. def OAI.Ostmann.ratioTest line 14
  2. def OAI.Ostmann.ratioDifferenceTransform line 18
  3. theorem OAI.Ostmann.ratioTest_sum line 22
  4. theorem OAI.Ostmann.ratioDifferenceTransform_eq_mellin line 41
  5. theorem OAI.Ostmann.ratioDifferenceTransform_parseval line 76

    Source documentation

    The sum over all quotient characters costs no small-correlation hypothesis.

    theorem ratioDifferenceTransform_parseval {p : ℕ} [Fact p.Prime]
    (F : ZMod p → ℂ) (y : (ZMod p)ˣ) (h0 : F 0 = 0) (hy : F y = 0) :
    (∑ ν : MulChar (ZMod p) ℂ, ‖ratioDifferenceTransform F y ν‖ ^ 2) =
      (Fintype.card (ZMod p)ˣ : ℝ) / (p : ℝ) ^ 2 * ∑ d : ZMod p, ‖F d‖ ^ 2 := by
…

    Mentions: OAI.Ostmann.ratioDifferenceTransform