OAI/Combinatorics/Progressions/Lattices/CircleResiduePartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.CircleFourier.one_le_mul_dist_toAddCircle line 13
2. def OAI.Erdos3.CircleFourier.residueCutoff line 28
3. theorem OAI.Erdos3.CircleFourier.residueCutoff_unit_interval line 31
4. theorem OAI.Erdos3.CircleFourier.residueCutoff_lipschitz line 36
5. theorem OAI.Erdos3.CircleFourier.residueCutoff_at_grid line 54
6. theorem OAI.Erdos3.CircleFourier.sum_residueCutoff_at_grid line 63
7. theorem OAI.Erdos3.CircleFourier.residueCutoff_positive_iff line 68