OAI/Analysis/CoulombIonization/Localization/CoreHistoryMassBarrier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.sum_nextCoreObservation_mass line 17
2. lemma OAI.CoulombAtom.sum_nextCoreObservation_excess line 31
3. structure OAI.CoulombAtom.CoreObservationGraph line 44
4. def OAI.CoulombAtom.CoreObservationGraph.initial line 53
5. def OAI.CoulombAtom.CoreObservationGraph.observe line 60
6. def OAI.CoulombAtom.CoreObservationGraph.mass line 68
7. def OAI.CoulombAtom.CoreObservationGraph.coreAverage line 70
8. lemma OAI.CoulombAtom.CoreObservationGraph.observe_mass line 73
9. lemma OAI.CoulombAtom.CoreObservationGraph.mass_nonneg line 78
10. lemma OAI.CoulombAtom.CoreObservationGraph.observe_total_size line 80