OAI/Probability/DirectionalWalk/CylinderLaw.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.walkInitialLaw line 10
  2. instance OAI.DirectionalZeroOne.(instance at line 13) line 13
  3. def OAI.DirectionalZeroOne.walkStateLaw line 18
  4. instance OAI.DirectionalZeroOne.(instance at line 22) line 22
  5. lemma OAI.DirectionalZeroOne.lintegral_transition line 27
  6. lemma OAI.DirectionalZeroOne.walkStateLaw_initial_history line 36
  7. lemma OAI.DirectionalZeroOne.walkStateLaw_initial line 43
  8. lemma OAI.DirectionalZeroOne.walkStateLaw_one_step line 52
  9. def OAI.DirectionalZeroOne.entryWeight line 68
  10. lemma OAI.DirectionalZeroOne.measurable_entryWeight line 71
  11. def OAI.DirectionalZeroOne.prefixMatches line 80
  12. def OAI.DirectionalZeroOne.prefixObservable line 83
  13. lemma OAI.DirectionalZeroOne.measurableSet_prefixMatches line 88
  14. lemma OAI.DirectionalZeroOne.measurable_prefixObservable line 94
  15. lemma OAI.DirectionalZeroOne.prefixMatches_succ line 100
  16. def OAI.DirectionalZeroOne.pathWeight line 111
  17. lemma OAI.DirectionalZeroOne.measurable_pathWeight line 115
  18. lemma OAI.DirectionalZeroOne.pathWeight_succ line 119
  19. lemma OAI.DirectionalZeroOne.history_matches_iff line 123
  20. lemma OAI.DirectionalZeroOne.prefix_lintegral_succ line 131
  21. lemma OAI.DirectionalZeroOne.prefix_lintegral_zero line 178
  22. lemma OAI.DirectionalZeroOne.prefix_lintegral line 194
  23. def OAI.DirectionalZeroOne.stateLaw line 207
  24. lemma OAI.DirectionalZeroOne.annealed_eq_map_stateLaw line 210
  25. def OAI.DirectionalZeroOne.walkLaw line 213
  26. instance OAI.DirectionalZeroOne.(instance at line 216) line 216
  27. def OAI.DirectionalZeroOne.pathCylinder line 221
  28. lemma OAI.DirectionalZeroOne.measurableSet_pathCylinder line 224
  29. lemma OAI.DirectionalZeroOne.walkLaw_cylinder line 230
  30. lemma OAI.DirectionalZeroOne.annealed_cylinder line 249
  31. lemma OAI.DirectionalZeroOne.stepVector_injective line 255
  32. lemma OAI.DirectionalZeroOne.entryWeight_step line 265
  33. def OAI.DirectionalZeroOne.quenchedKernel line 269
  34. instance OAI.DirectionalZeroOne.(instance at line 274) line 274
  35. lemma OAI.DirectionalZeroOne.walkLaw_apply line 279
  36. lemma OAI.DirectionalZeroOne.walkLaw_dirac line 301
  37. lemma OAI.DirectionalZeroOne.annealed_apply line 307
  38. lemma OAI.DirectionalZeroOne.quenchedKernel_cylinder line 312
  39. lemma OAI.DirectionalZeroOne.measure_eq_of_prefix line 318
  40. lemma OAI.DirectionalZeroOne.pathMeasure_ext line 335