OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedCoefficientNormalization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The other-cusp Whittaker coefficients have the explicit arithmetic normalization, with the same actual scalar as the original cusp.

  1. lemma OAI.CubicFirstMoment.cubicThetaShiftedFrequency_lambda line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedPoleWeight line 21
  3. def OAI.CubicFirstMoment.cubicThetaShiftedNormalizedCoefficient line 51
  4. theorem OAI.CubicFirstMoment.cubicThetaShiftedNormalizedCoefficient_explicit line 56