OAI/NumberTheory/CubicMoment/Theta/CubicThetaIncomingForcing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The incoming height term gives an entire family of compact annular forcing terms. This is the scalar term to be assembled in the arithmetic cusps before applying the continued global resolvent.

  1. def OAI.CubicFirstMoment.cubicThetaIncomingForcing line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaCutoffIncoming_equation line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaIncomingForcing_zero line 33
  4. lemma OAI.CubicFirstMoment.cubicThetaIncomingForcing_compact line 38
  5. lemma OAI.CubicFirstMoment.cubicThetaIncomingForcing_analytic line 46