OAI/Combinatorics/Progressions/Geometry/ActualFixedSpatialSlicedModelPrecision.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.inverse_radius_le_one line 32
2. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.nativeAmbientLip_le_one line 41
3. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.nativePullbackLip_le line 70
4. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.nativePullback_lipschitz line 80
5. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.decayConstant_le_exp line 125
6. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernelWidth_lower_of_length line 133
7. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonGridLog line 152
8. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonPrecisionFloor line 156
9. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonError_le_exp line 160
10. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonPrecision_grid_mesh line 255
11. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonPrecision_geometry line 305
12. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonPrecision_tail line 348
13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonPrecisionFloor_pos line 393
14. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.comparisonPrecisionFloor_le_exp line 397
15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.native_ambient_model_precision line 540