OAI/NumberTheory/CubicMoment/Theta/CubicThetaPoincareUnfolding.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact unfolding against compact periodized seeds, using the actual measurable arithmetic fundamental domain and absolute integrability.

  1. lemma OAI.CubicFirstMoment.cubicThetaFundamental_translates_summable line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaFundamental_integral_tsum line 26
  3. theorem OAI.CubicFirstMoment.cubicThetaPoincare_pairing_integral line 39