OAI/Combinatorics/Progressions/Dynamics/PreparedFiniteStageNativeBudget.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameterPolynomial line 10
  2. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardWorkPolynomial line 22
  3. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCapPolynomial line 26
  4. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCountPolynomial line 31
  5. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardBranchPolynomial line 36
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameterPolynomial_zero line 43
  7. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameterPolynomial_succ line 47
  8. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter line 54
  9. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardWork line 58
  10. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCap line 62
  11. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCount line 66
  12. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardBranch line 70
  13. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter_zero line 74
  14. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardWork_eq line 79
  15. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCap_eq line 86
  16. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCount_eq line 94
  17. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardBranch_eq line 102
  18. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter_succ line 112
  19. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter_nonneg line 121
  20. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardWork_nonneg line 126
  21. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCap_nonneg line 131
  22. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardCount_nonneg line 136
  23. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardBranch_nonneg line 141
  24. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter_strictMono line 146
  25. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardParameter_monotone line 156
  26. theorem OAI.Erdos3.VectorPolynomial.le_preparedFiniteForwardParameter line 161
  27. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardSchedule_budget line 166
  28. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteStageNative_budget line 212
  29. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteStageNative_work_budget line 247