OAI/Combinatorics/Progressions/Sampling/AllocatedRecoveredForecastDecay.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_read_depth line 21
2. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_read_product line 31
3. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_read_deep_product line 41
4. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysical_forecast_bad_product_le line 60
5. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysical_forecast_bad_product_le_of_deep line 72
6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalForecast_crt_decay line 120
7. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalForecast_crt_decay_of_deep line 150
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_modular_forecast_continuous_source line 295
9. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredForecastPolynomial_eq line 454
10. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredForecast_crt_decay line 483