OAI/Combinatorics/Progressions/Dynamics/AllocatedExternalCandidateExponentialFreezingBudget.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.mono line 46
  2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.massBudget line 60
  3. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.budgetRefinement line 113
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.budgetRefinement_productive line 127
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.budgetRefinement_chartValues line 132
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.budgetRefinement_physical line 139
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.budgetRefinement_candidate_orbit line 146
  8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.mono line 157
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.mono_ambient line 172
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.mono_retained line 177
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.mono_slice line 182
  12. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_cost_le_uniform line 197
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.refilteredFrozenScore_mono line 270
  14. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_densityLoss line 291
  15. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_cost_le line 302
  16. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_cost_le_of_card_bound line 313
  17. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_mass line 325
  18. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_mass_le line 331
  19. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_recursive_mass_le line 336
  20. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_recursive_score_le line 342
  21. theorem OAI.Erdos3.VectorPolynomial.finiteFreezing_exp_recursive_budget line 347