OAI/NumberTheory/CubicMoment/Theta/CubicThetaTwistFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite Fourier inversion for the periodic numerator twists in the cubic theta formula. The trace pairing is perfect for primary moduli.

  1. def OAI.CubicFirstMoment.cubicThetaResidueChar line 13

    Source documentation

    The source trace character, without the inverse-different factor. For primary q the removed factor is a unit modulo q.

    def cubicThetaResidueChar (q : Eisenstein) (hq : q ≠ 0) : AddChar (Residues q) ℂ :=
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues

  2. lemma OAI.CubicFirstMoment.cubicThetaResidueChar_mk line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaResidueChar_primitive line 27
  4. def OAI.CubicFirstMoment.cubicThetaTwistTransform line 43

    Source documentation

    Finite numerator Fourier transform in the exact trace normalization.

    def cubicThetaTwistTransform (q : Eisenstein) (hq : q ≠ 0)
    [Fintype (Residues q)] (ψ : Residues q → ℂ) (u : Residues q) : ℂ :=
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues

  5. lemma OAI.CubicFirstMoment.cubicThetaTwist_fourier_sum line 47
  6. theorem OAI.CubicFirstMoment.cubicThetaTwist_fourier_inversion line 82

    Source documentation

    Fourier inversion for an arbitrary periodic coefficient twist.

    theorem cubicThetaTwist_fourier_inversion {q : Eisenstein} (hq : primary q)
    [Fintype (Residues q)] (ψ : Residues q → ℂ) (y : Residues q) :
    ψ y = (norm q:ℂ)⁻¹*∑ u : Residues q,
      cubicThetaTwistTransform q (primary_ne_zero hq) ψ u*
        cubicThetaResidueChar q (primary_ne_zero hq) (-u*y) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaTwistTransform, OAI.CubicFirstMoment.primary_ne_zero, OAI.CubicFirstMoment.cubicThetaResidueChar