OAI/Dynamics/StandardMap/Coding/SanitizedTowerLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicCoding.sanitized_tower_short_word_lawClose line 14
2. lemma OAI.HyperbolicCoding.marked_tower_short_word_lawClose line 51
3. lemma OAI.HyperbolicCoding.marked_pushWeight_support line 85
4. theorem OAI.HyperbolicCoding.actual_synchronized_copy line 96
5. theorem OAI.HyperbolicCoding.actual_rate_controlled_copy line 167
6. lemma OAI.HyperbolicCoding.normalizedPrefixCost_modify line 217
7. lemma OAI.HyperbolicCoding.prefixNameCost_word_factor line 224
8. theorem OAI.HyperbolicCoding.lift_prefix_transport line 228
9. theorem OAI.HyperbolicCoding.entropy_controlled_copy_tests line 261
10. structure OAI.HyperbolicCoding.IIDCopyTest line 325
11. lemma OAI.HyperbolicCoding.exists_iidCopyTest line 338
12. theorem OAI.HyperbolicCoding.IIDCopyTest.copy line 350
13. def OAI.HyperbolicCoding.MatrixCoupling.independent line 392
14. theorem OAI.HyperbolicCoding.initial_rate_controlled_copy line 400