MixedResidueCharacters.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual mixed cubic residue characters and their finite Fourier transform.

lemma OAI.CubicFirstMoment.mixedCubic_congr line 14
lemma OAI.CubicFirstMoment.mixedCubic_eq_zero_of_nonunit line 18
def OAI.CubicFirstMoment.mixedResidueChar line 28
Source documentation
This character is defined at composite conductors, rather than supplied as an abstract character agreeing with the desired cubic symbol.
```
def mixedResidueChar (a b : Eisenstein) (ha : primary a) (hb : primary b) :
    MulChar (Residues (a*b)) ℂ where
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues
lemma OAI.CubicFirstMoment.mixedResidueChar_mk line 47
lemma OAI.CubicFirstMoment.huxleyPhase_eq_fourierChar line 52
theorem OAI.CubicFirstMoment.mixedResidueChar_fourier line 70
Source documentation
The raw Gauss transform has exactly the conductor square-root factor. This identity holds also at nonunit frequencies (where the right side vanishes).
```
theorem mixedResidueChar_fourier {a b : Eisenstein} (ha : primary a) (hb : primary b)
    (hsa : Squarefree a) (hsb : Squarefree b) (hab : IsCoprime a b)
    [Fintype (Residues (a*b))] (n : Eisenstein) :
    (∑ x : Residues (a*b), mixedResidueChar a b ha hb x *
      huxleyPhase (a*b) (residueRepresentative (a*b) x) n) =
      ((Real.sqrt (norm (a*b)):ℂ)*(gauss a*star (gauss b)) /
        mixedCubic a b 3) * star (mixedCubic a b n) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.mixedResidueChar, OAI.CubicFirstMoment.huxleyPhase, OAI.CubicFirstMoment.residueRepresentative, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.mixedCubic