OAI/Combinatorics/Progressions/Geometry/ActualFixedSpatialSlicedAnalyticIdentification.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernelSupport line 38
2. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.activeSide line 44
3. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.activeLength_two line 49
4. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.activeSupport line 59
5. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.activeLower_eq line 66
6. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.activeWidth_eq line 71
7. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.normalizedNoise_eq_kernelFrame line 115