OAI/Dynamics/StandardMap/Coupling/ChunkNameCost.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.symbolCost_le_one line 11
  2. lemma OAI.HyperbolicCoding.nameCost_le_card line 14
  3. lemma OAI.HyperbolicCoding.nameCost_le_chunkCost line 18
  4. theorem OAI.HyperbolicCoding.nameCost_le_retained_chunks line 25
  5. lemma OAI.HyperbolicCoding.MatrixCoupling.cost_mono line 68
  6. lemma OAI.HyperbolicCoding.MatrixCoupling.cost_affine line 72
  7. theorem OAI.HyperbolicCoding.lift_observation_transport line 91
  8. theorem OAI.HyperbolicCoding.full_word_transport line 123
  9. lemma OAI.HyperbolicCoding.finite_remote_lawClose line 183
  10. theorem OAI.HyperbolicCoding.weakBernoulli_finite_copy line 203
  11. theorem OAI.HyperbolicCoding.weakBernoulli_forward_blocks line 233
  12. lemma OAI.StandardMapEntropy.Entropy.continuous_shannon line 278
  13. theorem OAI.StandardMapEntropy.Entropy.finite_entropy_continuity line 282
  14. lemma OAI.StandardMapEntropy.Entropy.obs_eq_entropy_map line 295
  15. theorem OAI.StandardMapEntropy.Entropy.obs_continuity_in_law line 302
  16. lemma OAI.StandardMapEntropy.Entropy.cond_factor_chain line 326
  17. theorem OAI.StandardMapEntropy.Entropy.conditional_defect_data_processing line 337
  18. def OAI.HyperbolicCoding.relativeInformation line 359
  19. lemma OAI.HyperbolicCoding.log_ratio_hellinger_bound line 362
  20. theorem OAI.HyperbolicCoding.finite_pinsker_sq line 385