OAI/Combinatorics/Progressions/Sampling/PreparedModularGeneralDetectorSamplingBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.boundedCoefficientExponent_card_mono_embedding line 10
2. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientIndex_card_from_layer_counts line 21
3. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_jet_counts_of_geometry line 51
4. structure OAI.Erdos3.VectorPolynomial.PreparedModularGeneralDetectorSamplingBounds line 68
5. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_sampling_bounds line 116
6. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralDetector_sampling_bounds_of_geometry line 271