OAI/Combinatorics/Progressions/Dynamics/PreparedNestedEndpointDimensionBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_endpointDimension_local_budget line 11
2. theorem OAI.Erdos3.VectorPolynomial.exists_endpointDimension_uniform_budget line 32
3. def OAI.Erdos3.VectorPolynomial.preparedNestedEndpointDimensionExponent line 54
4. theorem OAI.Erdos3.VectorPolynomial.preparedNestedEndpointDimensionExponent_two_le line 57
5. theorem OAI.Erdos3.VectorPolynomial.preparedNestedEndpointDimension_bounds line 61