OAI/Analysis/CoulombIonization/Fermionic/Multiplier2.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CoulombAtom.LipschitzMultiplier line 29
  2. lemma OAI.CoulombAtom.LipschitzMultiplier.value_memLp line 36
  3. lemma OAI.CoulombAtom.LipschitzMultiplier.gradient_memLp line 41
  4. def OAI.CoulombAtom.LipschitzMultiplier.apply line 53
  5. lemma OAI.CoulombAtom.LipschitzMultiplier.apply_value line 65
  6. lemma OAI.CoulombAtom.LipschitzMultiplier.apply_gradient line 71
  7. structure OAI.CoulombAtom.FermionLipschitzMultiplier line 80
  8. def OAI.CoulombAtom.FermionLipschitzMultiplier.apply line 83
  9. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.apply_value line 99
  10. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.apply_gradient line 105
  11. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.apply_nuclear line 114
  12. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.apply_pair line 123
  13. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.gradient_ims line 132
  14. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.value_pairing line 147
  15. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.nuclear_pairing line 160
  16. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.pair_pairing line 167
  17. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.kinetic_ims line 174
  18. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.operator_pairing line 188
  19. lemma OAI.CoulombAtom.lipschitz_ims_arithmetic line 201
  20. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.form_ims line 206
  21. theorem OAI.CoulombAtom.quantum_ground_multiplier_lipschitz line 221