OAI/Combinatorics/EuclideanRamsey/RationalConvolution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanRamsey.bounded_grid_finite line 25
2. lemma OAI.EuclideanRamsey.lattice_sum_perturb_bound line 31
3. theorem OAI.EuclideanRamsey.lattice_riemann_perturb line 52
4. lemma OAI.EuclideanRamsey.convolution_support line 86
5. lemma OAI.EuclideanRamsey.rational_convolution_coeff line 98
6. lemma OAI.EuclideanRamsey.rational_vector_strict line 119
7. lemma OAI.EuclideanRamsey.rationalize_convolution line 133