OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateThresholdSuccessor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_floor_le_exp line 10
  2. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_floor_le_recursive line 30
  3. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_floor_of_recursive_side line 43
  4. def OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff line 61
  5. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff_ge_input line 65
  6. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff_le_geometry line 72
  7. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff_le_budget line 102
  8. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff_floor line 109
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_primitive_nativeReset_degreeRule line 191
  10. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff_add_two_le_geometry line 304
  11. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff_add_two_le_budget line 338
  12. theorem OAI.Erdos3.VectorPolynomial.candidatePrimitiveFreezingCutoff_integer_cost line 345
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_threshold_nativeReset_degreeRule line 420