OAI/Analysis/CoulombIonization/Variational/BindingNuclearSum.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.bindingPairApprox_ite_integral_le line 58
  2. lemma OAI.CoulombAtom.graph_nuclear_integrable line 70
  3. lemma OAI.CoulombAtom.graph_pair_integrable line 76
  4. def OAI.CoulombAtom.bindingNuclearSum line 83
  5. def OAI.CoulombAtom.bindingPairSum line 86
  6. def OAI.CoulombAtom.bindingCappedSum line 89
  7. lemma OAI.CoulombAtom.graph_mass_integral line 93
  8. lemma OAI.CoulombAtom.bindingNuclearSum_tendsto line 98
  9. lemma OAI.CoulombAtom.bindingCappedSum_tendsto line 109
  10. lemma OAI.CoulombAtom.bindingCappedSum_le line 131
  11. lemma OAI.CoulombAtom.quantum_ground_binding_approx line 156
  12. theorem OAI.CoulombAtom.quantum_ground_particle_bound line 169