OAI/Probability/StrongRayleigh/ReferenceNoise.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.ReferenceNoise.history line 17
  2. def OAI.Problem336AdditiveD139.ReferenceNoise.increment line 21
  3. def OAI.Problem336AdditiveD139.ReferenceNoise.incrementVariance line 25
  4. lemma OAI.Problem336AdditiveD139.ReferenceNoise.measurable_history line 28
  5. lemma OAI.Problem336AdditiveD139.ReferenceNoise.measurable_increment line 38
  6. theorem OAI.Problem336AdditiveD139.ReferenceNoise.increment_indep_history line 50
  7. theorem OAI.Problem336AdditiveD139.ReferenceNoise.increment_hasLaw line 74
  8. theorem OAI.Problem336AdditiveD139.ReferenceNoise.increment_condExp_test line 82
  9. theorem OAI.Problem336AdditiveD139.ReferenceNoise.increment_condExp_eq_zero line 105
  10. lemma OAI.Problem336AdditiveD139.ReferenceNoise.coe_incrementVariance line 115
  11. theorem OAI.Problem336AdditiveD139.ReferenceNoise.increment_condExp_sq line 119
  12. theorem OAI.Problem336AdditiveD139.ReferenceNoise.increment_condExp_characteristic line 138