OAI/Analysis/CoulombIonization/Localization/UnshiftedEnsemble.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.priceEnergy_zero line 12
2. lemma OAI.CoulombAtom.corePriceExcess_le_zero_add line 15
3. lemma OAI.CoulombAtom.CoreObservationGraph.excess_le_zero_add line 24
4. lemma OAI.CoulombAtom.CoreObservationGraph.fieldMoment_tendsto_zero line 38
5. def OAI.CoulombAtom.CoreObservationEnsemble.coreParticleMoment line 64
6. lemma OAI.CoulombAtom.CoreObservationEnsemble.coreParticleMoment_nonneg line 67
7. lemma OAI.CoulombAtom.CoreObservationEnsemble.excess_le_zero_add line 70
8. lemma OAI.CoulombAtom.CoreObservationEnsemble.fieldMoment_tendsto_zero line 78
9. theorem OAI.CoulombAtom.ensemble_unshifted_local_field_scale line 85