OAI/Probability/StrongRayleigh/ReferenceObservation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336AdditiveD139.ReferenceObservation.Space line 16
  2. def OAI.Problem336AdditiveD139.ReferenceObservation.law line 18
  3. instance OAI.Problem336AdditiveD139.ReferenceObservation.law_isProbabilityMeasure line 22
  4. theorem OAI.Problem336AdditiveD139.ReferenceObservation.signal_hasLaw line 29
  5. theorem OAI.Problem336AdditiveD139.ReferenceObservation.noiseField_hasLaw line 32
  6. theorem OAI.Problem336AdditiveD139.ReferenceObservation.noise_hasLaw line 37
  7. theorem OAI.Problem336AdditiveD139.ReferenceObservation.iid_noise line 42
  8. theorem OAI.Problem336AdditiveD139.ReferenceObservation.signal_indep_noiseField line 46
  9. def OAI.Problem336AdditiveD139.ReferenceObservation.noise line 52
  10. def OAI.Problem336AdditiveD139.ReferenceObservation.observation line 54
  11. theorem OAI.Problem336AdditiveD139.ReferenceObservation.noise_projection_measurePreserving line 57
  12. theorem OAI.Problem336AdditiveD139.ReferenceObservation.noise_isPreBrownian line 61
  13. theorem OAI.Problem336AdditiveD139.ReferenceObservation.noise_isBrownian line 65
  14. theorem OAI.Problem336AdditiveD139.ReferenceObservation.iid_noise_paths line 70
  15. theorem OAI.Problem336AdditiveD139.ReferenceObservation.signal_indep_noise_paths line 74
  16. theorem OAI.Problem336AdditiveD139.ReferenceObservation.measurable_noise line 80
  17. theorem OAI.Problem336AdditiveD139.ReferenceObservation.measurable_observation line 84
  18. theorem OAI.Problem336AdditiveD139.ReferenceObservation.measurable_observation_joint line 91
  19. theorem OAI.Problem336AdditiveD139.ReferenceObservation.continuous_observation_path line 99
  20. theorem OAI.Problem336AdditiveD139.ReferenceObservation.ae_continuous_noise_paths line 103
  21. theorem OAI.Problem336AdditiveD139.ReferenceObservation.ae_continuous_observation_paths line 108
  22. theorem OAI.Problem336AdditiveD139.ReferenceObservation.signal_real_mem_unitInterval line 115
  23. theorem OAI.Problem336AdditiveD139.ReferenceObservation.integrable_signal_real line 119
  24. theorem OAI.Problem336AdditiveD139.ReferenceObservation.integrable_observation line 128