OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveSquareSource.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The square-class source identity holds for every positive cutoff, including the lower profiles reached by repeated Hecke action.

  1. theorem OAI.CubicFirstMoment.cubicThetaPositiveSquareSource line 13