OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeComplexIntegration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Complex integration on the actual cubed-prime cover and the integrability of Hermitian products of square-integrable sections.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeComplexSheetIntegral line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaSquareIntegrablePair line 37
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeComplexSheet_integrable line 49