OAI/Analysis/CoulombRadii/Localization/DensityCut.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.densityCut line 97
2. lemma OAI.Coulomb.densityCut_nonneg line 98
3. lemma OAI.Coulomb.densityCut_le line 100
4. lemma OAI.Coulomb.densityCut_bound line 101
5. lemma OAI.Coulomb.densityCut_measurable line 102
6. lemma OAI.Coulomb.densityCut_integrable line 104
7. lemma OAI.Coulomb.densityCut_kinetic_integrable line 110
8. lemma OAI.Coulomb.densityCut_support line 117
9. lemma OAI.Coulomb.densityCut_tendsto line 120
10. lemma OAI.Coulomb.packetDensity_mono line 126
11. lemma OAI.Coulomb.packetDensity_cut_tendsto line 134
12. lemma OAI.Coulomb.packetDensity_cut_weighted_tendsto line 148