OAI/NumberTheory/CubicMoment/Theta/CubicThetaObservationScaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The geometric normalization of the actual Whittaker observation under multiplication of its arithmetic frequency.

  1. lemma OAI.CubicFirstMoment.cubicThetaPoleWeight_mul line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPoleWeight_cube_mul line 21
  3. def OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient line 28
  4. theorem OAI.CubicFirstMoment.cubicThetaNormalizedArithmeticResidue_observation line 32