OAI/Analysis/CoulombRadii/FieldAnalysis/WedgeMultiplicity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.mass_permutation line 64
  2. lemma OAI.Coulomb.kinetic_permutation line 72
  3. lemma OAI.Coulomb.mass_fullAntisymmetrize_of_sq line 82
  4. lemma OAI.Coulomb.kinetic_fullAntisymmetrize_of_sq line 97
  5. lemma OAI.Coulomb.mass_scale line 126
  6. lemma OAI.Coulomb.kinetic_scale line 129
  7. lemma OAI.Coulomb.antisymmetric_scale line 133
  8. def OAI.Coulomb.wedgeMultiplicity line 141
  9. lemma OAI.Coulomb.wedgeMultiplicity_pos line 144
  10. def OAI.Coulomb.H1Vector.wedge line 148
  11. lemma OAI.Coulomb.wedge_normalizer_sq line 151
  12. lemma OAI.Coulomb.wedge_antisymmetric line 156
  13. lemma OAI.Coulomb.mass_wedge line 160
  14. lemma OAI.Coulomb.kinetic_wedge line 171
  15. def OAI.Coulomb.potentialEnergy line 183
  16. lemma OAI.Coulomb.permute_integral_real line 186
  17. lemma OAI.Coulomb.potential_integrable_permutation line 191
  18. lemma OAI.Coulomb.potentialEnergy_permutation line 199
  19. lemma OAI.Coulomb.potentialEnergy_fullAntisymmetrize_of_sq line 210
  20. lemma OAI.Coulomb.potentialEnergy_scale line 231
  21. lemma OAI.Coulomb.potentialEnergy_wedge line 236