OAI/Probability/Ballisticity/Stationary/EpisodeInjection.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.BoundedInjection.injectionMultiplier line 14
  2. lemma OAI.DirectionalTransience.BoundedInjection.injectionMultiplier_lt line 16
  3. def OAI.DirectionalTransience.BoundedInjection.injectionChoice line 22
  4. def OAI.DirectionalTransience.BoundedInjection.injectionOffset line 27
  5. def OAI.DirectionalTransience.BoundedInjection.injectTuple line 31
  6. lemma OAI.DirectionalTransience.BoundedInjection.injectionOffset_le line 35
  7. lemma OAI.DirectionalTransience.BoundedInjection.injectTuple_separated line 39
  8. lemma OAI.DirectionalTransience.BoundedInjection.injectTuple_height line 48
  9. lemma OAI.DirectionalTransience.BoundedInjection.injectTuple_kernel_le line 59
  10. def OAI.DirectionalTransience.BoundedInjection.injectionProfile line 91
  11. lemma OAI.DirectionalTransience.BoundedInjection.injectionProfile_measurable line 100
  12. lemma OAI.DirectionalTransience.BoundedInjection.injectionProfile_retained line 104
  13. def OAI.DirectionalTransience.episodeInitial line 134
  14. lemma OAI.DirectionalTransience.episodeInitial_retained line 142
  15. def OAI.DirectionalTransience.episodeFinal line 155
  16. lemma OAI.DirectionalTransience.episodeFinal_gt line 161
  17. lemma OAI.DirectionalTransience.episodeFinal_le line 168
  18. def OAI.DirectionalTransience.episodeBoundary line 174
  19. lemma OAI.DirectionalTransience.episodeBoundary_le line 181
  20. lemma OAI.DirectionalTransience.episodeBoundary_progress line 192
  21. theorem OAI.DirectionalTransience.episodeBoundary_complete line 206