OAI/Probability/Ballisticity/Entropy/StoppedWindowEntropy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.StoppedWindow.ownLowerReference line 16
  2. theorem OAI.DirectionalTransience.StoppedWindow.stopped_chain line 19
  3. theorem OAI.DirectionalTransience.StoppedWindow.stopped_kernel_increment line 28
  4. theorem OAI.DirectionalTransience.StoppedWindow.fresh_prod_chain line 38
  5. theorem OAI.DirectionalTransience.StoppedWindow.same_auxiliary_cost line 47
  6. def OAI.DirectionalTransience.stoppedWindowOutput line 62
  7. lemma OAI.DirectionalTransience.stoppedWindowOutput_measurable line 70
  8. lemma OAI.DirectionalTransience.stoppedWindowOutput_factor line 81
  9. def OAI.DirectionalTransience.stoppedWindowLaw line 99
  10. lemma OAI.DirectionalTransience.stoppedWindowLaw_upper_observation line 103
  11. lemma OAI.DirectionalTransience.stoppedWindowLaw_fst line 121
  12. lemma OAI.DirectionalTransience.stoppedWindowLaw_reference line 140
  13. theorem OAI.DirectionalTransience.actual_stopped_window_entropy_increment line 154