OAI/Combinatorics/Progressions/Dynamics/PreparedFiniteForwardLaterWorkBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForward_local_shiftedPower_le_later_work line 9
2. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForward_local_polynomial_le_later_work line 32