OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeTraceL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite trace has finite mass. Each sheet is integrated using the actual hyperbolic measure and the constructed disjoint fundamental domain.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeSection_memLp_domain line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeSheet_memLp line 24
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceSection_memLp_domain line 37
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeTraceSection_memLp line 49