OAI/Combinatorics/Progressions/Sampling/AllocatedExternalCandidateActualShearForecastScore.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.exists_retained_degreeZero_forecast_score line 50
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.exists_shear_buffered_forecast_score line 152
3. def OAI.Erdos3.VectorPolynomial.actualForecastDataModelRequired line 268
4. def OAI.Erdos3.VectorPolynomial.PreparedActualSlicedForecastModelPacket line 272
5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedActualSlicedForecastModelPacket line 310
6. theorem OAI.Erdos3.VectorPolynomial.exists_preparedActualSlicedForecastModelPacket_from_setup line 336
7. theorem OAI.Erdos3.VectorPolynomial.exists_preparedActualSlicedForecastModelPacket_from_setup_with_cap_bound line 369
8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleModelsAtLaw_actualData line 409
9. theorem OAI.Erdos3.VectorPolynomial.actualForecastDataModelRequired_sum_bound line 487
10. theorem OAI.Erdos3.VectorPolynomial.actualForecastDataModelRequired_common_precision line 507
11. theorem OAI.Erdos3.VectorPolynomial.exists_actualForecastDataModelRequired_common_polynomial_budget line 518
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.exists_actual_shear_buffered_forecast_score line 608