OAI/Combinatorics/Progressions/Estimates/GaussianPerturbation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.norm_sq_le_four_add_dilated_norm_sq line 11
2. theorem OAI.Erdos3.gaussian_perturbation_lower line 28
3. theorem OAI.Erdos3.gaussian_orbit_perturbation_lower line 38