OAI/Combinatorics/Progressions/Estimates/CubeTranslation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.translateSupport line 13
2. theorem OAI.Erdos3.mem_translateSupport line 15
3. theorem OAI.Erdos3.card_translateSupport line 24
4. def OAI.Erdos3.supportedCubeTranslateEquiv line 27
5. theorem OAI.Erdos3.card_supportedCube_translate line 48
6. theorem OAI.Erdos3.mixedCubeProduct_translate line 54
7. theorem OAI.Erdos3.supportedCubeSum_translate line 59
8. theorem OAI.Erdos3.finiteSupportGowersNorm_translate line 68
9. theorem OAI.Erdos3.ReflectsPairSums.translate line 73