OAI/Analysis/CoulombIonization/Localization/ObservationLikelihood.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombObservation.shiftedObservationEvent line 18
  2. lemma OAI.CoulombObservation.shiftedObservationEvent_measurable line 21
  3. def OAI.CoulombObservation.observationLikelihood line 26
  4. lemma OAI.CoulombObservation.observationLikelihood_eq_probability line 29
  5. lemma OAI.CoulombObservation.observationLikelihood_nonneg line 45
  6. lemma OAI.CoulombObservation.observationLikelihood_le_one line 51
  7. lemma OAI.CoulombObservation.observationLikelihood_contDiff line 57
  8. lemma OAI.CoulombObservation.observationLikelihood_fderiv line 63
  9. def OAI.CoulombObservation.observationPlacement line 97
  10. lemma OAI.CoulombObservation.observationPlacement_apply line 101
  11. def OAI.CoulombObservation.arrayLikelihood line 105
  12. def OAI.CoulombObservation.arrayScore line 109
  13. lemma OAI.CoulombObservation.arrayLikelihood_eq_probability line 113
  14. lemma OAI.CoulombObservation.arrayLikelihood_nonneg line 119
  15. lemma OAI.CoulombObservation.arrayLikelihood_le_one line 123
  16. lemma OAI.CoulombObservation.arrayLikelihood_contDiff line 127
  17. lemma OAI.CoulombObservation.arrayLikelihood_fderiv line 132
  18. lemma OAI.CoulombObservation.eventScore_zero line 143
  19. lemma OAI.CoulombObservation.arrayScore_sq line 150
  20. lemma OAI.CoulombObservation.arrayScore_sq_one line 168