OAI/Probability/Ballisticity/Stationary/ArrayClosed.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.closed_support_weak_limit line 13
  2. lemma OAI.DirectionalTransience.actualOccupation_ae_of_invariant line 26
  3. def OAI.DirectionalTransience.currentOffsets line 62
  4. lemma OAI.DirectionalTransience.currentOffsets_continuous line 66
  5. lemma OAI.DirectionalTransience.currentOffsets_closed line 71
  6. lemma OAI.DirectionalTransience.actual_currentOffsets line 77
  7. lemma OAI.DirectionalTransience.actualOccupation_currentOffsets line 95
  8. abbrev OAI.DirectionalTransience.AmbientCurrentWindow line 117
  9. instance OAI.DirectionalTransience.currentOffsets_secondCountable line 121
  10. instance OAI.DirectionalTransience.currentData_secondCountable line 123
  11. instance OAI.DirectionalTransience.currentProfiles_secondCountable line 126
  12. instance OAI.DirectionalTransience.currentFields_secondCountable line 128
  13. instance OAI.DirectionalTransience.ambientCurrentWindow_borel line 130
  14. instance OAI.DirectionalTransience.currentWindow_borel line 132
  15. def OAI.DirectionalTransience.currentWindowInclude line 135
  16. lemma OAI.DirectionalTransience.currentWindowInclude_continuous line 138
  17. lemma OAI.DirectionalTransience.currentWindowInclude_injective line 141
  18. def OAI.DirectionalTransience.currentArrayWindow line 149
  19. lemma OAI.DirectionalTransience.currentArrayWindow_continuous line 154
  20. lemma OAI.DirectionalTransience.currentArrayWindow_actual line 159
  21. lemma OAI.DirectionalTransience.currentArrayWindow_shift line 164
  22. lemma OAI.DirectionalTransience.currentArrayWindow_iterate line 168
  23. def OAI.DirectionalTransience.typedCurrentArrayWindow line 177
  24. lemma OAI.DirectionalTransience.typedCurrentArrayWindow_measurable line 183
  25. lemma OAI.DirectionalTransience.currentWindowInclude_typed line 199
  26. lemma OAI.DirectionalTransience.typedCurrentArrayWindow_actual line 204