OAI/Combinatorics/Progressions/Estimates/AllocatedIdealComparisonAssembly.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCovered_profile_comparison line 57
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_ideal_comparison line 113
3. def OAI.Erdos3.VectorPolynomial.AllocatedGoodKernelIdealResult line 261
4. def OAI.Erdos3.VectorPolynomial.AllocatedPhysicalIdealAt line 328
5. def OAI.Erdos3.VectorPolynomial.AllocatedGoodKernelIdealAt line 435
6. def OAI.Erdos3.VectorPolynomial.AllocatedChosenIdealAt line 479
7. theorem OAI.Erdos3.VectorPolynomial.allocatedGoodKernelIdealAt_chooseScale line 502
8. theorem OAI.Erdos3.VectorPolynomial.allocated_goodKernel_ideal_of_comparison line 543