OAI/Combinatorics/Progressions/Sampling/ForecastOriginalSampleUniformBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.forecastOriginalSmoothBudget line 9
2. theorem OAI.Erdos3.VectorPolynomial.forecastOriginalSmoothBudget_bounds line 12
3. theorem OAI.Erdos3.VectorPolynomial.allocatedForecastAllAxisRowCap_le_exp line 52
4. theorem OAI.Erdos3.VectorPolynomial.allocatedForecastAllAxisLift_budget line 97
5. theorem OAI.Erdos3.VectorPolynomial.forecastEmptySpatial_budget line 165
6. def OAI.Erdos3.VectorPolynomial.forecastOriginalSmoothCapLog line 197
7. def OAI.Erdos3.VectorPolynomial.forecastOriginalSmoothLipLog line 200
8. theorem OAI.Erdos3.VectorPolynomial.forecastAllAxis_budget line 203
9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalForecast_uniform_budget line 289
10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalForecast_common_budget line 321