OAI/Dynamics/EntropyCounterexample/ImageEntropy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.dynCover_prefix_product line 12
  2. theorem OAI.Problem340.coverMincard_le_initial_card_mul_image line 58
  3. theorem OAI.Problem340.coverEntropyEntourage_le_image_of_initial_cover line 80
  4. theorem OAI.Problem340.coverEntropy_le_image_of_isCompact line 92
  5. theorem OAI.Problem340.coverEntropy_univ_eq_range line 107
  6. theorem OAI.Problem340.coverEntropy_univ_eq_zero_of_image_subset line 116
  7. theorem OAI.Problem340.coverEntropy_univ_eq_zero_of_first_image_factor line 127