OAI/Combinatorics/Progressions/Sampling/DetectedTranslationMajorSamplingContainment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.realSpanIntegerRowBound_le_exp_of_imageHeight line 9
2. theorem OAI.Erdos3.samplingProjectedImage_row_le_exp line 29
3. theorem OAI.Erdos3.exists_samplingProjectedImage_budget line 43
4. theorem OAI.Erdos3.exists_samplingProjectedImage_complete_budget line 83
5. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslation_samplingRank_le_base_span line 134
6. theorem OAI.Erdos3.PolynomialTranslationLie.exists_detectedTranslation_samplingRank_le_base_span line 201
7. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorTranslation_samplingRank_le_real_base_image line 258