OAI/Analysis/CoulombIonization/FormDomain/CoreKinetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.coreKinetic line 122
  2. def OAI.CoulombAtom.coreNuclear line 125
  3. def OAI.CoulombAtom.outNuclear line 128
  4. def OAI.CoulombAtom.coreRepulsion line 131
  5. lemma OAI.CoulombAtom.integral_core_kinetic line 135
  6. lemma OAI.CoulombAtom.integral_core_nuclear line 155
  7. lemma OAI.CoulombAtom.integral_core_repulsion line 180
  8. lemma OAI.CoulombAtom.coreSlice_parts_integrable line 221
  9. lemma OAI.CoulombAtom.integrated_core_parts line 256
  10. lemma OAI.CoulombAtom.sum_embedding_le line 275
  11. lemma OAI.CoulombAtom.coreKinetic_le line 282
  12. lemma OAI.CoulombAtom.coreRepulsion_le line 293
  13. lemma OAI.CoulombAtom.formNuclear_core_out line 316
  14. theorem OAI.CoulombAtom.exterior_energy_lower line 323
  15. lemma OAI.CoulombAtom.outNuclear_le line 332