OAI/Combinatorics/Progressions/Estimates/FiniteTriangularRationalCorrection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_finite_triangular_correction_of_windows line 13
2. theorem OAI.Erdos3.exists_finite_triangular_rational_correction line 87
3. theorem OAI.Erdos3.exists_triangular_rational_correction_enumeration line 110
4. theorem OAI.Erdos3.exists_triangular_rational_correction_enumeration_exp line 131
5. theorem OAI.Erdos3.exists_uniform_triangular_rational_correction_enumeration line 147