OAI/Dynamics/EntropyCounterexample/EntropyLocalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem340.ereal_le_of_sparse_block_bounds line 12
  2. lemma OAI.Problem340.IsDynCoverOf.entropy_le_real_log_card_div line 32
  3. lemma OAI.Problem340.log_sparse_word_bound line 45
  4. theorem OAI.Problem340.coverEntropyEntourage_le_of_sparse_block_covers line 70
  5. lemma OAI.Problem340.exists_small_log_dynCover_of_zero_entropy line 99
  6. theorem OAI.Problem340.entropy_le_of_neighborhood_attracting_dynCover line 138
  7. theorem OAI.Problem340.coverEntropy_eq_zero_of_neighborhood_attraction line 181
  8. theorem OAI.Problem340.entropy_le_of_attracting_dynCover line 211
  9. theorem OAI.Problem340.coverEntropy_eq_zero_of_pointwise_attraction line 225