OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedPrimaryResidue.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The signed-primary selection rule holds for the actual residue and matches the prescribed coefficient on the same arithmetic frequency.

  1. theorem OAI.CubicFirstMoment.cubicThetaFrequencyContinuation_primary_support_germ line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_primary_support line 28
  3. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_signed_primary_support line 42
  4. theorem OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_primary_support_eq line 86