OAI/Combinatorics/Progressions/Linear/SmoothCoefficientRankBadProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.scalarCoefficientTupleEquiv line 11
2. def OAI.Erdos3.scalarCoefficientBad line 26
3. theorem OAI.Erdos3.scalarCoefficientBad_probability_eq line 34
4. theorem OAI.Erdos3.scalarCoefficientBad_probability line 51
5. theorem OAI.Erdos3.uniform_eventProbability_instances line 79
6. def OAI.Erdos3.smoothCoefficientRankBad line 90
7. theorem OAI.Erdos3.smoothCoefficientRank_bad_product_probability line 96
8. theorem OAI.Erdos3.exists_early_smoothCoefficientRank_bad_product_cutoff line 128