OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveCuspRestriction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded restriction to any positive-height period strip. Injectivity is replaced by the proved finite multiplicity below height two.

  1. abbrev OAI.CubicFirstMoment.CubicThetaPositiveStripL2 line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPositiveStrip_finite line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaFiniteEnergy_positiveStrip_memLp line 28
  4. def OAI.CubicFirstMoment.cubicThetaFinitePositiveCuspRestriction line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaFinitePositiveCuspRestriction_norm_sq line 48
  6. lemma OAI.CubicFirstMoment.cubicThetaFinitePositiveCuspRestriction_bound line 58
  7. def OAI.CubicFirstMoment.cubicThetaPositiveCuspRestriction line 88
  8. lemma OAI.CubicFirstMoment.cubicThetaPositiveCuspRestriction_finiteEnergy line 95