OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspDisjointness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Above height one, two arithmetic cusp neighborhoods are either identical at every height or disjoint. This removes duplicate cusp charts before summing the sharp exterior energy inequality.

  1. lemma OAI.CubicFirstMoment.cubicThetaPointHeight_upper line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_mem_iff line 24
  3. lemma OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_parabolic_eq line 34
  4. theorem OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_overlap line 59
  5. theorem OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_eq_or_disjoint line 81