OAI/Combinatorics/Progressions/Sampling/AllocatedFiniteModelSquareSampling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos3.BooleanCubeKernel.physicalModelRows line 14
2. abbrev OAI.Erdos3.BooleanCubeKernel.physicalModelRowSets line 17
3. def OAI.Erdos3.BooleanCubeKernel.PhysicalModelSquareSampling line 20
4. theorem OAI.Erdos3.BooleanCubeKernel.exists_physical_model_square_sampling line 80
5. def OAI.Erdos3.BooleanCubeKernel.physicalModelSamplingExponent line 126
6. theorem OAI.Erdos3.BooleanCubeKernel.physicalModelSamplingExponent_spec line 129
7. theorem OAI.Erdos3.VectorPolynomial.allocated_finite_model_square_sampling line 185
8. theorem OAI.Erdos3.VectorPolynomial.allocated_finite_model_reference_sample line 299