OAI/Analysis/CoulombIonization/Localization/BarrierEventSymmetryBarrier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.arrayObservedConfiguration line 16
2. def OAI.CoulombAtom.arrayUnorderedConfiguration line 20
3. lemma OAI.CoulombAtom.arrayUnorderedConfiguration_measurable line 24
4. lemma OAI.CoulombAtom.arrayUnorderedConfiguration_reindex line 34
5. def OAI.CoulombAtom.arrayObservationInformation line 44
6. lemma OAI.CoulombAtom.arrayObservationInformation_le line 49
7. lemma OAI.CoulombAtom.observationInformation_eq_arrayComap line 58
8. def OAI.CoulombAtom.symmetricArraySpace line 70
9. lemma OAI.CoulombAtom.arrayObservationInformation_le_symmetric line 79
10. theorem OAI.CoulombAtom.observation_event_symmetric_representation line 92