OAI/Combinatorics/Progressions/Sampling/AllocatedForecastPrimitiveCapBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_modular_forecast_smooth_source line 138
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_original_sample_modular_forecast_source line 357
3. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_modular_forecast_norm_le line 510
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_modular_forecast_source line 711
5. theorem OAI.Erdos3.forecastActualCap_early_exp_bound line 858
6. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_modular_forecast_early_norm_le line 950
7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_modular_forecast_primitive_norm_le line 1081