OAI/Combinatorics/Progressions/Polynomial/ScaledPolynomialDualBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialConstantHom line 15
  2. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialConstantHom_coord line 19
  3. theorem OAI.Erdos3.NilpotentLieFiltration.polynomial_factor_middle_constant line 25
  4. def OAI.Erdos3.NilpotentLieFiltration.adaptedConstantLieHom line 55
  5. def OAI.Erdos3.NilpotentLieFiltration.adaptedConstantGroupHom line 68
  6. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedConstantGroupHom_log line 71
  7. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialConstantHom_constant line 74
  8. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolHom_constant line 80
  9. theorem OAI.Erdos3.NilpotentLieFiltration.exists_constant_normalized_polynomial line 85
  10. def OAI.Erdos3.NilpotentLieFiltration.PolynomialRationalGrid line 117
  11. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_of_dvd line 121
  12. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_constant line 126
  13. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_groupHom_iff line 143
  14. def OAI.Erdos3.NilpotentLieFiltration.PolynomialSlowBound line 187
  15. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_inv_iff line 192
  16. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_mono line 199
  17. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_constant line 205
  18. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_groupHom_iff line 218
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realAdapted_factor_middle_constant line 252
  20. theorem OAI.Erdos3.NilpotentLieFiltration.exists_polynomial_rational_product_bound line 276
  21. theorem OAI.Erdos3.NilpotentLieFiltration.linearPolynomial_adapted line 344
  22. def OAI.Erdos3.NilpotentLieFiltration.linearPolynomialGroup line 354
  23. theorem OAI.Erdos3.NilpotentLieFiltration.linearPolynomialGroup_log line 358
  24. theorem OAI.Erdos3.NilpotentLieFiltration.stepOne_lie_eq_zero line 361
  25. theorem OAI.Erdos3.NilpotentLieFiltration.stepOne_coord_mul line 367
  26. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSlowBound_linear line 371
  27. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialRationalGrid_linear line 386
  28. theorem OAI.Erdos3.NilpotentLieFiltration.exists_polynomial_slow_product_bound line 418
  29. def OAI.Erdos3.NilpotentLieFiltration.affinePolynomialOrbit line 498
  30. theorem OAI.Erdos3.NilpotentLieFiltration.affinePolynomialOrbit_log line 506
  31. theorem OAI.Erdos3.NilpotentLieFiltration.affinePolynomialOrbit_real_coord line 511
  32. theorem OAI.Erdos3.NilpotentLieFiltration.affinePolynomialOrbit_integer_coord line 517
  33. def OAI.Erdos3.NilpotentLieFiltration.RealAdaptedCoefficientBound line 538
  34. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedCoefficientBound_mono line 543
  35. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedCoefficientBound_scaled_iff line 550
  36. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedCoefficientBound_polynomial_iff line 556
  37. theorem OAI.Erdos3.NilpotentLieFiltration.exists_scaled_polynomial_dual_bound line 562