OAI/Analysis/CoulombRadii/FormDomain/SmoothCompact.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.complex_smooth_compact_ibp line 31
  2. def OAI.Coulomb.H1Vector.ofSmoothCompact line 58
  3. lemma OAI.Coulomb.tensor_compact_support line 69
  4. def OAI.Coulomb.configurationHomeomorph line 78
  5. lemma OAI.Coulomb.tensorOrbital_compact_support line 83
  6. def OAI.Coulomb.positionCLM line 90
  7. lemma OAI.Coulomb.positionCLM_apply line 95
  8. lemma OAI.Coulomb.tensorOrbital_contDiff line 98
  9. def OAI.Coulomb.slaterConfiguration line 107
  10. lemma OAI.Coulomb.slaterConfiguration_expansion line 111
  11. lemma OAI.Coulomb.slaterConfiguration_contDiff line 118
  12. lemma OAI.Coulomb.slaterConfiguration_compact_support line 125
  13. def OAI.Coulomb.slaterState line 140
  14. lemma OAI.Coulomb.slaterState_antisymmetric line 146
  15. def OAI.Coulomb.flatSpinOrbital line 160
  16. lemma OAI.Coulomb.flatSpinOrbital_memLp line 163
  17. lemma OAI.Coulomb.flatSpinOrbital_inner line 176
  18. lemma OAI.Coulomb.slaterState_cubeState line 191
  19. lemma OAI.Coulomb.slaterState_normalized line 198