OAI/Analysis/CoulombRadii/FieldAnalysis/SliceExpectation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.nuclearEnergy_unit_eq_coreCoulomb line 132
2. lemma OAI.Coulomb.potentialForm_cross_eq_coreCoulomb line 141
3. lemma OAI.Coulomb.conditionalEnergy_eq_screened line 147
4. def OAI.Coulomb.sliceExpectation line 155
5. lemma OAI.Coulomb.slice_weight_integrable_const line 158
6. lemma OAI.Coulomb.sliceExpectation_const line 166
7. lemma OAI.Coulomb.measurable_retained_sum line 174
8. def OAI.Coulomb.retainedNuclearPotential line 182
9. def OAI.Coulomb.retainedCrossPotential line 186
10. lemma OAI.Coulomb.retainedNuclearPotential_nonneg line 190
11. lemma OAI.Coulomb.retainedNuclearPotential_le line 193
12. lemma OAI.Coulomb.retainedNuclearPotential_measurable line 197
13. lemma OAI.Coulomb.retainedCrossPotential_nonneg line 202
14. lemma OAI.Coulomb.retainedCrossPotential_le line 205
15. lemma OAI.Coulomb.retainedCrossPotential_measurable line 209
16. lemma OAI.Coulomb.H1Vector.retained_outer_nuclear_integrable line 221
17. lemma OAI.Coulomb.H1Vector.retained_cross_integrable line 233
18. lemma OAI.Coulomb.potentialForm_retainedCross_eq line 245
19. lemma OAI.Coulomb.retained_field_weight line 266
20. lemma OAI.Coulomb.retained_field_weight_integrable line 275