OAI/Combinatorics/Progressions/Estimates/QuadraticCyclicAntisymmetric.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_reflected_corner_correlation line 17
  2. theorem OAI.Erdos3.derivative_correlation_mean_sq_le line 87
  3. theorem OAI.Erdos3.derivative_correlation_fourth_moment line 143
  4. theorem OAI.Erdos3.exists_phase_aligned_derivatives line 179
  5. theorem OAI.Erdos3.exists_correlated_corner line 196
  6. theorem OAI.Erdos3.exists_quadratic_bounded_mixed_correlation line 233
  7. theorem OAI.Erdos3.exists_quadratic_native_mixed_correlation line 284
  8. theorem OAI.Erdos3.exists_quadratic_fixed_mixed_correlation line 313
  9. theorem OAI.Erdos3.exists_quadratic_corner_model line 350
  10. theorem OAI.Erdos3.exists_quadratic_exchanged_correlations line 421
  11. theorem OAI.Erdos3.exists_quadratic_reflected_model line 491
  12. theorem OAI.Erdos3.exists_quadratic_cyclic_antisymmetric line 544