OAI/Analysis/CoulombIonization/Localization/OrdinaryDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.rawOneParticleLaw line 17
  2. lemma OAI.CoulombAtom.rawOneParticleLaw_finite line 20
  3. lemma OAI.CoulombAtom.rawOneParticleLaw_ac line 25
  4. def OAI.CoulombAtom.ordinaryDensity line 32
  5. lemma OAI.CoulombAtom.ordinaryDensity_nonneg line 35
  6. lemma OAI.CoulombAtom.ordinaryDensity_measurable line 38
  7. lemma OAI.CoulombAtom.ordinaryDensity_integrable line 42
  8. lemma OAI.CoulombAtom.rawOneParticleLaw_pairing line 48
  9. lemma OAI.CoulombAtom.ordinaryDensity_pairing line 59
  10. lemma OAI.CoulombAtom.ordinaryDensity_measure line 69
  11. lemma OAI.CoulombAtom.ordinaryDensity_mass line 81
  12. lemma OAI.CoulombAtom.ordinaryDensity_raw_local_potential line 91
  13. theorem OAI.CoulombAtom.ordinaryDensity_raw_local_holder line 129