OAI/Combinatorics/Progressions/Polynomial/PolynomialDerivativeDifferences.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_adapted_dual_grid line 12
2. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedAdjoint_tensor line 74
3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_polynomial_dual_grid line 84
4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_formal_polynomial_operation_grid line 159
5. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_add_sub line 224
6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_rational_derivative_correction_grid line 252
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_polynomial_log_derivative_bound line 291
8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_polynomial_adjoint_bound line 326
9. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_add_sub line 377
10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_slow_derivative_correction_bound line 394
11. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_sub line 470
12. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_sub line 481
13. theorem OAI.Erdos3.NilpotentLieFiltration.polynomial_common_derivative_difference line 500