OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialForm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The closed energy space of one Dirichlet cusp mode, constructed from compactly supported test functions. No differential inverse is assumed.

  1. def OAI.CubicFirstMoment.cubicThetaRadialTests line 15
  2. abbrev OAI.CubicFirstMoment.CubicThetaRadialJet line 25
  3. abbrev OAI.CubicFirstMoment.CubicThetaRadialAmbient line 26
  4. def OAI.CubicFirstMoment.cubicThetaRadialJet line 28
  5. lemma OAI.CubicFirstMoment.cubicThetaRadialJet_continuous line 31
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialJet_compact line 42
  7. lemma OAI.CubicFirstMoment.cubicThetaRadialJet_memLp line 53
  8. def OAI.CubicFirstMoment.cubicThetaRadialGraph line 58
  9. def OAI.CubicFirstMoment.cubicThetaRadialEnergySpace line 91
  10. instance OAI.CubicFirstMoment.cubicThetaRadialEnergy_complete line 94
  11. def OAI.CubicFirstMoment.cubicThetaRadialEnergyTest line 98