OAI/Analysis/CoulombIonization/Variational/WeightedMass.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.weightedMass line 54
  2. def OAI.CoulombAtom.weightedGradient line 57
  3. def OAI.CoulombAtom.weightedFullDensity line 60
  4. def OAI.CoulombAtom.weightedCoreDensity line 63
  5. def OAI.CoulombAtom.weightedNuclear line 67
  6. def OAI.CoulombAtom.weightedPairs line 71
  7. lemma OAI.CoulombAtom.weightedMass_nonneg line 75
  8. lemma OAI.CoulombAtom.weightedFullDensity_delete line 79
  9. lemma OAI.CoulombAtom.FermionMultiplier.value_weighted_pairing line 89
  10. lemma OAI.CoulombAtom.ground_weighted_identity line 95
  11. lemma OAI.CoulombAtom.sum_rotate_three line 106
  12. def OAI.CoulombAtom.graphKineticPair line 112
  13. def OAI.CoulombAtom.weightedKinetic line 116
  14. lemma OAI.CoulombAtom.weightedKinetic_expand line 121
  15. lemma OAI.CoulombAtom.bindingTotal_full line 127
  16. lemma OAI.CoulombAtom.bindingTotal_kinetic line 135
  17. lemma OAI.CoulombAtom.sum_sub_le_transport line 146
  18. lemma OAI.CoulombAtom.bindingTotal_kinetic_diagonal line 153
  19. lemma OAI.CoulombAtom.bindingTotal_kinetic_lower_packed line 160
  20. lemma OAI.CoulombAtom.FermionMultiplier.form_weighted_packed line 175
  21. lemma OAI.CoulombAtom.binding_form_sum_arithmetic line 183
  22. lemma OAI.CoulombAtom.binding_form_lower line 193
  23. lemma OAI.CoulombAtom.bindingTotal_mass line 211
  24. lemma OAI.CoulombAtom.energy_weighted_core_le line 219
  25. lemma OAI.CoulombAtom.binding_cancellation line 233
  26. theorem OAI.CoulombAtom.quantum_ground_binding_regularized line 242