OAI/Probability/GaussianReplacement/Observation.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.appendEquiv line 13
  2. lemma OAI.CurrentProjection.appendEquiv_map line 25
  3. abbrev OAI.CurrentProjection.Observations line 29
  4. def OAI.CurrentProjection.pairObservation line 31
  5. def OAI.CurrentProjection.observationEquiv line 34
  6. lemma OAI.CurrentProjection.observationEquiv_apply line 37
  7. def OAI.CurrentProjection.gaussianObservation line 40
  8. instance OAI.CurrentProjection.gaussianObservation_probability line 43
  9. def OAI.CurrentProjection.gaussianObservations line 46
  10. instance OAI.CurrentProjection.gaussianObservations_probability line 49
  11. lemma OAI.CurrentProjection.gaussianObservations_eq line 52
  12. def OAI.CurrentProjection.ownObservations line 58
  13. lemma OAI.CurrentProjection.measurable_ownObservations line 61
  14. lemma OAI.CurrentProjection.ownObservations_append line 66
  15. lemma OAI.CurrentProjection.gaussianObservations_append line 71
  16. lemma OAI.CurrentProjection.conditionalReferenceKL_map_context line 76
  17. lemma OAI.CurrentProjection.conditionalReferenceKL_context_equiv line 92
  18. def OAI.CurrentProjection.observationReferenceKL line 100
  19. lemma OAI.CurrentProjection.observationReferenceKL_decomposition line 104
  20. lemma OAI.CurrentProjection.observationReferenceKL_chain_exposed line 116
  21. def OAI.CurrentProjection.snocEquiv line 129
  22. lemma OAI.CurrentProjection.snocEquiv_apply line 134
  23. lemma OAI.CurrentProjection.snocEquiv_map line 139
  24. lemma OAI.CurrentProjection.conditionalReferenceKL_outcome_equiv line 148
  25. def OAI.CurrentProjection.arrayResidualObservation line 162
  26. lemma OAI.CurrentProjection.measurable_arrayResidualObservation line 165
  27. def OAI.CurrentProjection.arrayResidualLaw line 171
  28. instance OAI.CurrentProjection.arrayResidualLaw_probability line 175
  29. def OAI.CurrentProjection.freshArrayLaw line 181
  30. instance OAI.CurrentProjection.freshArrayLaw_probability line 184
  31. def OAI.CurrentProjection.freshReference line 188
  32. def OAI.CurrentProjection.freshSlope line 192
  33. lemma OAI.CurrentProjection.freshArrayLaw_eq line 196
  34. lemma OAI.CurrentProjection.freshArrayLaw_fst line 203
  35. lemma OAI.CurrentProjection.arrayResidualLaw_eq line 214
  36. lemma OAI.CurrentProjection.scalarObservationLaw_context line 223
  37. lemma OAI.CurrentProjection.freshSlope_eq line 235
  38. lemma OAI.CurrentProjection.ownObservations_snoc line 244
  39. lemma OAI.CurrentProjection.prod_append_gaussian_map line 249
  40. lemma OAI.CurrentProjection.arrayResidualLaw_append line 262
  41. lemma OAI.CurrentProjection.freshArrayLaw_append line 285
  42. lemma OAI.CurrentProjection.freshReference_append line 300
  43. def OAI.CurrentProjection.singleResidualObservation line 324
  44. lemma OAI.CurrentProjection.measurable_singleResidualObservation line 327
  45. def OAI.CurrentProjection.singleSignalLaw line 331
  46. instance OAI.CurrentProjection.singleSignalLaw_probability line 335
  47. def OAI.CurrentProjection.singleObservationLaw line 341
  48. instance OAI.CurrentProjection.singleObservationLaw_probability line 344
  49. def OAI.CurrentProjection.singleReference line 348
  50. lemma OAI.CurrentProjection.singleObservationLaw_eq line 352
  51. lemma OAI.CurrentProjection.singleObservationLaw_fst line 358
  52. lemma OAI.CurrentProjection.singleObservationLaw_scalar line 365
  53. lemma OAI.CurrentProjection.singleReference_fresh line 373
  54. lemma OAI.CurrentProjection.gaussianRows_one line 390
  55. lemma OAI.CurrentProjection.gaussianObservations_one line 394
  56. lemma OAI.CurrentProjection.singleSignalLaw_fresh line 398
  57. lemma OAI.CurrentProjection.freshReference_one line 412
  58. lemma OAI.CurrentProjection.freshReference_succ line 426
  59. lemma OAI.CurrentProjection.arrayResidualLaw_context line 432
  60. lemma OAI.CurrentProjection.freshReference_context line 444
  61. lemma OAI.CurrentProjection.freshSlope_context line 456
  62. lemma OAI.CurrentProjection.arrayResidualLaw_keep line 464
  63. lemma OAI.CurrentProjection.arrayResidualLaw_drop_last line 472
  64. lemma OAI.CurrentProjection.conditionalReferenceKL_map_context_le line 492
  65. lemma OAI.CurrentProjection.freshSlope_monotone line 506
  66. lemma OAI.CurrentProjection.freshReference_monotone line 518
  67. lemma OAI.CurrentProjection.freshSlope_mul_le line 525
  68. lemma OAI.CurrentProjection.freshSlope_average line 534
  69. lemma OAI.CurrentProjection.scalarReference_context line 549
  70. lemma OAI.CurrentProjection.freshSlope_succ line 556