OAI/Combinatorics/Progressions/Estimates/HigherResidualRowDifferences.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_unit_row_model_with_differences line 18
2. theorem OAI.Erdos3.dense_set_mean_lower_bound line 94
3. theorem OAI.Erdos3.exists_quadratic_primitive_correlation_large_modulus line 116
4. theorem OAI.Erdos3.exists_cyclicNativeInverse_two line 284
5. theorem OAI.Erdos3.exists_unit_row_family_with_differences line 318
6. theorem OAI.Erdos3.exists_native_mixed_from_inverse line 430
7. theorem OAI.Erdos3.exists_cubic_native_mixed_correlation line 452
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_residual_row_differences_degree line 470