OAI/Combinatorics/Progressions/Sampling/ForecastInactiveSlicedCappedContinuousSource.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.forecastInactiveSlicedSiteNumerics line 25
2. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_retained_character_sites line 92
3. def OAI.Erdos3.VectorPolynomial.slicedFixedUniformSiteLog line 198
4. theorem OAI.Erdos3.VectorPolynomial.slicedFixedUniformSiteLog_nonneg line 201
5. theorem OAI.Erdos3.VectorPolynomial.slicedGridSiteLog_le_uniform line 209
6. def OAI.Erdos3.VectorPolynomial.slicedFixedUniformAccuracyLog line 217
7. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSlicedSiteNumerics_of_uniform_envelope line 225
8. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSlicedSiteNumerics_of_primitive_uniform_budgets line 324
9. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_rational_site_approximation line 404
10. theorem OAI.Erdos3.VectorPolynomial.forecastInactiveSlicedTailCap_of_primitive_uniform_budgets line 500
11. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_continuous_rational_source line 567
12. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_capped_continuous_rational_source line 701