OAI/NumberTheory/CubicMoment/Theta/CubicThetaPoincareLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A seed in one covering sheet periodizes to the corresponding invariant cutoff of the original section, including its cubic multiplier.

  1. lemma OAI.CubicFirstMoment.cubicThetaPoincare_localization_eq line 12