OAI/NumberTheory/JointDickman/Probability/ResidueFourierParseval.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact unit-residue Parseval identity for the fine histograms

  1. theorem OAI.JointDickman.stdAddChar_conj line 12
  2. theorem OAI.JointDickman.unitResidue_fourier_pair line 16
  3. def OAI.JointDickman.unitResidueFourier line 37
  4. theorem OAI.JointDickman.unitResidue_fourier_parseval line 41
  5. theorem OAI.JointDickman.normalizedUnitResidue_fourier_parseval line 69

    Source documentation

    Dividing the transform by phi gives the manuscript's probability normalization.

    theorem normalizedUnitResidue_fourier_parseval {q : ℕ} [NeZero q]
    (v : (ZMod q)ˣ → ℂ) :
    (∑ h : ZMod q, ‖unitResidueFourier v h/(q.totient : ℂ)‖^2) =
      ((q : ℝ)/(q.totient : ℝ))*((1/(q.totient : ℝ))*∑ r : (ZMod q)ˣ, ‖v r‖^2) := by
…

    Mentions: OAI.JointDickman.unitResidueFourier