OAI/Combinatorics/Progressions/Estimates/FirstCoefficientDerivativeBounds.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialTensor_injective line 22
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedLogDerivative_mul line 35
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientDirectionMap_mul_rat line 48
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientDirectionMap_triple_rat line 59
  5. theorem OAI.Erdos3.realLinearMap_eq_of_rat_directions line 78
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientDirectionMap_mul line 101
  7. def OAI.Erdos3.NilpotentLieFiltration.FirstCoefficientSlowBound line 129
  8. def OAI.Erdos3.NilpotentLieFiltration.FirstCoefficientGrid line 134
  9. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientSlowBound_map line 138
  10. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGrid_map line 146
  11. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientSection line 173
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientSection_rightInverse line 180
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientSection_surviving_coordinate line 184
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientSection_coordinate_zero line 195
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientSection_coordinate line 215
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientSection_slow line 225
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientSection_grid line 236
  18. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedConstant line 265
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedConstant_mem_first line 269
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedConstant_tensor line 276
  21. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientConstant line 295
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientOfPolynomial_constant line 304
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientConstant_coordinate line 314
  24. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientConstant_slow line 325
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientConstant_grid line 337
  26. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientAdjoint_bound_of_polynomial_bound line 368
  27. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientAdjoint_grid_of_polynomial_grid line 384
  28. theorem OAI.Erdos3.NilpotentLieFiltration.exists_firstCoefficient_adjoint_bound line 396
  29. theorem OAI.Erdos3.NilpotentLieFiltration.exists_firstCoefficient_operation_grid line 423
  30. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientOfPolynomial_adjoint line 473
  31. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientOfPolynomial_adjoint_constant line 486
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientOfPolynomial_logDerivative line 497
  33. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientOfPolynomial_normalizedRelativeLog line 509
  34. theorem OAI.Erdos3.NilpotentLieFiltration.exists_firstCoefficient_coordinate_derivative_bound line 539