OAI/Dynamics/StandardMap/Coding/ReconstructionEntropy.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.Entropy.rate_factor line 16
  2. lemma OAI.StandardMapEntropy.Entropy.rate_word_le line 31
  3. lemma OAI.StandardMapEntropy.Entropy.rate_word_eq line 56
  4. lemma OAI.StandardMapEntropy.Entropy.rate_integer_shift line 65
  5. lemma OAI.StandardMapEntropy.Entropy.rate_le_window_decoder line 80
  6. theorem OAI.StandardMapEntropy.Entropy.rate_lower_of_window_decoder line 97
  7. theorem OAI.StandardMapEntropy.Entropy.rate_lower_of_small_window_error line 112
  8. lemma OAI.HyperbolicCoding.word_centered_iterate line 137
  9. theorem OAI.HyperbolicCoding.marked_tower_decode_level line 147
  10. theorem OAI.HyperbolicCoding.marked_tower_decode_symbol line 161
  11. theorem OAI.HyperbolicCoding.marked_tower_decode_error_sum line 175
  12. theorem OAI.HyperbolicCoding.marked_tower_decode_error line 206
  13. def OAI.HyperbolicCoding.extendPrefixDecoder line 247
  14. theorem OAI.HyperbolicCoding.marked_tower_prefix_decoder_error line 251
  15. theorem OAI.HyperbolicCoding.MatrixCoupling.exists_decodable_coupling_scaled line 310
  16. def OAI.HyperbolicCoding.MatrixCoupling.decodingThreshold line 347
  17. lemma OAI.HyperbolicCoding.MatrixCoupling.decodingThreshold_pos line 350
  18. theorem OAI.HyperbolicCoding.MatrixCoupling.decodable_coupling_tolerance line 353
  19. theorem OAI.HyperbolicCoding.MatrixCoupling.exists_decodable_coupling_tolerance line 383