OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimaryObservedCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized Whittaker coefficients agree with the explicit primary theta family up to its single base coefficient.

  1. def OAI.CubicFirstMoment.cubicThetaObservedBaseFactor line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_weighted line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_one line 29
  4. theorem OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_primary line 34