OAI/Combinatorics/Progressions/Estimates/UniformFiniteMarkedFactorParameters.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.MarkedRationalFactorFreezing line 16
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_marked_rational_factor_freezing_bound line 44
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_marked_rational_factor_freezing line 145
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.MarkedRationalFactorFreezing.finite_enumeration line 187
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.MarkedRationalFactorFreezing.mono line 245
6. def OAI.Erdos3.RationalFilteredNilmanifold.MarkedSlowFactorFreezing line 273
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_marked_factor_parameters line 305
8. def OAI.Erdos3.RationalFilteredNilmanifold.FiniteMarkedRationalFactorFreezing line 398
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.MarkedSlowFactorFreezing.mono_bound line 428
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_finite_marked_factor_parameters line 445