OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveUnfold.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Positive unfolding on the actual quotient. Integrability follows from an integrable periodization, so the seed need not have compact support.
- lemma
OAI.CubicFirstMoment.cubicThetaPositive_unfoldline 11