OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateRealThreshold.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.candidateSideCutoff line 12
2. theorem OAI.Erdos3.VectorPolynomial.candidateSideCutoff_pos line 14
3. theorem OAI.Erdos3.VectorPolynomial.lt_candidateSideCutoff line 17
4. theorem OAI.Erdos3.VectorPolynomial.candidateSideCutoff_lt_max_add_two line 22
5. def OAI.Erdos3.VectorPolynomial.candidateSideCutoffCost line 30
6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.realThresholdKeep line 62
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.realThreshold_long line 71
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.realThreshold_strict_long line 80
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_realThresholdAxisFreezing line 87