OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootPairing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual Hermitian pairing on the finite arithmetic root cover. Both root translations and Weyl inversion preserve its integral.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeRootSectionPairing line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionPairing_apply line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionPairing_continuous line 33
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionPairing_smul line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootSectionPairing_translate line 49
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootSectionPairing_translation_integral line 58
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootSectionPairing_weyl_integral line 67