OAI/Combinatorics/Progressions/Estimates/AllocatedCommonWeightedOriginal.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedChosenProjectedIdealAt line 56
2. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedData_chosen_projected_ideal line 190
3. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedData_chosen_original_ideal line 303
4. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalPrescribedAtScale line 372
5. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalPrescribedAt line 479
6. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalSelectedAt line 518
7. theorem OAI.Erdos3.VectorPolynomial.allocatedReferencePrescribedIdealAt_original line 657
8. def OAI.Erdos3.VectorPolynomial.AllocatedCommonOriginalAt line 821
9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPrescribedAt_commonScale line 830
10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_common_original line 857
11. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalResidueWeightedAtScale line 936
12. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPrescribedAtScale_residue_weighted line 1041
13. def OAI.Erdos3.VectorPolynomial.AllocatedCommonResidueWeightedOriginalAt line 1081
14. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonOriginalAt_residue_weighted line 1090
15. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_common_residue_weighted_original line 1100