OAI/Combinatorics/Progressions/Sampling/FixedSpatialKernelNativeForecastSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_retained_character_sites line 29
2. theorem OAI.Erdos3.VectorPolynomial.exists_forecast_rational_site_approximation line 160
3. theorem OAI.Erdos3.VectorPolynomial.exists_forecast_actual_smooth_rational_source line 362
4. theorem OAI.Erdos3.VectorPolynomial.exists_forecast_continuous_rational_source line 580
5. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_modular_forecast_continuous_source line 791
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_original_sample_modular_forecast_continuous_source line 987
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_density_native_forecast_source line 1189
8. theorem OAI.Erdos3.VectorPolynomial.exists_fixedSpatialKernel_native_forecast_source line 1480