OAI/Combinatorics/Progressions/Geometry/FixedSpatialNativeRawSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_nonzero_norm_le_two line 51
2. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_nonzero_spatial_bounds line 59
3. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_nonzero_active_bounds line 68
4. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_active_bound_three line 77
5. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernelOriginalForecastDensity_zero_outside_integerBox line 90
6. theorem OAI.Erdos3.VectorPolynomial.forecastNativeRawSpatialFamily_fixedSpatial_zero_outside line 115