OAI/Combinatorics/SumProduct/Alignment/NearLattice01.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NearLattice.card_int_interval_le line 15
2. theorem OAI.NearLattice.card_int_subset_interval_le line 26
3. theorem OAI.NearLattice.card_nat_subset_interval_le line 35
4. theorem OAI.NearLattice.card_affine_near_le line 49
5. theorem OAI.NearLattice.card_affine_near_abs_le line 96
6. theorem OAI.NearLattice.card_near_of_approx line 115
7. theorem OAI.NearLattice.exists_small_denominator line 200
8. theorem OAI.NearLattice.vinogradov_inverse line 235