OAI/Combinatorics/Progressions/Sampling/PreparedShortForecastRawSourceBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.preparedForecastLateScalarBounds line 9
2. structure OAI.Erdos3.VectorPolynomial.PreparedForecastSourceScalarBounds line 44
3. theorem OAI.Erdos3.VectorPolynomial.preparedForecastSourceScalarBounds line 65
4. theorem OAI.Erdos3.VectorPolynomial.preparedForecastSource_width line 132
5. structure OAI.Erdos3.VectorPolynomial.PreparedCenteredShortForecastGoodBounds line 263
6. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecastGoodExtraData line 317
7. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecastGoodModelInterface_of_model line 404
8. structure OAI.Erdos3.VectorPolynomial.PreparedShortForecastSourceRawBounds line 507
9. theorem OAI.Erdos3.VectorPolynomial.preparedShortForecastSourceRawBounds_to_good line 557
10. theorem OAI.Erdos3.VectorPolynomial.preparedShortForecastRawSourceBounds line 629