OAI/Combinatorics/Progressions/Sampling/SharedWidthPreparedProductiveShortGoodForecastSource.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedPerturbativeForecastSourceStatement line 12
2. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_perturbative_forecast_source line 171
3. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedEarlyWidthForecastSourceStatement line 281
4. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_early_width_forecast_source line 442
5. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedShortCertifiedForecastSourceStatement line 511
6. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_short_certified_forecast_source line 672
7. def OAI.Erdos3.VectorPolynomial.SharedWidthPreparedProductiveShortGoodForecastSourceStatement line 735
8. theorem OAI.Erdos3.VectorPolynomial.sharedWidthSource_late_projection line 903
9. theorem OAI.Erdos3.VectorPolynomial.exists_sharedWidth_prepared_productive_short_good_forecast_source line 907