OAI/Combinatorics/Progressions/Fourier/AffineTorusGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.affineTorusRadius line 12
2. def OAI.Erdos3.affineTorusFactor line 15
3. theorem OAI.Erdos3.affineTorusFactor_pos line 18
4. instance OAI.Erdos3.affineTorusFactor_neZero line 22
5. theorem OAI.Erdos3.affineTorusFactor_le line 25
6. theorem OAI.Erdos3.affineWeightedCube_bound_le_torus line 29
7. theorem OAI.Erdos3.affineWeightedModerate_bound_le_torus line 42
8. theorem OAI.Erdos3.affineModerate_physical_volume_lower line 56