OAI/Combinatorics/Progressions/Fourier/AffineTorusDensityIncrement.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.periodic_lipschitz_dist_le_of_integer_approx line 14
2. theorem OAI.Erdos3.affine_phase_block_error line 29
3. theorem OAI.Erdos3.affine_torus_block_error line 55
4. theorem OAI.Erdos3.exists_affine_torus_progression_partition line 70
5. theorem OAI.Erdos3.affine_torus_density_increment line 105