OAI/Combinatorics/Progressions/Geometry/AllocatedCommonSupportedMesh.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalMeshForSampler line 35
2. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalSupportedMeshAtScale line 132
3. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSupportedMesh_budgets line 263
4. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalResidueWeightedMeshAtScale_supported line 319
5. def OAI.Erdos3.VectorPolynomial.AllocatedCommonSupportedMeshAt line 432
6. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonResidueWeightedOriginalMeshAt_supported line 448