OAI/Combinatorics/Progressions/Sampling/ForecastInactiveFixedProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_fixed_site_expansion line 58
2. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_fixed_site_all_cases line 225
3. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_fixed_budgeted_site line 305
4. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixed_normalized_norm_le line 383
5. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveFixed_norm_exp_bound line 424
6. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_fixed_zero_axis_norm_le line 458
7. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_fixed_zero_axis_site line 521
8. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_fixed_product_site line 605