OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeEnergySpace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The completed actual value-gradient graph on the finite prime cover. The Atkin transformation extends as an isometry of this energy space.

  1. abbrev OAI.CubicFirstMoment.CubicThetaPrimeEnergyAmbient line 14
  2. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyGraph line 17
  3. def OAI.CubicFirstMoment.cubicThetaPrimeEnergySpace line 22
  4. instance OAI.CubicFirstMoment.cubicThetaPrimeEnergySpace_complete line 25
  5. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyTest line 29
  6. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyInclusion line 34
  7. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyDerivative line 39
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyInclusion_test line 44
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyDerivative_test line 48
  10. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergy_norm_sq line 52
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyTest_dense line 57
  12. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyAtkin_test_norm line 72
  13. def OAI.CubicFirstMoment.cubicThetaPrimeAtkinEnergy line 82
  14. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinEnergy_test line 87