OAI/Combinatorics/Progressions/Polynomial/CandidateNestedDegreeNetSchedule.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.candidateDegreeReturnBudget line 10
  2. theorem OAI.Erdos3.VectorPolynomial.candidateDegreeReturnBudget_zero line 13
  3. theorem OAI.Erdos3.VectorPolynomial.candidateDegreeReturnBudget_succ line 17
  4. theorem OAI.Erdos3.VectorPolynomial.candidateDegreeReturnBudget_nonneg line 23
  5. theorem OAI.Erdos3.VectorPolynomial.candidateDegreeReturnBudget_mono line 31
  6. theorem OAI.Erdos3.VectorPolynomial.candidateDegreeReturnBudget_monotone_degree line 39
  7. theorem OAI.Erdos3.VectorPolynomial.le_candidateDegreeReturnBudget line 47
  8. theorem OAI.Erdos3.VectorPolynomial.candidateDegreeReturnBudget_bounds_sequence line 52
  9. theorem OAI.Erdos3.VectorPolynomial.exists_candidateDegreeReturn_nested_power_budget line 63
  10. theorem OAI.Erdos3.VectorPolynomial.exists_candidateNestedForward_polynomial_next_seed line 100
  11. theorem OAI.Erdos3.VectorPolynomial.exists_candidateDegreeReturn_next_seed line 127
  12. def OAI.Erdos3.VectorPolynomial.candidateNestedDegreeNetExponent line 159
  13. theorem OAI.Erdos3.VectorPolynomial.candidateNestedDegreeNetExponent_zero line 164
  14. theorem OAI.Erdos3.VectorPolynomial.candidateNestedDegreeNetExponent_succ line 167
  15. def OAI.Erdos3.VectorPolynomial.candidateNestedDegreeConstantBound line 172
  16. theorem OAI.Erdos3.VectorPolynomial.candidateNestedDegreeConstant_le_bound line 177
  17. def OAI.Erdos3.VectorPolynomial.candidateNestedDegreeNetBound line 187
  18. theorem OAI.Erdos3.VectorPolynomial.candidateNestedDegreeNetExponent_le_bound line 190
  19. theorem OAI.Erdos3.VectorPolynomial.exists_candidateNestedDegreeReturn_power_budget line 195