OAI/Combinatorics/Progressions/Estimates/TailReflectionInduction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_family_reflected_correlation line 11
2. theorem OAI.Erdos3.exists_cubic_reflected_correlation line 98
3. theorem OAI.Erdos3.exists_family_cubic_reflected_correlation line 172
4. def OAI.Erdos3.quarticReflectionKernel line 266
5. theorem OAI.Erdos3.exists_quartic_reflected_correlation line 271
6. structure OAI.Erdos3.TailReflectionData line 356
7. def OAI.Erdos3.TailReflectionData.correlation line 370
8. def OAI.Erdos3.TailReflectionData.pair line 376
9. def OAI.Erdos3.TailReflectionData.reflectedKernel line 400
10. theorem OAI.Erdos3.TailReflectionData.reflectedKernel_cons line 404
11. theorem OAI.Erdos3.TailReflectionData.correlation_square_le_pair line 423
12. theorem OAI.Erdos3.TailReflectionData.exists_reflected_correlation line 502