OAI/Analysis/CoulombIonization/RadialBounds/TruncationRadius.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.truncationRadius line 102
  2. lemma OAI.CoulombAtom.truncationRadius_pos line 103
  3. lemma OAI.CoulombAtom.truncationRadius_one_le line 105
  4. def OAI.CoulombAtom.truncationMultiplier line 108
  5. def OAI.CoulombAtom.truncateForm line 114
  6. lemma OAI.CoulombAtom.SobolevFermion.truncate line 117
  7. lemma OAI.CoulombAtom.truncation_value_le_one line 120
  8. lemma OAI.CoulombAtom.truncation_value_one line 127
  9. lemma OAI.CoulombAtom.truncation_derivative_zero line 137
  10. lemma OAI.CoulombAtom.truncation_derivative_bound line 148
  11. lemma OAI.CoulombAtom.truncation_eventually_identity line 167
  12. lemma OAI.CoulombAtom.truncateForm_eventually_identity line 179
  13. lemma OAI.CoulombAtom.truncateForm_value_sq_le line 193
  14. lemma OAI.CoulombAtom.truncateForm_gradient_sq_le line 202
  15. lemma OAI.CoulombAtom.truncateForm_mass_tendsto line 217
  16. lemma OAI.CoulombAtom.truncateForm_kinetic_tendsto line 232
  17. lemma OAI.CoulombAtom.truncateForm_coulomb_tendsto line 248
  18. lemma OAI.CoulombAtom.truncateForm_energy_tendsto line 265
  19. lemma OAI.CoulombAtom.truncation_value_zero line 293
  20. lemma OAI.CoulombAtom.truncateForm_support line 302
  21. lemma OAI.CoulombAtom.truncation_gradient_zero line 309
  22. lemma OAI.CoulombAtom.truncateForm_gradient_support line 319
  23. theorem OAI.CoulombAtom.admissible_compact_approximation line 327
  24. theorem OAI.CoulombAtom.quantum_sector_compact_near_minimizer line 357