OAI/Combinatorics/Progressions/Dynamics/AllocatedExternalCandidateCoveredBudget.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.finiteFreezingInitialPrecision line 9
  2. def OAI.Erdos3.VectorPolynomial.finiteFreezingInitialDiscard line 12
  3. def OAI.Erdos3.VectorPolynomial.finiteFreezingRecursiveParameter line 15
  4. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_precision_pos line 18
  5. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_discard_pos line 21
  6. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_precision_lt_one line 24
  7. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_discard_lt_one line 30
  8. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_precision_exponent line 35
  9. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_discard_exponent line 40
  10. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_score_surplus line 45
  11. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_initial_le_polynomial line 59
  12. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_uniform_recursive_exponents line 68
  13. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_uniform_recursive_budget line 92
  14. theorem OAI.Erdos3.VectorPolynomial.exists_finiteFreezingRecursiveParameter_bound line 109
  15. theorem OAI.Erdos3.VectorPolynomial.exists_finiteFreezing_recursive_output_bound line 118
  16. def OAI.Erdos3.VectorPolynomial.candidateCoveredOuterParameter line 136
  17. def OAI.Erdos3.VectorPolynomial.candidateCoveredRightParameter line 139
  18. def OAI.Erdos3.VectorPolynomial.candidateCoveredDictionaryParameter line 142
  19. def OAI.Erdos3.VectorPolynomial.candidateCoveredGeometryParameter line 145
  20. def OAI.Erdos3.VectorPolynomial.candidateCoveredDiagramParameter line 149
  21. theorem OAI.Erdos3.VectorPolynomial.candidateCoveredGeometryParameter_bounds line 152
  22. theorem OAI.Erdos3.VectorPolynomial.exists_candidateCoveredParameters_bound line 176