OAI/Geometry/NodalSets/Charts/SphereEnergyCompletion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Yau.Target.SphereEnergyData line 11
  2. def OAI.Yau.Target.SphereEnergySmooth line 20
  3. instance OAI.Yau.Target.SphereEnergySmooth.instAddCommGroup line 24
  4. instance OAI.Yau.Target.SphereEnergySmooth.instModule line 25
  5. instance OAI.Yau.Target.SphereEnergySmooth.instInnerCore line 26
  6. instance OAI.Yau.Target.SphereEnergySmooth.instNormedAddCommGroup line 28
  7. instance OAI.Yau.Target.SphereEnergySmooth.instInnerProductSpace line 29
  8. def OAI.Yau.Target.SphereEnergySmooth.toSmooth line 32
  9. theorem OAI.Yau.Target.SphereEnergySmooth.norm_sq line 34
  10. abbrev OAI.Yau.Target.SphereEnergyHilbert line 41
  11. def OAI.Yau.Target.sphereEnergyToCompletion line 43
  12. theorem OAI.Yau.Target.sphereEnergyToCompletion_dense line 46