OAI/Combinatorics/Progressions/Estimates/NativeIteratedDifferencing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.mean_row_correlation_sq_le_derivative_correlation line 12
2. theorem OAI.Erdos3.mean_row_correlation_sq_le_approximated_derivatives line 41
3. theorem OAI.Erdos3.mean_mul_error_le_separate line 75
4. theorem OAI.Erdos3.mean_row_correlation_sq_le_product_derivatives line 95
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_cyclic_second_difference_models_degree line 129
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_differenced_rows_degree line 185
7. theorem OAI.Erdos3.exists_differenced_scalar_expansions line 272
8. theorem OAI.Erdos3.exists_many_native_derivative_correlations line 374
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_univariate_cyclic_difference_models line 465
10. theorem OAI.Erdos3.exists_iterated_native_derivative_correlations line 511