OAI/Probability/StrongRayleigh/ObservationNoise.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.ObservationNoise.referenceMeasure line 19
  2. instance OAI.Problem336AdditiveD139.ObservationNoise.(instance at line 22) line 22
  3. def OAI.Problem336AdditiveD139.ObservationNoise.history line 26
  4. def OAI.Problem336AdditiveD139.ObservationNoise.increment line 30
  5. def OAI.Problem336AdditiveD139.ObservationNoise.incrementVariance line 34
  6. theorem OAI.Problem336AdditiveD139.ObservationNoise.incrementVariance_coe line 37
  7. theorem OAI.Problem336AdditiveD139.ObservationNoise.measurable_history line 43
  8. theorem OAI.Problem336AdditiveD139.ObservationNoise.measurable_increment line 54
  9. def OAI.Problem336AdditiveD139.ObservationNoise.historySigma line 60
  10. theorem OAI.Problem336AdditiveD139.ObservationNoise.historySigma_mono line 65
  11. def OAI.Problem336AdditiveD139.ObservationNoise.filtration line 74
  12. theorem OAI.Problem336AdditiveD139.ObservationNoise.measurable_current_observation line 82
  13. theorem OAI.Problem336AdditiveD139.ObservationNoise.increment_indep_history line 89
  14. theorem OAI.Problem336AdditiveD139.ObservationNoise.increment_hasLaw line 106
  15. theorem OAI.Problem336AdditiveD139.ObservationNoise.increment_condExp_gaussian line 115
  16. theorem OAI.Problem336AdditiveD139.ObservationNoise.increment_condExp_eq_zero line 131