OAI/Analysis/CoulombIonization/Localization/PatchCenterObservable.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.conditionalPatchCenter line 20
2. def OAI.CoulombAtom.weightedNegativePatchCenter line 26
3. lemma OAI.CoulombAtom.weightedNegativePatchCenter_nonneg line 30
4. lemma OAI.CoulombAtom.normalizedCoreField_eval_aemeasurable line 35
5. lemma OAI.CoulombAtom.tfBallPotential_zero_continuous line 42
6. lemma OAI.CoulombAtom.conditionalPatchCenter_aemeasurable line 51
7. lemma OAI.CoulombAtom.weightedNegativePatchCenter_aestronglyMeasurable line 58
8. theorem OAI.CoulombAtom.negativePatchCenter_integral_event line 65