OAI/Probability/GaussianReplacement/RowOrder.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.exchangeMiddle line 13
  2. lemma OAI.CurrentProjection.cauchyObservationLaw_single line 23
  3. lemma OAI.CurrentProjection.cauchyReference_single line 41
  4. lemma OAI.CurrentProjection.cauchyReference_context line 48
  5. lemma OAI.CurrentProjection.freshSlope_next_residual line 63
  6. def OAI.CurrentProjection.liftActualObservation line 70
  7. lemma OAI.CurrentProjection.measurable_liftActualObservation line 74
  8. def OAI.CurrentProjection.liftActualLaw line 80
  9. instance OAI.CurrentProjection.liftActualLaw_probability line 84
  10. lemma OAI.CurrentProjection.liftActualLaw_fst line 90
  11. def OAI.CurrentProjection.actualFreshArrayLaw line 100
  12. lemma OAI.CurrentProjection.measurable_actualFreshArray line 106
  13. instance OAI.CurrentProjection.actualFreshArrayLaw_probability line 113
  14. lemma OAI.CurrentProjection.actualFreshArrayLaw_first line 119
  15. lemma OAI.CurrentProjection.actualFreshArrayLaw_second line 132
  16. lemma OAI.CurrentProjection.actualFreshArrayLaw_swapped_first line 143
  17. lemma OAI.CurrentProjection.actualFreshArrayLaw_swapped_second line 157
  18. lemma OAI.CurrentProjection.actual_fresh_diamond line 168
  19. lemma OAI.CurrentProjection.residualLabelLaw_to_single line 184
  20. lemma OAI.CurrentProjection.scalarObservationLaw_fst_direct line 195
  21. lemma OAI.CurrentProjection.singleReference_lift_eq line 203
  22. lemma OAI.CurrentProjection.actual_fresh_row_bound line 230
  23. def OAI.CurrentProjection.initialArray line 249
  24. lemma OAI.CurrentProjection.measurable_initialArray line 252
  25. lemma OAI.CurrentProjection.initialArray_pi line 256
  26. def OAI.CurrentProjection.prefixLaw line 269
  27. instance OAI.CurrentProjection.prefixLaw_probability line 273
  28. lemma OAI.CurrentProjection.prefixLaw_fst line 279
  29. lemma OAI.CurrentProjection.prefixLaw_self line 284
  30. lemma OAI.CurrentProjection.prefixLaw_independence line 289
  31. def OAI.CurrentProjection.observationSignalMap line 304
  32. lemma OAI.CurrentProjection.measurable_observationSignalMap line 307
  33. def OAI.CurrentProjection.observationSignalLaw line 313
  34. instance OAI.CurrentProjection.observationSignalLaw_probability line 317
  35. lemma OAI.CurrentProjection.observationSignalLaw_context line 323
  36. def OAI.CurrentProjection.nextActualRowLaw line 331
  37. lemma OAI.CurrentProjection.measurable_nextActualRow line 336
  38. instance OAI.CurrentProjection.nextActualRowLaw_probability line 343
  39. lemma OAI.CurrentProjection.nextActualRowLaw_fst line 349
  40. lemma OAI.CurrentProjection.initialArray_snoc line 357
  41. lemma OAI.CurrentProjection.snoc_ownObservations line 364
  42. lemma OAI.CurrentProjection.nextActualRowLaw_single line 369
  43. def OAI.CurrentProjection.rawNextRowLaw line 391
  44. lemma OAI.CurrentProjection.measurable_rawNextRow line 396
  45. instance OAI.CurrentProjection.rawNextRowLaw_probability line 401
  46. lemma OAI.CurrentProjection.rawNextRowLaw_fst line 407
  47. lemma OAI.CurrentProjection.nextActualRowLaw_raw line 413
  48. lemma OAI.CurrentProjection.rowCharge_eq_raw line 419
  49. lemma OAI.CurrentProjection.prefix_rowInformation_step line 431