OAI/Analysis/CoulombIonization/Localization/FormRawLaw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.formRawDensity line 18
  2. lemma OAI.CoulombAtom.formRawDensity_nonneg line 21
  3. lemma OAI.CoulombAtom.formRawDensity_integrable line 24
  4. lemma OAI.CoulombAtom.formRawDensity_integral line 28
  5. def OAI.CoulombAtom.formRawLaw line 32
  6. lemma OAI.CoulombAtom.formRawLaw_univ line 35
  7. lemma OAI.CoulombAtom.formRawLaw_finite line 42
  8. lemma OAI.CoulombAtom.formRawLaw_probability line 48
  9. lemma OAI.CoulombAtom.formRawLaw_integral line 53
  10. lemma OAI.CoulombAtom.formRawLaw_integral_eq_spin_sum line 61
  11. def OAI.CoulombAtom.rawBallCount line 71
  12. def OAI.CoulombAtom.rawStripCount line 74
  13. lemma OAI.CoulombAtom.rawBallCount_nonneg line 77
  14. lemma OAI.CoulombAtom.rawBallCount_le line 81
  15. lemma OAI.CoulombAtom.configuration_distance_measurable line 87
  16. lemma OAI.CoulombAtom.rawBallCount_measurable line 92
  17. lemma OAI.CoulombAtom.rawBallCount_sq_integrable line 98
  18. lemma OAI.CoulombAtom.rawStripCount_eq_card line 107
  19. lemma OAI.CoulombAtom.upperCount_le_rawBallCount line 121
  20. theorem OAI.CoulombAtom.radial_raw_radius_selection line 128