OAI/Combinatorics/Progressions/Estimates/UniformFormalCurrentLayerStep.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.controlled_zero_sum_separation line 15
2. theorem OAI.Erdos3.current_derivative_polynomials_separate line 26
3. theorem OAI.Erdos3.current_derivative_terms_vanish_of_invariant_polynomial line 57
4. theorem OAI.Erdos3.eval₂_lie_mem_of_coefficients line 97
5. theorem OAI.Erdos3.NilpotentLieFiltration.formal_current_layer_derivative_equation line 113
6. theorem OAI.Erdos3.NilpotentLieFiltration.formal_current_layer_derivative_equation_mod line 170
7. theorem OAI.Erdos3.NilpotentLieFiltration.formal_current_layer_correction_preserves_lifts_mod line 206
8. theorem OAI.Erdos3.VectorPolynomial.homogeneous_pderiv_coordinate_bound line 248
9. theorem OAI.Erdos3.VectorPolynomial.pderiv_coordinate_grid line 274
10. theorem OAI.Erdos3.NilpotentLieFiltration.formal_correction_sub_mem_layer line 302
11. theorem OAI.Erdos3.NilpotentLieFiltration.formal_correction_preserves_bracket_remainder line 313
12. theorem OAI.Erdos3.NilpotentLieFiltration.formal_correction_preserves_projected_log line 331
13. theorem OAI.Erdos3.NilpotentLieFiltration.formal_correction_advances_log_conditions line 345
14. theorem OAI.Erdos3.NilpotentLieFiltration.formal_correction_preserves_horizontal_extra line 378
15. theorem OAI.Erdos3.NilpotentLieFiltration.current_correction_derivative_terms_vanish line 420
16. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_formal_current_layer_step line 508
17. theorem OAI.Erdos3.NilpotentLieFiltration.exists_uniform_formal_current_layer_step line 717