OAI/Combinatorics/Progressions/Estimates/AllocatedOriginalPrescribedMesh.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedChosenProjectedIdealMeshAt line 57
2. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedData_chosen_projected_ideal_mesh line 137
3. def OAI.Erdos3.VectorPolynomial.AllocatedChosenOriginalIdealMeshAt line 257
4. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedData_chosen_original_ideal_mesh line 353
5. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalPrescribedMeshAtScale line 422
6. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalPrescribedMeshAt line 530
7. theorem OAI.Erdos3.VectorPolynomial.allocatedReferencePrescribedIdealAt_original_mesh_of_family line 548
8. theorem OAI.Erdos3.VectorPolynomial.allocatedReferencePrescribedIdealAt_original_mesh line 690