OAI/Analysis/CoulombRadii/FieldAnalysis/AtomicWeighted.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.potentialForm_smoothMul line 13
2. lemma OAI.Coulomb.regularized_weighted_core line 25
3. def OAI.Coulomb.atomicCross line 87
4. lemma OAI.Coulomb.atomicCross_integrable line 89
5. lemma OAI.Coulomb.potentialForm_bdd_mul_integrable line 93
6. lemma OAI.Coulomb.potentialForm_tendsto_bdd line 98
7. def OAI.Coulomb.atomicWeight line 119
8. lemma OAI.Coulomb.atomicWeight_bound line 120
9. lemma OAI.Coulomb.atomicWeight_measurable line 123
10. lemma OAI.Coulomb.regularized_weighted_core_limit line 125