OAI/NumberTheory/CubicMoment/Theta/CubicThetaTypeILogCoefficients.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed logarithmic coefficient factors can be retained in the actual weight family. This is the form used by short logarithmic convolutions.

  1. theorem OAI.CubicFirstMoment.cubicTheta_typeI_low_log_coefficients line 13