OAI/Combinatorics/Progressions/Estimates/AllocatedCandidateTerminalNextWork.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCandidateTerminalFullInput_forward_budget line 11
2. def OAI.Erdos3.VectorPolynomial.terminalAffinePolynomial line 49
3. theorem OAI.Erdos3.VectorPolynomial.terminalAffinePolynomial_eval line 54
4. def OAI.Erdos3.VectorPolynomial.terminalUniformPolynomial line 60
5. theorem OAI.Erdos3.VectorPolynomial.terminalUniformPolynomial_eval line 65
6. theorem OAI.Erdos3.VectorPolynomial.terminalFullInput_le_uniform line 77
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCandidateTerminalFullInput_polynomial_next_work line 89
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCandidateTerminalFullInput_next_work line 134