OAI/Combinatorics/Progressions/Estimates/GaussianScaledShortVectorBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.latticeGaussianMass_ge_multiples line 11
2. theorem OAI.Erdos3.latticeGaussianMass_mul_norm_ge line 43
3. theorem OAI.Erdos3.latticeGaussianMass_controls_integer_factor line 62
4. theorem OAI.Erdos3.latticeGaussianMass_ge_multiples_at_temperature line 89
5. theorem OAI.Erdos3.latticeGaussianMass_mul_scaled_norm_ge line 126