OAI/Dynamics/StandardMap/Towers/ScaledFiniteCoupling.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.mass_smul_measure line 15
  2. lemma OAI.HyperbolicCoding.normalize_mass_cancel line 20
  3. def OAI.HyperbolicCoding.MatrixCoupling.scale line 28
  4. lemma OAI.HyperbolicCoding.MatrixCoupling.scale_cost line 34
  5. lemma OAI.HyperbolicCoding.MatrixCoupling.cost_nonneg line 37
  6. lemma OAI.HyperbolicCoding.MatrixCoupling.cost_mul line 40
  7. lemma OAI.HyperbolicCoding.nameCost_nonneg line 52
  8. lemma OAI.HyperbolicCoding.nameCost_le_symbolCost line 54
  9. lemma OAI.HyperbolicCoding.normalized_restriction_probability line 75
  10. theorem OAI.HyperbolicCoding.lift_ambient_word_transport line 81
  11. lemma OAI.HyperbolicCoding.base_mass_to_law line 140
  12. def OAI.HyperbolicCoding.wordWindow line 154
  13. lemma OAI.HyperbolicCoding.wordWindow_word line 159
  14. lemma OAI.HyperbolicCoding.tower_interior_level_law line 165
  15. lemma OAI.HyperbolicCoding.tower_interior_law line 191
  16. theorem OAI.HyperbolicCoding.tower_short_word_lawClose line 224
  17. theorem OAI.HyperbolicCoding.dynamical_word_copy line 291
  18. theorem OAI.HyperbolicCoding.weakBernoulli_dynamical_copy line 319