OAI/Combinatorics/Progressions/Estimates/FormalCurrentInputBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.projected_lift_residual_eq line 14
2. theorem OAI.Erdos3.projected_lift_array_homogeneous line 32
3. theorem OAI.Erdos3.projected_lift_array_bound line 48
4. theorem OAI.Erdos3.projected_lift_array_grid line 77
5. theorem OAI.Erdos3.liftQuotientArray_map_neg line 94
6. theorem OAI.Erdos3.projected_polynomial_coefficient_bound line 115
7. theorem OAI.Erdos3.projected_polynomial_coefficient_grid line 137
8. theorem OAI.Erdos3.uniform_current_layer_inputs_from_ambient line 148