OAI/Combinatorics/Progressions/Polynomial/RefinementPolynomialBound.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.CellRefinement.refinementRankPolynomial line 11
  2. def OAI.Erdos3.CellRefinement.refinementDepthPolynomial line 14
  3. def OAI.Erdos3.CellRefinement.refinementFinalRankPolynomial line 16
  4. def OAI.Erdos3.CellRefinement.refinementMatchPolynomial line 19
  5. def OAI.Erdos3.CellRefinement.refinementUnbalancedPolynomial line 22
  6. def OAI.Erdos3.CellRefinement.refinementRoundPolynomial line 28
  7. def OAI.Erdos3.CellRefinement.refinementWidthPolynomial line 32
  8. def OAI.Erdos3.CellRefinement.refinementCostPolynomial line 35
  9. theorem OAI.Erdos3.CellRefinement.refinementRankPolynomial_eval line 41
  10. theorem OAI.Erdos3.CellRefinement.refinementDepthPolynomial_eval line 46
  11. theorem OAI.Erdos3.CellRefinement.refinementFinalRankPolynomial_eval line 50
  12. theorem OAI.Erdos3.CellRefinement.refinementMatchPolynomial_eval line 56
  13. theorem OAI.Erdos3.CellRefinement.refinementUnbalancedPolynomial_eval line 62
  14. theorem OAI.Erdos3.CellRefinement.refinementRoundPolynomial_eval line 71
  15. theorem OAI.Erdos3.CellRefinement.refinementWidthPolynomial_eval line 78
  16. theorem OAI.Erdos3.CellRefinement.refinementCostPolynomial_eval line 84
  17. theorem OAI.Erdos3.CellRefinement.refinement_cost_le_polynomial line 94
  18. theorem OAI.Erdos3.CellRefinement.exists_refinement_cost_polynomial line 210
  19. theorem OAI.Erdos3.CellRefinement.exists_rescaled_refinement_budget line 238