OAI/Combinatorics/Progressions/Polynomial/NativePolynomialOrbitConstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.NativePolynomialOrbitFactors line 13
2. def OAI.Erdos3.NativePolynomialOrbitFactors.mono line 60
3. theorem OAI.Erdos3.NativePolynomialOrbitFactors.middle_values line 69
4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.middle_top_frequency line 79
5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.middle_bracket_frequency line 84
6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.eval_niltest line 96
7. theorem OAI.Erdos3.exists_native_polynomial_orbit_factors line 118