OAI/Combinatorics/EuclideanRamsey/OrbitAveraging.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.EuclideanRamsey.OrbitWords line 32
2. lemma OAI.EuclideanRamsey.OrbitWords.reindex line 38
3. lemma OAI.EuclideanRamsey.OrbitWords.normalize line 44
4. lemma OAI.EuclideanRamsey.OrbitWords.average line 47
5. def OAI.EuclideanRamsey.OrbitIn line 58
6. def OAI.EuclideanRamsey.OrbitBound line 61
7. lemma OAI.EuclideanRamsey.orbitIn_normalize line 65
8. lemma OAI.EuclideanRamsey.orbitIn_average line 70
9. lemma OAI.EuclideanRamsey.orbitBound_normalize line 77
10. lemma OAI.EuclideanRamsey.orbitBound_average line 84
11. lemma OAI.EuclideanRamsey.orbitIn_raise line 97
12. lemma OAI.EuclideanRamsey.contraction_bound line 106
13. inductive OAI.EuclideanRamsey.Evolution line 145
14. lemma OAI.EuclideanRamsey.Evolution.trans line 153
15. lemma OAI.EuclideanRamsey.Evolution.words line 159
16. lemma OAI.EuclideanRamsey.Evolution.positive line 165
17. lemma OAI.EuclideanRamsey.Evolution.orbitIn line 170
18. lemma OAI.EuclideanRamsey.Evolution.orbitBound line 176
19. lemma OAI.EuclideanRamsey.evolve_finite line 186
20. lemma OAI.EuclideanRamsey.orbit_raise_depth line 206
21. lemma OAI.EuclideanRamsey.all_orbits_derived line 215
22. lemma OAI.EuclideanRamsey.contraction_iterate line 224
23. lemma OAI.EuclideanRamsey.contraction_rate line 242
24. lemma OAI.EuclideanRamsey.orbit_make_small line 266
25. theorem OAI.EuclideanRamsey.finite_group_averaging line 289