OAI/Combinatorics/Progressions/Estimates/CubicPermutedSeven.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.cubicExchangeSwap line 11
  2. theorem OAI.Erdos3.expect_cubicExchangeSwap line 13
  3. def OAI.Erdos3.cubicReducedCorner line 22
  4. def OAI.Erdos3.cubicSymmetricCorner line 31
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSymmetricSeven line 44
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSymmetricSeven_norm line 47
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSymmetricSeven_unit line 52
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSymmetricSeven_explicit line 60
  9. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenOriginalFactor line 74
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenOriginalFactor_norm line 78
  11. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenExchangeFactor line 83
  12. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenExchangeProduct line 90
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedSeven_cross_symmetric line 95
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenExchangeFactor_norm line 109
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenExchangeProduct_norm line 120
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenExchangeFactor_mean_error line 129
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSevenExchangeProduct_mean_error line 179
  18. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicWrappedDiagonalCorrection line 225
  19. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicCyclicDiagonalCorrection line 232
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicWrappedDiagonalCorrection_mean_error line 240
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicCyclicDiagonalCorrection_mean_error line 284
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_cubicCyclicDiagonalCorrection_expansion line 326
  23. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedExchangeLeft line 425
  24. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedExchangeRight line 435
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedExchangeLeft_norm line 445
  26. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedExchangeRight_norm line 461
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedExchangeLeft_mean_error line 477
  28. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedExchangeRight_mean_error line 504
  29. def OAI.Erdos3.cubicSevenMerge line 546
  30. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicHnnTensor line 553
  31. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicHhnTensor line 556
  32. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicHnnTensor_norm line 559
  33. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicHhnTensor_norm line 564
  34. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicHnnTensor_unit line 569
  35. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicHhnTensor_unit line 573
  36. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicSymmetricSeven_merge line 577
  37. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRawSevenFactor line 604
  38. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicRawSevenFactor_norm line 609
  39. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicMixedSeven_cross_symmetric_raw line 614
  40. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedSevenFactor line 622
  41. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedSevenProduct line 630
  42. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedSevenFactor_norm line 635
  43. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedSevenProduct_norm line 651
  44. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedSevenFactor_mean_error line 664
  45. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicPermutedSevenProduct_mean_error line 688