OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspRestriction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded restriction from the completed global energy space to the literal high cusp strip, extending all actual C1 finite-energy sections.

  1. lemma OAI.CubicFirstMoment.cubicThetaFiniteEnergyEmbedding_dense line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaFiniteCuspRestriction_energy_bound line 26
  3. def OAI.CubicFirstMoment.cubicThetaCuspRestriction line 33
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspRestriction_finiteEnergy line 38
  5. lemma OAI.CubicFirstMoment.cubicThetaCuspRestriction_norm line 44