OAI/Combinatorics/Progressions/Dynamics/PreparedFiniteForwardActualNativeBudget.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleLocalPrecisionBudget line 10
2. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleLocalResourceBudget line 81
3. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleLocalResourceBudget_source_model line 206
4. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleUniformLocalResourceBudget line 252
5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleUniformLocalResourceBudget_source_model line 309
6. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardActualNativeBudget line 356
7. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardActualNativeBudgetExponent line 410
8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardActualNativeBudgetExponent_two_le line 414