OAI/Combinatorics/Progressions/Sampling/ActualSlicedForecastLateData.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_separateTail_continuous_rational_source line 34
2. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_separateTail_native_source line 189
3. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecast_native_source line 416
4. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.targetAt line 601
5. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.targetAt_eq_target line 635
6. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecast_universal_native_source line 651
7. structure OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedAdmissiblePath line 830
8. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecastFamily_of_numerics line 850
9. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecastFamily_option_of_numerics line 966
10. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecastUniversalFamily_of_numerics line 1030
11. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecastUniversalFamily_option_of_numerics line 1159
12. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedAdmissiblePath.withNumerics line 1239
13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedAdmissiblePath.withNumerics_slice line 1254
14. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedAdmissiblePath.withNumerics_target line 1270
15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedAdmissiblePath.withNumerics_targetAt line 1280
16. theorem OAI.Erdos3.VectorPolynomial.actualSlicedForecastOptionFamily_accuracy_transport line 1300
17. theorem OAI.Erdos3.VectorPolynomial.exists_actualSlicedForecast_late_data line 1384