OAI/NumberTheory/CubicMoment/Theta/CubicThetaMobiusGenerators.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Translation and level inversion matrices in the exact coordinates used by the cubic theta Fourier and Mellin expansions.

  1. def OAI.CubicFirstMoment.cubicThetaTranslationMatrix line 11
  2. def OAI.CubicFirstMoment.cubicThetaInversionMatrix line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaMobius_translation line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaInversionMatrix_denominator line 23
  5. theorem OAI.CubicFirstMoment.cubicThetaMobius_inversion line 29