OAI/Combinatorics/Progressions/Sampling/PreparedCenteredForecastEarlyWidth.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecast_slice_bounds line 23
2. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecast_slice_family_bounds line 29
3. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecast_niltest_star_eval_bound line 39
4. def OAI.Erdos3.VectorPolynomial.PreparedCenteredForecastModelInterface line 116
5. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecastModelInterface_of_radius line 256
6. def OAI.Erdos3.VectorPolynomial.PreparedActualForecastModelInterface line 421
7. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastModelInterface_of_prepared line 556
8. def OAI.Erdos3.VectorPolynomial.PreparedCenteredForecastEarlyWidthModelInterface line 695
9. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecastEarlyWidthModelInterface_of_model line 707
10. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecastEarlyWidthModelInterface_apply line 729