OAI/Combinatorics/Progressions/Polynomial/ScalarNestedSourceDegreeGlobalization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.zeroLayerNestedDegreeSourceProfile line 52
2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.zeroLayerNestedDegreeSourceProfile_of_exponent line 177
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_zeroLayerNestedDegreeSourceProfile_scalars line 240
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_zeroLayerNestedDegreeSourceProfile_of_exponent_scalars line 297
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_zeroLayerNestedDegreeSourceProfile_full_scalars line 396
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_zeroLayerNestedDegreeSourceProfile_of_exponent_full_scalars line 458
7. def OAI.Erdos3.VectorPolynomial.PreparedScalarNestedPowerDegreeProfiles line 524
8. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarNestedPowerDegreeProfiles_of_exponent line 594
9. def OAI.Erdos3.VectorPolynomial.preparedScalarNestedFamilyProfileExponent line 668
10. theorem OAI.Erdos3.VectorPolynomial.preparedScalarNestedFamilyProfileExponent_bounds line 673
11. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarNestedPowerDegreeProfiles line 689
12. def OAI.Erdos3.VectorPolynomial.PreparedScalarNestedPowerDegreeProfilesFull line 714
13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarNestedPowerDegreeProfiles_full_of_exponent line 788
14. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarNestedPowerDegreeProfiles_full line 860
15. def OAI.Erdos3.VectorPolynomial.ScalarNestedSourceDegreeGlobalization line 886
16. theorem OAI.Erdos3.VectorPolynomial.exists_scalarNestedSourceDegreeGlobalization line 920