OAI/Analysis/CoulombRadii/FieldAnalysis/WeightedInner.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.weightedInnerField line 13
2. lemma OAI.Coulomb.weightedInnerField_measurable line 17
3. lemma OAI.Coulomb.weightedInnerField_reindex line 33
4. lemma OAI.Coulomb.inner_shell_separation line 42
5. lemma OAI.Coulomb.weighted_raw_inner_abs_le line 51
6. lemma OAI.Coulomb.weightedInnerField_abs_le line 72
7. lemma OAI.Coulomb.weightedInnerField_join_of_support line 82
8. lemma OAI.Coulomb.potentialForm_const_mul_value line 94
9. lemma OAI.Coulomb.conditional_weighted_inner_le line 98