OAI/Combinatorics/Progressions/Polynomial/ShiftedSmoothPolynomialSublevel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.decide_eq_classical line 11
2. def OAI.Erdos3.shiftedSmoothSublevelConstant line 16
3. def OAI.Erdos3.shiftedSmoothSublevelThreshold line 19
4. theorem OAI.Erdos3.shiftedSmoothSublevelConstant_nonneg line 23
5. theorem OAI.Erdos3.shiftedSmoothSublevelThreshold_pos line 29
6. theorem OAI.Erdos3.shiftedSmoothSublevelThreshold_le_half line 34
7. theorem OAI.Erdos3.shiftedSmoothProduct_polynomial_sublevel line 39
8. theorem OAI.Erdos3.shiftedSmoothProduct_polynomial_family_threshold line 61