OAI/Combinatorics/Progressions/Estimates/QuarticCyclicDiagonalComparison.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.quarticBlockPermutation line 9
  2. theorem OAI.Erdos3.quarticInput_replica line 12
  3. theorem OAI.Erdos3.quarticInput_permute line 16
  4. theorem OAI.Erdos3.quartic_eval_permute line 29
  5. theorem OAI.Erdos3.quartic_eval_permutationWord line 38
  6. theorem OAI.Erdos3.quartic_eval_doubleFirst line 45
  7. theorem OAI.Erdos3.quartic_eval_doubleSecond line 58
  8. abbrev OAI.Erdos3.QuarticSixFactorIndex line 81
  9. def OAI.Erdos3.quarticSixMain line 83
  10. def OAI.Erdos3.quarticSixBoundary line 87
  11. def OAI.Erdos3.quarticSixFactorVector line 92
  12. def OAI.Erdos3.quarticSixFactorCoordinate line 96
  13. def OAI.Erdos3.quarticSixFactorReindex line 100
  14. theorem OAI.Erdos3.quarticSixFactorReindex_class line 104
  15. theorem OAI.Erdos3.quarticSixFactorVector_reindex line 110
  16. theorem OAI.Erdos3.quarticSixFactorIndex_card line 141
  17. theorem OAI.Erdos3.quarticSixMain_unit line 147
  18. theorem OAI.Erdos3.quarticSixBoundary_unit line 154
  19. theorem OAI.Erdos3.quarticSixFactorVector_unit line 163
  20. theorem OAI.Erdos3.quarticSixBoundary_norm line 169
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticSixMain_tensorPower line 189
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.tensorPower_quartic_repeated_symmetry line 199
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticSixMain_norm line 212
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_six_factor_multilinearization line 227
  25. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.quartic_six_factor_sample_correlation line 265
  26. def OAI.Erdos3.quarticPermuteSample line 306
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_division_quartic_last_slots_equivalence line 311
  28. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_division_quartic_tensor_last_slots_equivalence line 348
  29. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_root_last_slots_equivalence line 385
  30. def OAI.Erdos3.quarticCornerWeight line 410
  31. def OAI.Erdos3.quarticCornerSample line 412
  32. def OAI.Erdos3.quarticCanonicalSample line 414
  33. def OAI.Erdos3.quarticTailSortWord line 417
  34. def OAI.Erdos3.quarticHeadWord line 423
  35. def OAI.Erdos3.quarticPreExchangeSample line 426
  36. def OAI.Erdos3.quarticPostExchangeWord line 429
  37. theorem OAI.Erdos3.quarticCornerSample_input line 432
  38. theorem OAI.Erdos3.quarticCanonicalSample_of_first_one line 435
  39. theorem OAI.Erdos3.quarticCanonicalSample_of_first_zero line 450
  40. theorem OAI.Erdos3.quarticCorner_first_zero_of_ne_one line 465
  41. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRawCornerFactor line 483
  42. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticRawCornerFactor_norm line 488
  43. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCornerExchangeFactor line 493
  44. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCornerExchangeFactor_norm line 505
  45. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCornerExchangeFactor_mean_error line 532
  46. abbrev OAI.Erdos3.QuarticCornerBlock line 567
  47. def OAI.Erdos3.quarticBlockAssignment line 569
  48. theorem OAI.Erdos3.quarticBlockAssignment_nonzero line 576
  49. def OAI.Erdos3.quarticBlockCorner line 587
  50. theorem OAI.Erdos3.quarticBlockCorner_injective line 590
  51. def OAI.Erdos3.quarticBlockEquiv line 592
  52. theorem OAI.Erdos3.quarticBlockCorner_canonical line 597
  53. def OAI.Erdos3.quarticFifteenMerge line 612
  54. theorem OAI.Erdos3.quarticFifteenMerge_block line 616
  55. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticSymmetricFifteen line 636
  56. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticSymmetricFifteen_norm line 640
  57. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticSymmetricFifteen_unit line 645
  58. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticMixedFifteen_cross_symmetric line 653
  59. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticFifteenExchangeProduct line 661
  60. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticFifteenExchangeProduct_norm line 666
  61. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticFifteenExchangeProduct_mean_error line 680
  62. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticWrappedDiagonalCorrection line 719
  63. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCyclicDiagonalCorrection line 726
  64. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticWrappedDiagonalCorrection_mean_error line 734
  65. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticCyclicDiagonalCorrection_mean_error line 778
  66. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quarticCyclicDiagonalCorrection_expansion line 821