OAI/Analysis/CoulombRadii/FieldAnalysis/FieldSubmean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.coreCoulombPotential_aestronglyMeasurable line 13
2. lemma OAI.Coulomb.coreField_aestronglyMeasurable line 25
3. lemma OAI.Coulomb.coreField_ballCloud_integrable line 29
4. lemma OAI.Coulomb.coreField_positive_ballCloud_integrable line 47
5. lemma OAI.Coulomb.attraction_le_totalCharge_div line 56
6. lemma OAI.Coulomb.coreField_positive_square_ballCloud_integrable line 66
7. lemma OAI.Coulomb.ballCloud_nested_le line 92
8. lemma OAI.Coulomb.square_weighted_mean_le line 106
9. theorem OAI.Coulomb.coreField_positive_submean_square line 127