OAI/Combinatorics/Progressions/Sampling/ForecastInactiveSlicedFixedAxisCap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_sliced_fixed_mem_physical_support line 40
2. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_sliced_fixed_scaled_support line 53
3. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_bounded_site_expansion line 65
4. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_site_expansion line 161
5. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_zero_axis_site line 343
6. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_sliced_fixed_zero_axis_norm_le line 406
7. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveGrid_height_le_of_small_original_side line 482
8. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_site_all_cases line 512
9. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_site_small_or_dense line 573
10. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_sliced_fixed_zero_axis_norm_le_small_or_dense line 676