OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteCusps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite cusp cover can be made disjoint without changing its union at any height. Representatives are selected from the given arithmetic charts, so all preceding analytic estimates continue to apply.

  1. lemma OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_one_nonempty line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaFiniteCusps_disjoint line 20