OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalCharacterOrthogonality.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality of the literal trace characters on the half-open three-Eisenstein cell, including its unnormalized volume.

  1. lemma OAI.CubicFirstMoment.cubicThetaHorizontalCharacter_add_index line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaHorizontalCharacter_inner line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaHorizontalCharacter_nontrivial line 30
  4. theorem OAI.CubicFirstMoment.cubicThetaHorizontalFourier_character_zero line 49