OAI/Probability/Ballisticity/Stationary/ArrayPermutation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.labelPerm line 15
  2. def OAI.DirectionalTransience.arrayPerm line 18
  3. lemma OAI.DirectionalTransience.arrayPerm_continuous line 24
  4. lemma OAI.DirectionalTransience.arrayPerm_shift line 27
  5. lemma OAI.DirectionalTransience.arrayPerm_iterate line 31
  6. def OAI.DirectionalTransience.anchorsPerm line 38
  7. lemma OAI.DirectionalTransience.anchorsPerm_measurable line 40
  8. def OAI.DirectionalTransience.inputPerm line 43
  9. lemma OAI.DirectionalTransience.inputPerm_measurable line 45
  10. lemma OAI.DirectionalTransience.arrayPerm_actual line 50
  11. lemma OAI.DirectionalTransience.anchorLaw_perm line 54
  12. lemma OAI.DirectionalTransience.inputLaw_perm line 65
  13. lemma OAI.DirectionalTransience.occupation_perm_integral line 81
  14. lemma OAI.DirectionalTransience.OperationalConstants.bad_limit_perm line 111