OAI/Dynamics/StandardMap/Coding/FixedWindowTower.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicCoding.blockWindow_word line 12
2. lemma OAI.HyperbolicCoding.integrable_wordCost line 20
3. lemma OAI.HyperbolicCoding.fixedWindowCost_scale line 30
4. theorem OAI.HyperbolicCoding.fixed_window_tower_bounds line 44
5. theorem OAI.HyperbolicCoding.actual_fixed_window_copy line 105
6. theorem OAI.HyperbolicCoding.actual_fixed_window_rate_copy line 224
7. theorem OAI.HyperbolicCoding.fixed_decoder_arbitrary_tests line 273
8. lemma OAI.HyperbolicCoding.disagreement_triangle line 340
9. lemma OAI.HyperbolicCoding.disagreement_symm line 350
10. lemma OAI.HyperbolicCoding.sequence_distance_le_sum line 358
11. lemma OAI.HyperbolicCoding.partition_limit_distance_bound line 367
12. lemma OAI.HyperbolicCoding.finite_decoder_perturbation line 383
13. theorem OAI.HyperbolicCoding.seeded_exact_iid_limit line 408