OAI/Probability/Ballisticity/Stationary/StationaryCompact.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectionalTransience.StationaryCompact.invariant_of_weak_limit line 16
  2. theorem OAI.DirectionalTransience.StationaryCompact.exists_invariant_subsequence line 42
  3. lemma OAI.DirectionalTransience.StationaryCompact.episode_telescope line 58
  4. lemma OAI.DirectionalTransience.StationaryCompact.episode_boundary_bound line 66
  5. def OAI.DirectionalTransience.StationaryCompact.episodeOccupationRaw line 89
  6. instance OAI.DirectionalTransience.StationaryCompact.episodeOccupationRaw_finite line 93
  7. lemma OAI.DirectionalTransience.StationaryCompact.sum_indicator_range line 99
  8. lemma OAI.DirectionalTransience.StationaryCompact.episodeOccupationRaw_integral line 107
  9. lemma OAI.DirectionalTransience.StationaryCompact.episodeOccupationRaw_mass line 140
  10. def OAI.DirectionalTransience.StationaryCompact.episodeOccupation line 147
  11. lemma OAI.DirectionalTransience.StationaryCompact.episodeOccupation_integral line 151
  12. lemma OAI.DirectionalTransience.StationaryCompact.episode_sum_integrable line 174
  13. lemma OAI.DirectionalTransience.StationaryCompact.episodeOccupation_defect line 192
  14. theorem OAI.DirectionalTransience.StationaryCompact.episodeOccupation_stationary_limit line 217