OAI/Combinatorics/Progressions/Geometry/ActualFixedSpatialSlicedDataComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.centered_recovery line 51
2. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.stepInputLaw_sample_characteristic_decay line 121
3. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.modular_decay_dimension line 153
4. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.nativeMean line 251
5. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.decayConstant line 258
6. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonError line 310
7. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.native_ambient_comparison line 340
8. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.native_ambient_comparison_actualForecastData line 558
9. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.native_ambient_model_comparison line 605