OAI/Dynamics/MultipleMixing/WeakLimits.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Rokhlin.ArrayObjects.initial_correlation_zero line 29
2. def OAI.Rokhlin.ArrayObjects.firstDuplicate line 54
3. lemma OAI.Rokhlin.ArrayObjects.continuous_firstDuplicate line 57
4. lemma OAI.Rokhlin.ArrayObjects.continuous_array_amap line 61
5. lemma OAI.Rokhlin.ArrayObjects.continuous_array_plane line 65
6. lemma OAI.Rokhlin.ArrayObjects.continuous_array_planes line 68
7. lemma OAI.Rokhlin.ArrayObjects.amap_iterate line 72
8. lemma OAI.Rokhlin.ArrayObjects.plane_firstDuplicate_zero line 79
9. lemma OAI.Rokhlin.ArrayObjects.plane_firstDuplicate_succ line 84
10. lemma OAI.Rokhlin.ArrayObjects.planes_firstDuplicate_succ line 97
11. def OAI.Rokhlin.ArrayObjects.continuousPush line 108
12. lemma OAI.Rokhlin.ArrayObjects.continuous_continuousPush line 111
13. lemma OAI.Rokhlin.ArrayObjects.continuousPush_comp line 113
14. lemma OAI.Rokhlin.ArrayObjects.continuousPush_id line 118
15. lemma OAI.Rokhlin.ArrayObjects.continuousPush_pi line 122
16. def OAI.Rokhlin.ArrayObjects.weakArrayLaw line 135
17. lemma OAI.Rokhlin.ArrayObjects.weakArrayLaw_tendsto line 141
18. lemma OAI.Rokhlin.ArrayObjects.firstDuplicate_amap line 149
19. lemma OAI.Rokhlin.ArrayObjects.weakArrayLaw_invariant line 154
20. lemma OAI.Rokhlin.ArrayObjects.weakArrayLaw_iterate_invariant line 177
21. lemma OAI.Rokhlin.ArrayObjects.weakArrayLaw_consistent line 188
22. lemma OAI.Rokhlin.ArrayObjects.weakArrayLaw_proper line 228
23. lemma OAI.Rokhlin.probability_pi_tendsto_of_rectangles line 268
24. lemma OAI.Rokhlin.ArrayObjects.weakArrayLaw_proper_input line 300
25. def OAI.Rokhlin.ArrayObjects.weakInitialLaws line 356
26. lemma OAI.Rokhlin.ArrayObjects.weakInitialLaws_zero line 365
27. lemma OAI.Rokhlin.ArrayObjects.weakInitialLaws_correlation line 370
28. lemma OAI.Rokhlin.ArrayObjects.compact_zero_entropy_no_witness line 391