OAI/Analysis/CoulombIonization/RadialBounds/FermiMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.fermiRegion line 16
2. def OAI.CoulombAtom.fermiMeasure line 19
3. lemma OAI.CoulombAtom.fermiRadius_measurable line 21
4. lemma OAI.CoulombAtom.fermiRegion_measurable line 25
5. lemma OAI.CoulombAtom.fermiMeasure_le line 28
6. lemma OAI.CoulombAtom.fermiRegion_subset line 30
7. lemma OAI.CoulombAtom.fermiMeasure_finite line 45
8. lemma OAI.CoulombAtom.fermiMeasure_mem line 53
9. lemma OAI.CoulombAtom.fermiMeasure_integral line 58
10. lemma OAI.CoulombAtom.fermiMeasure_integrable_continuous line 74
11. lemma OAI.CoulombAtom.fermiMeasure_mass line 81
12. lemma OAI.CoulombAtom.fermiMeasure_kinetic line 93