OAI/Probability/Ballisticity/Stationary/StationaryWindowEntropy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.typedCurrentArrayWindow_shift line 15
  2. lemma OAI.DirectionalTransience.stationary_currentWindow_law line 19
  3. theorem OAI.DirectionalTransience.OperationalConstants.stationary_window_entropy line 44
  4. lemma OAI.DirectionalTransience.actualOccupation_ae_of_ae_invariant line 72
  5. def OAI.DirectionalTransience.ArrayElliptic line 109
  6. lemma OAI.DirectionalTransience.arrayElliptic_closed line 112
  7. lemma OAI.DirectionalTransience.arrayElliptic_shift line 121
  8. lemma OAI.DirectionalTransience.auxiliary_rows line 127
  9. lemma OAI.DirectionalTransience.actualArrayMap_elliptic_ae line 140
  10. lemma OAI.DirectionalTransience.actualOccupation_elliptic line 168