OAI/NumberTheory/CubicMoment/Theta/CubicThetaMobiusGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The literal hyperbolic three-space action used in DR v3, Section 5.1. The determinant calculation is kept explicit, before using the action to transport the cubic theta series.

  1. def OAI.CubicFirstMoment.cubicThetaMobiusDenominator line 13
  2. def OAI.CubicFirstMoment.cubicThetaMobiusNumerator line 16
  3. def OAI.CubicFirstMoment.cubicThetaMobius line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaMobius_det line 23
  5. lemma OAI.CubicFirstMoment.cubicThetaMobius_denominator_pos line 27
  6. lemma OAI.CubicFirstMoment.cubicThetaMobius_height_pos line 40
  7. lemma OAI.CubicFirstMoment.normSq_lagrange line 44
  8. lemma OAI.CubicFirstMoment.cubicThetaMobius_radius line 53