OAI/Combinatorics/Progressions/Polynomial/ControlledPositivePolynomialDownsets.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.positivePolynomialInputBudget line 10
  2. def OAI.Erdos3.positivePolynomialDenominatorBudget line 13
  3. def OAI.Erdos3.positivePolynomialModelBudget line 16
  4. theorem OAI.Erdos3.positivePolynomialInputBudget_nonneg line 21
  5. theorem OAI.Erdos3.squarefreeInputBudget_le_positive line 25
  6. theorem OAI.Erdos3.positivePolynomialInputBudget_le_denominator line 29
  7. theorem OAI.Erdos3.positivePolynomialDenominatorBudget_le_model line 33
  8. theorem OAI.Erdos3.exists_positivePolynomialModel_budget line 39
  9. abbrev OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.PositivePolynomialBasisIndex line 70
  10. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialBasis line 73
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialBasisIndex_card_le line 77
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positiveCoefficientBasis_card_le line 85
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialBasis_structure_height line 92
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialBasis_evaluation_height line 104
  15. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialFinBasis line 114
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialFinBasis_structure_height line 118
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialFinBasis_evaluation_height line 124
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialFinBasis_multidegree_height line 130
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialFinBasis_degree_height line 136
  20. abbrev OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.PositivePolynomialDownsetIndex line 157
  21. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetBasis line 160
  22. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetFinBasis line 166
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetIndex_card_le line 172
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetBasis_structure line 177
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetFinBasis_multidegree_height line 183
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetFinBasis_degree_height line 190
  27. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.PositivePolynomialGridStable line 212
  28. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialLattice line 217
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialLattice_coordinates line 223
  30. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialEvaluationDenominator line 228
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialEvaluationDenominator_pos line 232
  32. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialLattice_maps line 236
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_positivePolynomial_stable_grid line 253
  34. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialModel line 277
  35. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialModelMultidegree line 295
  36. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialModel_complexity line 303
  37. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialEvaluationDenominator_le_exp line 336
  38. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_controlled_positivePolynomial_model line 367
  39. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_positivePolynomial_model_uniform line 401
  40. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetLattice line 434
  41. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetLattice_coordinates line 442
  42. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetModel line 453
  43. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetModelMultidegree line 474
  44. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialDownsetModel_complexity line 482
  45. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialEvaluation_metric_bound line 522
  46. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialEvaluationCosetMap line 535
  47. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialEvaluationCosetMap_mk line 545
  48. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.positivePolynomialEvaluationCosetMap_lipschitz line 561
  49. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_positivePolynomial_observable_pullback line 581
  50. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_positivePolynomial_downset_models_uniform line 612