OAI/Combinatorics/Progressions/Polynomial/AllocatedAxisPartitionWithTailDegree.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerPMFsWithTailDegree line 20
2. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerColumnsWithTailDegree_chart line 31
3. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerSupportedWithTailDegree_polynomial_chart line 48
4. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerWithTailDegree_moderate_tail_zero line 87
5. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerWithTailDegree_moderate_eval line 102
6. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerWithTailDegree_moderate_eval_congr line 116
7. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerWithTailDegree_moderateJet_congr line 136
8. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerModerateIntegerImageWithTailDegree_freeze line 167
9. def OAI.Erdos3.VectorPolynomial.allocatedGridAxisWithTailDegree line 206
10. instance OAI.Erdos3.VectorPolynomial.allocatedGridAxisWithTailDegreeDecidable line 210
11. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSidesWithTailDegree_long line 219
12. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSidesWithTailDegree_long_restricted line 238
13. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalWithTailDegree_partition_residues line 248
14. theorem OAI.Erdos3.VectorPolynomial.allocatedGridAxisWithTailDegree_jet_frozen line 270