OAI/Dynamics/StandardMap/Coupling/AtomlessFinitePartition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicCoding.exists_disjoint_cuts line 14
  2. lemma OAI.HyperbolicCoding.exists_measurable_coloring line 60
  3. theorem OAI.HyperbolicCoding.exists_finite_random_variable line 89
  4. theorem OAI.HyperbolicCoding.realize_finite_coupling line 144
  5. lemma OAI.HyperbolicCoding.repaint_error_eq_sum line 166
  6. theorem OAI.HyperbolicCoding.copy_finite_law line 183
  7. lemma OAI.StandardMapEntropy.Entropy.mass_triple_first_third line 219
  8. lemma OAI.StandardMapEntropy.Entropy.mass_triple_second_third line 233
  9. theorem OAI.HyperbolicCoding.copy_independent_of_finite_past line 257
  10. def OAI.HyperbolicCoding.symbolCost line 336
  11. lemma OAI.HyperbolicCoding.symbolCost_self line 340
  12. lemma OAI.HyperbolicCoding.symbolCost_nonneg line 341
  13. lemma OAI.HyperbolicCoding.symbolCost_triangle line 342
  14. def OAI.HyperbolicCoding.MatrixCoupling.reindex line 349
  15. lemma OAI.HyperbolicCoding.MatrixCoupling.reindex_cost line 356
  16. def OAI.HyperbolicCoding.nameCost line 365
  17. lemma OAI.HyperbolicCoding.nameCost_self line 368
  18. lemma OAI.HyperbolicCoding.nameCost_triangle line 370
  19. lemma OAI.HyperbolicCoding.nameCost_cons line 374
  20. theorem OAI.HyperbolicCoding.coupling_step line 384