OAI/NumberTheory/CubicMoment/Theta/CubicThetaGlobalEnergy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The global energy completion of genuine compact smooth cubic sections. Its two coordinates are the value and the actual gradient.

  1. abbrev OAI.CubicFirstMoment.CubicThetaGlobalEnergyAmbient line 12
  2. def OAI.CubicFirstMoment.cubicThetaGlobalEnergyGraph line 14
  3. def OAI.CubicFirstMoment.cubicThetaGlobalEnergySpace line 18
  4. instance OAI.CubicFirstMoment.cubicThetaGlobalEnergySpace_complete line 21
  5. def OAI.CubicFirstMoment.cubicThetaGlobalEnergyTest line 24
  6. def OAI.CubicFirstMoment.cubicThetaGlobalInclusion line 27
  7. def OAI.CubicFirstMoment.cubicThetaGlobalEnergyGradient line 31
  8. lemma OAI.CubicFirstMoment.cubicThetaGlobalInclusion_test line 35
  9. lemma OAI.CubicFirstMoment.cubicThetaGlobalEnergyGradient_test line 38
  10. lemma OAI.CubicFirstMoment.cubicThetaGlobalInclusion_bound line 41
  11. lemma OAI.CubicFirstMoment.cubicThetaGlobalInclusion_norm line 44
  12. lemma OAI.CubicFirstMoment.cubicThetaGlobalEnergy_norm_sq line 49
  13. lemma OAI.CubicFirstMoment.cubicThetaGlobalEnergyTest_norm_sq line 53