OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedReduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reduce the literal coefficient identity to its two nonvanishing ramified classes. The third class is zero by the proved ramified selection rule.

  1. theorem OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_lambda_cube_pow line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaCoefficientAgreement_lambda_cube_pow_iff line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_missing_class line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaCoefficientAgreement_missing_class line 48
  5. theorem OAI.CubicFirstMoment.cubicThetaCoefficientAgreement_ramified_reduction line 58