OAI/Analysis/CoulombIonization/Localization/PatchLocalObservable.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAnalysis.local_coulomb_pair_eq line 17
2. def OAI.CoulombAtom.weightedPatchLocalPotential line 42
3. lemma OAI.CoulombAtom.retainedPatchLocalPotential_nonneg line 48
4. lemma OAI.CoulombAtom.retainedPatchLocalPotential_le line 53
5. lemma OAI.CoulombAtom.retainedPatchLocalPotential_measurable line 70
6. lemma OAI.CoulombAtom.weightedPatchLocalPotential_nonneg line 82
7. lemma OAI.CoulombAtom.weightedPatchLocalPotential_integrable line 88