OAI/Analysis/CoulombRadii/Variational/PhysicalBridge.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.flattenConfiguration line 14
  2. lemma OAI.NeutralAtom.flattenConfiguration_apply line 23
  3. lemma OAI.NeutralAtom.flattenConfiguration_symm_apply line 25
  4. lemma OAI.NeutralAtom.flattenConfiguration_symm_measurePreserving line 28
  5. lemma OAI.NeutralAtom.flattenConfiguration_measurePreserving line 31
  6. lemma OAI.NeutralAtom.flattenConfiguration_coordinateDirection line 35
  7. lemma OAI.NeutralAtom.flattenConfiguration_permute line 41
  8. lemma OAI.NeutralAtom.flattenConfiguration_symm_permute line 43
  9. lemma OAI.NeutralAtom.weakDirectional_pullback line 46
  10. def OAI.NeutralAtom.asH1 line 70
  11. def OAI.NeutralAtom.fromH1Wave line 87
  12. def OAI.NeutralAtom.fromH1Gradient line 89
  13. lemma OAI.NeutralAtom.fromH1_weak line 92
  14. lemma OAI.NeutralAtom.asH1_antisymmetric line 100
  15. lemma OAI.NeutralAtom.fromH1_domain line 106
  16. lemma OAI.NeutralAtom.fromH1_mass line 124
  17. lemma OAI.NeutralAtom.asH1_mass line 131
  18. lemma OAI.NeutralAtom.position_flattenConfiguration line 140
  19. lemma OAI.NeutralAtom.coulombPotential_flatten line 143
  20. lemma OAI.NeutralAtom.fromH1_energy line 150
  21. lemma OAI.NeutralAtom.asH1_energy line 188
  22. lemma OAI.NeutralAtom.asH1_groundState line 194
  23. lemma OAI.NeutralAtom.fromH1_groundState line 213
  24. lemma OAI.NeutralAtom.fromH1_exteriorMass line 223
  25. lemma OAI.NeutralAtom.asH1_exteriorMass line 251