OAI/Combinatorics/Progressions/Estimates/NativeOrbitFreezing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.complex_expect_error_le line 14
2. theorem OAI.Erdos3.complex_discrepancy_after_freezing line 24
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.polynomialRationalGrid_uniform_cosets line 47
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_rational_period line 64
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_slow_factor_freezing line 105
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_anchored_factor_freezing line 152
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_auxiliary_frozen_discrepancy line 236
8. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitCoordinates_realValue line 342
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_orbit_rational_period line 357
10. theorem OAI.Erdos3.exists_native_orbit_local_control line 393
11. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_orbit_factor_freezing line 457