OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeFiniteEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual C1 sections of finite mass and gradient energy on the prime cover, with both coordinates retained as genuine L2 vectors.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeFiniteEnergy line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyValue line 42
  3. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyGradient line 48
  4. def OAI.CubicFirstMoment.cubicThetaPrimeEnergyAtkin line 67
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyValue_atkin_norm line 75
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyGradient_norm_sq line 81
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeEnergyGradient_atkin_norm line 91