PrimitiveResidueFourier.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The perfect codifferent pairing on every Eisenstein residue ring. Unlike the trace pairing without the different, this includes ramified moduli.

lemma OAI.CubicFirstMoment.fourierChar_eq_one_integer line 13
lemma OAI.CubicFirstMoment.residue_trace_dual_lattice line 29
Source documentation
The integral dual of the trace lattice is the inverse different.
```
lemma residue_trace_dual_lattice (z : ℂ)
    (h : ∀ n : Eisenstein, ∃ k : ℤ,
      tracePair (n : ℂ) (z / traceLambda) = k) :
    ∃ a : Eisenstein, (a : ℂ) = z := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.tracePair, OAI.CubicFirstMoment.traceLambda
def OAI.CubicFirstMoment.residueFourierChar line 57
Source documentation
Canonical primitive additive character modulo any nonzero Eisenstein integer.
```
def residueFourierChar (q : Eisenstein) (hq : q ≠ 0) : AddChar (Residues q) ℂ where
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues
lemma OAI.CubicFirstMoment.residueFourierChar_mk line 78
lemma OAI.CubicFirstMoment.residueFourierChar_isPrimitive line 83
def OAI.CubicFirstMoment.residueCharacterFourier line 112
Source documentation
The finite Fourier transform of the actual residue multiplicative character.
```
def residueCharacterFourier (q : Eisenstein) (hq : q ≠ 0)
    [Fintype (Residues q)] (χ : MulChar (Residues q) ℂ) (a : Residues q) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues
lemma OAI.CubicFirstMoment.residueCharacterFourier_unit line 117
Source documentation
Unit frequencies satisfy the exact Gauss eigenrelation for every modulus.
```
lemma residueCharacterFourier_unit (q : Eisenstein) (hq : q ≠ 0)
    [Fintype (Residues q)] (χ : MulChar (Residues q) ℂ) (a : (Residues q)ˣ) :
    residueCharacterFourier q hq χ a =
      (star χ) a * gaussSum χ (residueFourierChar q hq) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.residueCharacterFourier, OAI.CubicFirstMoment.residueFourierChar