OAI/Combinatorics/Progressions/Sampling/ActualFixedSpatialCenteredForecastModel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.forecastJacobianScaledExpansion_identity line 13
2. theorem OAI.Erdos3.forecastJacobianScaledExpansion_mass line 23
3. theorem OAI.Erdos3.forecastJacobianScaledExpansion_error line 31
4. theorem OAI.Erdos3.forecastJacobianScaledExpansion_cap line 41
5. theorem OAI.Erdos3.VectorPolynomial.forecastJacobianScaledNativeExpansion line 51
6. theorem OAI.Erdos3.VectorPolynomial.exists_fixedSpatialKernel_scaled_native_forecast_source line 228
7. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.target_norm_le line 371
8. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.target_norm_le line 435
9. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialForecastFamily_of_certificate line 504
10. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialForecastFamily line 659
11. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialForecastFamily_option_of_certificate line 723
12. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatial_centered_forecast_model line 797