OAI/Dynamics/StandardMap/Coupling/ActualFiniteRecodingBounds.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.observations_vector_cost line 15
  2. lemma OAI.HyperbolicCoding.recodingLaw_entropy_lower line 26
  3. lemma OAI.HyperbolicCoding.recodingLaw_transport_cost line 55
  4. def OAI.HyperbolicCoding.nestedPack line 96
  5. lemma OAI.HyperbolicCoding.nestedPack_symm line 99
  6. lemma OAI.HyperbolicCoding.nestedPack_word line 104
  7. lemma OAI.HyperbolicCoding.obs_nestedPack_word line 116
  8. lemma OAI.HyperbolicCoding.obs_nestedOutput line 125
  9. def OAI.HyperbolicCoding.fineWordCost line 132
  10. lemma OAI.HyperbolicCoding.fineWordCost_sum line 135
  11. lemma OAI.HyperbolicCoding.nameCost_nestedPack line 140
  12. lemma OAI.HyperbolicCoding.observations_word_cost line 147
  13. lemma OAI.HyperbolicCoding.observations_fineWordCost line 170
  14. lemma OAI.HyperbolicCoding.fineWordCost_abs_le line 188
  15. lemma OAI.HyperbolicCoding.obs_word_rate_lower line 195
  16. lemma OAI.HyperbolicCoding.recoding_entropy_scalar line 210
  17. lemma OAI.HyperbolicCoding.recoding_deficit_scalar line 220
  18. lemma OAI.HyperbolicCoding.recoding_wb_cost_scalar line 227
  19. lemma OAI.HyperbolicCoding.nestedOutput_word line 251
  20. lemma OAI.HyperbolicCoding.recoding_nested_entropy line 258
  21. lemma OAI.HyperbolicCoding.nested_reindex_transport line 279
  22. lemma OAI.HyperbolicCoding.recoding_nested_transport line 305
  23. lemma OAI.HyperbolicCoding.block_recoding_small_cost line 323
  24. lemma OAI.HyperbolicCoding.WeakBernoulliProcess.factor line 371
  25. theorem OAI.HyperbolicCoding.separating_wb_approximation line 389
  26. lemma OAI.HyperbolicCoding.finite_observation_entropy_test_uniform line 411
  27. theorem OAI.HyperbolicCoding.weakBernoulli_limit_finite_determination line 422