OAI/Combinatorics/Progressions/Lattices/IntegerGridPointCap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.integerPointDensity_norm_le_fourier_sum line 12
2. theorem OAI.Erdos3.pmf_bind_point_norm_le line 42