OAI/Combinatorics/Progressions/Polynomial/SlicedPolynomialPerturbation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.parameterPolynomialMap_mass_c2_bounds line 9
2. theorem OAI.Erdos3.realPolynomialMass_divMonomial_le line 49
3. theorem OAI.Erdos3.parameterPolynomialMap_mass_difference line 66
4. def OAI.Erdos3.slicedPolynomialScale line 100
5. theorem OAI.Erdos3.slicedPolynomialScale_spec line 103
6. theorem OAI.Erdos3.jointSlicedPrincipal_polynomial_tail_comparison line 151