OAI/Analysis/CoulombRadii/FieldAnalysis/CoreCoulombPotential.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.H1Vector.coulomb_density_prod_integrable line 64
2. def OAI.Coulomb.coreCoulombPotential line 99
3. lemma OAI.Coulomb.coreCoulombPotential_nonneg line 102
4. lemma OAI.Coulomb.coreCoulombPotential_bound line 110
5. lemma OAI.Coulomb.coreCoulombPotential_mul_integrable line 120
6. lemma OAI.Coulomb.coreCoulombPotential_fubini line 131
7. lemma OAI.Coulomb.weighted_series_integrable_hasSum line 157
8. lemma OAI.Coulomb.coreInteractionDensity_integrand_integrable line 187
9. lemma OAI.Coulomb.coreInteractionDensity_eq line 198
10. lemma OAI.Coulomb.finiteFermiDensity_integrable line 213
11. lemma OAI.Coulomb.attraction_nonneg line 225
12. lemma OAI.Coulomb.attraction_measurable line 229
13. theorem OAI.Coulomb.infinite_fermi_core_trial line 233