OAI/Combinatorics/Progressions/Estimates/AllocatedFlexibleOriginalMesh.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedReferenceSelectedIdealAt line 22
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_reference_chosen_ideal line 162
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_reference_prescribed_ideal line 228
4. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceChosenIdealAt_selectData line 295
5. def OAI.Erdos3.VectorPolynomial.AllocatedCommonReferenceAt line 342
6. theorem OAI.Erdos3.VectorPolynomial.allocatedReferencePrescribedIdealAt_commonScale line 351
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_common_reference line 374
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_reference_selected_ideal line 433
9. def OAI.Erdos3.VectorPolynomial.AllocatedCommonOriginalMeshAt line 500
10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPrescribedMeshAt_commonScale line 509
11. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_common_original_mesh line 536
12. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalResidueWeightedMeshAtScale line 615
13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPrescribedMeshAtScale_residue_weighted line 721
14. def OAI.Erdos3.VectorPolynomial.AllocatedCommonResidueWeightedOriginalMeshAt line 761
15. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonOriginalMeshAt_residue_weighted line 770
16. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_common_residue_weighted_original_mesh line 780
17. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_allocated_flexible_original_mesh line 831