OAI/Combinatorics/Progressions/Estimates/UniformFrozenDescent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.topQuotientModel line 16
2. theorem OAI.Erdos3.NilpotentLieFiltration.topQuotientModel_geometry line 24
3. theorem OAI.Erdos3.NilpotentLieFiltration.topQuotientModel_filtration line 36
4. theorem OAI.Erdos3.NilpotentLieFiltration.topQuotientModel_lattice line 41
5. theorem OAI.Erdos3.NilpotentLieFiltration.quotientFinBasis_repr_mk line 57
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_top_quotient line 72
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_reduced_square_geometry line 129
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_top_subspace_quotient line 165
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_topQuotientOtherTarget line 239
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.topQuotientOtherMap_real_kernel line 283
11. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_constructed_fixedObservable_topInvariant_descent line 305
12. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_frozen_descent line 389