OAI/Probability/DirectionalWalk/Model.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalZeroOne.Site line 10

    Also declared: ComparatorChallenges/DirectionalWalk.lean:10 (same declaration text).

  2. abbrev OAI.DirectionalZeroOne.Step line 11

    Also declared: ComparatorChallenges/DirectionalWalk.lean:11 (same declaration text).

  3. def OAI.DirectionalZeroOne.stepVector line 13

    Also declared: ComparatorChallenges/DirectionalWalk.lean:13 (same declaration text).

  4. def OAI.DirectionalZeroOne.Row line 16

    Also declared: ComparatorChallenges/DirectionalWalk.lean:16 (same declaration text).

  5. instance OAI.DirectionalZeroOne.(instance at line 19) line 19
  6. abbrev OAI.DirectionalZeroOne.Environment line 23

    Also declared: ComparatorChallenges/DirectionalWalk.lean:23 (same declaration text).

  7. abbrev OAI.DirectionalZeroOne.Path line 24

    Also declared: ComparatorChallenges/DirectionalWalk.lean:24 (same declaration text).

  8. abbrev OAI.DirectionalZeroOne.State line 25

    Also declared: ComparatorChallenges/DirectionalWalk.lean:25 (same declaration text).

  9. def OAI.DirectionalZeroOne.StrictEllipticity line 27

    Also declared: ComparatorChallenges/DirectionalWalk.lean:27 (same declaration text).

  10. def OAI.DirectionalZeroOne.environmentLaw line 30

    Also declared: ComparatorChallenges/DirectionalWalk.lean:30 (same declaration text).

  11. def OAI.DirectionalZeroOne.transition line 34

    Also declared: ComparatorChallenges/DirectionalWalk.lean:34 (same declaration text).

  12. instance OAI.DirectionalZeroOne.(instance at line 51) line 51
  13. def OAI.DirectionalZeroOne.historyKernel line 64

    Also declared: ComparatorChallenges/DirectionalWalk.lean:64 (same declaration text).

  14. instance OAI.DirectionalZeroOne.(instance at line 69) line 69
  15. def OAI.DirectionalZeroOne.initialLaw line 73

    Also declared: ComparatorChallenges/DirectionalWalk.lean:73 (same declaration text).

  16. def OAI.DirectionalZeroOne.annealed line 77

    Also declared: ComparatorChallenges/DirectionalWalk.lean:77 (same declaration text).

  17. def OAI.DirectionalZeroOne.escape line 82

    Also declared: ComparatorChallenges/DirectionalWalk.lean:82 (same declaration text).

  18. lemma OAI.DirectionalZeroOne.probabilityMeasure_map line 85
  19. instance OAI.DirectionalZeroOne.(instance at line 90) line 90
  20. instance OAI.DirectionalZeroOne.(instance at line 95) line 95
  21. instance OAI.DirectionalZeroOne.(instance at line 100) line 100
  22. lemma OAI.DirectionalZeroOne.measurableSet_escape line 105
  23. lemma OAI.DirectionalZeroOne.all_rows_strictly_positive line 111
  24. abbrev OAI.DirectionalZeroOne.rowSigma line 120
  25. lemma OAI.DirectionalZeroOne.rowSigma_le line 123
  26. lemma OAI.DirectionalZeroOne.measurable_row line 126
  27. lemma OAI.DirectionalZeroOne.independent_rowSigma line 130
  28. def OAI.DirectionalZeroOne.quenchedWeight line 136
  29. def OAI.DirectionalZeroOne.wordWeight line 139
  30. lemma OAI.DirectionalZeroOne.measurable_quenchedWeight_on_rows line 143
  31. lemma OAI.DirectionalZeroOne.measurable_quenchedWeight line 152
  32. lemma OAI.DirectionalZeroOne.departure_transfer line 156
  33. lemma OAI.DirectionalZeroOne.quenchedWeight_le_one line 166
  34. lemma OAI.DirectionalZeroOne.wordWeight_le_one line 172
  35. lemma OAI.DirectionalZeroOne.wordWeight_pos line 176
  36. def OAI.DirectionalZeroOne.meanStep line 190
  37. lemma OAI.DirectionalZeroOne.meanStep_pos line 193
  38. lemma OAI.DirectionalZeroOne.meanStep_le_one line 203
  39. lemma OAI.DirectionalZeroOne.meanStep_at_site line 208
  40. lemma OAI.DirectionalZeroOne.fresh_word_weight line 216