OAI/Combinatorics/Progressions/Estimates/QuarticCyclicPositiveCorrelation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_quartic_second_exchange_with_mixed line 13
  2. theorem OAI.Erdos3.exists_quartic_second_exchange line 86
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedSecondDifferenceWithShift_diagonal line 116
  4. theorem OAI.Erdos3.exists_quartic_carry_intervals_with_mixed line 133
  5. theorem OAI.Erdos3.exists_quartic_carry_intervals line 202
  6. theorem OAI.Erdos3.exists_quartic_unwrapped_intervals_with_mixed line 238
  7. theorem OAI.Erdos3.exists_quartic_unwrapped_intervals line 298
  8. theorem OAI.Erdos3.exists_quartic_fixed_unwrapped_intervals_with_mixed line 342
  9. theorem OAI.Erdos3.exists_quartic_fixed_unwrapped_intervals line 445
  10. theorem OAI.Erdos3.exists_quartic_multilinear_intervals_with_mixed line 490
  11. theorem OAI.Erdos3.exists_quartic_multilinear_intervals line 590
  12. theorem OAI.Erdos3.exists_quartic_fixed_multilinear_intervals_with_mixed line 646
  13. theorem OAI.Erdos3.exists_quartic_fixed_multilinear_intervals line 751
  14. theorem OAI.Erdos3.exists_quartic_separated_intervals_with_mixed line 807
  15. theorem OAI.Erdos3.exists_quartic_separated_intervals line 908
  16. theorem OAI.Erdos3.exists_quartic_common_interval_with_mixed line 952
  17. theorem OAI.Erdos3.exists_quartic_common_interval line 1045
  18. theorem OAI.Erdos3.exists_quartic_positive_correlation_with_mixed line 1088
  19. theorem OAI.Erdos3.exists_quartic_positive_correlation line 1205
  20. theorem OAI.Erdos3.exists_quartic_cyclic_positive_correlation_with_mixed line 1246
  21. theorem OAI.Erdos3.exists_quartic_cyclic_positive_correlation line 1344