OAI/Combinatorics/Progressions/Sampling/ForecastInactiveSlicedFixedScalarCapBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_zero_axis_budgeted_site line 45
2. def OAI.Erdos3.VectorPolynomial.slicedFixedZeroGeometryLog line 96
3. theorem OAI.Erdos3.VectorPolynomial.slicedFixedZeroGeometryLog_nonneg line 101
4. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_sliced_fixed_zero_axis_geometry_bounds line 109
5. theorem OAI.Erdos3.VectorPolynomial.exists_forecastInactive_sliced_fixed_zero_axis_primitive_budgeted_site line 173
6. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_sliced_fixed_zero_axis_norm_le_primitive_budget line 266