OAI/Analysis/CoulombIonization/Localization/ObservationIntegral.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombObservation.integrable_bounded_probability line 17
  2. lemma OAI.CoulombObservation.bounded_probability_rpow_integrable line 23
  3. lemma OAI.CoulombObservation.integral_bounded_probability_rpow line 31
  4. def OAI.CoulombObservation.eventMomentOrder line 42
  5. lemma OAI.CoulombObservation.eventMomentOrder_pos line 44
  6. lemma OAI.CoulombObservation.eventMomentOrder_bound line 47
  7. lemma OAI.CoulombObservation.eventMomentOrder_rpow_bound line 55
  8. lemma OAI.CoulombObservation.eventMomentOrder_integral_bound line 65
  9. lemma OAI.CoulombObservation.eventLog_eq line 79
  10. def OAI.CoulombObservation.arrayFisher line 87
  11. lemma OAI.CoulombObservation.arrayFisher_nonneg line 91
  12. lemma OAI.CoulombObservation.arrayFisher_measurable line 95
  13. lemma OAI.CoulombObservation.reciprocal_moment_sub_one_nonneg line 102
  14. lemma OAI.CoulombObservation.arrayFisher_integrable line 107
  15. lemma OAI.CoulombObservation.arrayFisher_integral_moment line 119
  16. def OAI.CoulombObservation.observationFisherConstant line 142
  17. lemma OAI.CoulombObservation.observationFisherConstant_pos line 144
  18. theorem OAI.CoulombObservation.arrayFisher_integral_log line 148