OAI/Combinatorics/Progressions/Estimates/EuclideanGraphResidual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.euclideanDerivativeShiftMap line 12
2. theorem OAI.Erdos3.euclideanDerivativeShiftMap_apply line 18
3. theorem OAI.Erdos3.euclideanDerivativeShiftMap_eq_zero_iff line 23
4. theorem OAI.Erdos3.euclideanDerivativeShiftMap_integer line 32
5. theorem OAI.Erdos3.euclideanDerivative_vertical_lattice_full line 43
6. theorem OAI.Erdos3.euclideanDerivative_integer_shift_lifts line 60
7. theorem OAI.Erdos3.euclidean_graph_residual_mem_kernel line 113