OAI/Dynamics/StandardMap/Coding/PartitionLimit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicCoding.exists_partition_limit line 13
  2. lemma OAI.HyperbolicCoding.measureReal_tendsto_zero_of_ae_eventually_notMem line 30
  3. lemma OAI.HyperbolicCoding.partition_limit_integer_names line 57
  4. lemma OAI.HyperbolicCoding.finite_code_error_tendsto_zero line 80
  5. lemma OAI.HyperbolicCoding.finite_box_law_tendsto line 97
  6. theorem OAI.HyperbolicCoding.iid_law_of_partition_limit line 132
  7. theorem OAI.HyperbolicCoding.measurable_decoder_of_ae_point_separation line 160
  8. theorem OAI.HyperbolicCoding.orbitName_shift_preserving line 188
  9. theorem OAI.HyperbolicCoding.measurable_decoder_of_conull_injective line 211
  10. theorem OAI.HyperbolicCoding.measurable_decoder_of_countable_factors line 237
  11. theorem OAI.HyperbolicCoding.measurable_decoder_of_generating_approximations line 252
  12. lemma OAI.HyperbolicCoding.decoder_error_tendsto line 275
  13. theorem OAI.HyperbolicCoding.approximate_decoders_pass_to_limit line 300
  14. theorem OAI.HyperbolicCoding.bernoulli_model_of_coherent_coding line 328