OAI/Analysis/CoulombIonization/Localization/UnorderedObservations.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.configurationSetoid line 18
  2. abbrev OAI.CoulombAtom.UnorderedConfiguration line 29
  3. def OAI.CoulombAtom.unorderedConfiguration line 31
  4. lemma OAI.CoulombAtom.unorderedConfiguration_measurable line 34
  5. def OAI.CoulombAtom.unorderedStatistic line 37
  6. lemma OAI.CoulombAtom.unorderedStatistic_mk line 43
  7. lemma OAI.CoulombAtom.unorderedStatistic_measurable line 46
  8. def OAI.CoulombAtom.physicalObservedConfiguration line 52
  9. lemma OAI.CoulombAtom.physicalObservedConfiguration_measurable line 56
  10. def OAI.CoulombAtom.unorderedObservedConfiguration line 67
  11. lemma OAI.CoulombAtom.unorderedObservedConfiguration_measurable line 71
  12. def OAI.CoulombAtom.observationInformation line 75
  13. lemma OAI.CoulombAtom.observationInformation_le line 80
  14. lemma OAI.CoulombAtom.observationInformation_antitone line 89
  15. lemma OAI.CoulombAtom.observationInformation_terminal line 98
  16. lemma OAI.CoulombAtom.observedStatistic_information_measurable line 105
  17. lemma OAI.CoulombObservation.compactNoiseLaw_ae_support line 125
  18. lemma OAI.CoulombObservation.compactNoiseLaw_pi_ae_support line 132
  19. def OAI.CoulombAtom.physicalObservationLaw line 142
  20. instance OAI.CoulombAtom.physicalObservationLaw_finite line 146
  21. lemma OAI.CoulombAtom.physicalObservationLaw_probability line 151
  22. lemma OAI.CoulombAtom.physicalObservedConfiguration_displacement line 156
  23. lemma OAI.CoulombAtom.physicalObservationLaw_ae_displacement line 182
  24. def OAI.CoulombAtom.observedLocalCount line 191
  25. lemma OAI.CoulombAtom.observedLocalCount_information_measurable line 195
  26. lemma OAI.CoulombAtom.observedLocalCount_nonneg line 201
  27. lemma OAI.CoulombAtom.observedLocalCount_le line 206
  28. lemma OAI.CoulombAtom.matchedLocal_test_error line 212