OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateCoveredFamilySuccessor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FamilyGlobalizationAt line 32
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeGlobalizationAt.family line 58
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.familyGlobalizationAt_zero line 73
4. def OAI.Erdos3.RationalFilteredNilmanifold.refilteredQuotientNetExponent line 98
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.refilteredQuotientNetExponent_ge_two line 101
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_refilteredQuotient_uniform_nets line 181
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_refilteredQuotient_uniform_member_nets line 370
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_covered_refilteredQuotient_uniform_member_nets line 496
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_covered_nativeReset_degreeRule line 666
10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_covered_nativeReset_familyRule line 875