OAI/Analysis/CoulombIonization/Fermionic/Multiplier.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CoulombAtom.SmoothMultiplier line 28
  2. lemma OAI.CoulombAtom.memLp_bounded_mul line 36
  3. lemma OAI.CoulombAtom.SmoothMultiplier.derivative_continuous line 47
  4. lemma OAI.CoulombAtom.SmoothMultiplier.value_memLp line 58
  5. lemma OAI.CoulombAtom.SmoothMultiplier.gradient_memLp line 63
  6. def OAI.CoulombAtom.SmoothMultiplier.apply line 70
  7. lemma OAI.CoulombAtom.SmoothMultiplier.apply_value line 82
  8. lemma OAI.CoulombAtom.SmoothMultiplier.apply_gradient line 88
  9. structure OAI.CoulombAtom.FermionMultiplier line 97
  10. def OAI.CoulombAtom.FermionMultiplier.apply line 100
  11. lemma OAI.CoulombAtom.FermionMultiplier.apply_value line 116
  12. lemma OAI.CoulombAtom.FermionMultiplier.apply_gradient line 122
  13. lemma OAI.CoulombAtom.graphNuclear_ae line 129
  14. lemma OAI.CoulombAtom.graphPair_ae line 135
  15. lemma OAI.CoulombAtom.FermionMultiplier.apply_nuclear line 147
  16. lemma OAI.CoulombAtom.FermionMultiplier.apply_pair line 156
  17. lemma OAI.CoulombAtom.coulombFormOperator_pairing line 165
  18. lemma OAI.CoulombAtom.energy_le_graphForm line 189
  19. theorem OAI.CoulombAtom.quantum_ground_form_equation line 202
  20. lemma OAI.CoulombAtom.FermionMultiplier.gradient_ims line 218
  21. lemma OAI.CoulombAtom.graphValue_pairing line 233
  22. lemma OAI.CoulombAtom.FermionMultiplier.value_pairing line 247
  23. lemma OAI.CoulombAtom.FermionMultiplier.nuclear_pairing line 260
  24. lemma OAI.CoulombAtom.FermionMultiplier.pair_pairing line 267
  25. lemma OAI.CoulombAtom.FermionMultiplier.kinetic_ims line 274
  26. lemma OAI.CoulombAtom.coulombFormOperator_diagonal line 288
  27. lemma OAI.CoulombAtom.FermionMultiplier.operator_pairing line 300
  28. lemma OAI.CoulombAtom.ims_arithmetic line 313
  29. lemma OAI.CoulombAtom.FermionMultiplier.form_ims line 318
  30. theorem OAI.CoulombAtom.quantum_ground_multiplier_smooth line 333