OAI/Combinatorics/Progressions/Estimates/IntegralHyperplaneCorrection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.normalFunctional line 12
2. theorem OAI.Erdos3.normalFunctional_apply line 15
3. def OAI.Erdos3.integralHyperplaneCorrection line 17
4. theorem OAI.Erdos3.integralHyperplaneCorrection_inner line 20
5. theorem OAI.Erdos3.integralHyperplaneCorrection_norm_sub line 28
6. theorem OAI.Erdos3.exists_hyperplane_lattice_translate line 40
7. theorem OAI.Erdos3.exists_corrected_hyperplane_representative line 48