OAI/Analysis/CoulombRadii/FieldAnalysis/RawObservable.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.rawSignedField line 15
2. lemma OAI.Coulomb.restrictedOutPotential_measurable_configuration line 18
3. lemma OAI.Coulomb.rawSignedField_measurable line 27
4. lemma OAI.Coulomb.rawSignedField_abs_le line 31
5. lemma OAI.Coulomb.restrictedOutPotential_permute line 41
6. lemma OAI.Coulomb.rawSignedField_permute line 47
7. lemma OAI.Coulomb.restrictedOutPotential_join line 52
8. lemma OAI.Coulomb.potentialForm_restrictedOutPotential line 58
9. lemma OAI.Coulomb.potentialForm_rawSignedField line 73
10. lemma OAI.Coulomb.coreConditionalObservable_rawSignedField line 87
11. lemma OAI.Coulomb.coreConditionalObservable_raw_positive_weight line 102
12. lemma OAI.Coulomb.potentialForm_labelCut line 113