OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedMissingCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Agreement of the actual and prescribed coefficients in the first absent ramified class. The frequency index is exactly -lambda*h.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_ramified_two line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_lambda_missing line 30
  3. theorem OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_lambda_missing_eq line 36