OAI/Combinatorics/Progressions/Estimates/QuarticSurvivorMultilinearization.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_ternary_expansion_equivalence line 14
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_ternary_assignment_equivalence line 87
  3. abbrev OAI.Erdos3.QuarticReplicatedIndex line 131
  4. def OAI.Erdos3.quarticReplica line 133
  5. def OAI.Erdos3.quarticRepeatedCoordinates line 135
  6. def OAI.Erdos3.quarticInput line 138
  7. def OAI.Erdos3.quarticTernarySample line 141
  8. theorem OAI.Erdos3.quarticInput_diagonal line 144
  9. theorem OAI.Erdos3.quarticTernarySample_sum line 150
  10. theorem OAI.Erdos3.quarticTernarySample_leaf line 159
  11. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_ternary_expansion line 171
  12. abbrev OAI.Erdos3.QuarticBinaryAssignment line 216
  13. abbrev OAI.Erdos3.QuarticTernaryAssignment line 218
  14. abbrev OAI.Erdos3.QuarticSurvivor line 220
  15. def OAI.Erdos3.quarticBinaryWord line 223
  16. def OAI.Erdos3.quarticAssignmentMap line 226
  17. theorem OAI.Erdos3.quarticAssignmentMap_bijective line 231
  18. def OAI.Erdos3.quarticAssignmentEquiv line 234
  19. theorem OAI.Erdos3.quarticSurvivor_card line 238
  20. theorem OAI.Erdos3.quarticAssignmentMap_word line 241
  21. theorem OAI.Erdos3.quartic_assignment_product line 254
  22. def OAI.Erdos3.quarticBinarySample line 283
  23. theorem OAI.Erdos3.quarticBinarySample_sum line 287
  24. theorem OAI.Erdos3.quarticBinarySample_leaf line 296
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_binary_expansion line 313
  26. def OAI.Erdos3.quarticReflectionMatrix line 361
  27. def OAI.Erdos3.quarticReflectionOffset line 367
  28. theorem OAI.Erdos3.quarticReflectionInput_sum line 371
  29. theorem OAI.Erdos3.quarticReflectionInput_left line 383
  30. theorem OAI.Erdos3.quarticReflectionInput_right line 394
  31. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_second_multilinearization line 415
  32. def OAI.Erdos3.quarticPermutationWord line 469
  33. theorem OAI.Erdos3.quarticPermutationWord_bijective line 472
  34. def OAI.Erdos3.quarticWordPermutation line 475
  35. def OAI.Erdos3.quarticDoubleFirstWord line 478
  36. def OAI.Erdos3.quarticDoubleSecondWord line 481
  37. def OAI.Erdos3.quarticSurvivorClassMap line 484
  38. theorem OAI.Erdos3.quarticSurvivorClassMap_bijective line 489
  39. def OAI.Erdos3.quarticSurvivorClassEquiv line 492
  40. theorem OAI.Erdos3.quartic_survivor_class_product line 495
  41. def OAI.Erdos3.quarticTerm line 515
  42. def OAI.Erdos3.quarticFaceVector line 519
  43. def OAI.Erdos3.quarticCommonVector line 523
  44. def OAI.Erdos3.quarticSurvivorVector line 527
  45. theorem OAI.Erdos3.quarticFaceVector_unit line 531
  46. theorem OAI.Erdos3.quarticCommonVector_unit line 540
  47. theorem OAI.Erdos3.quarticSurvivorVector_unit line 546
  48. def OAI.Erdos3.quarticFaceCoordinate line 554
  49. theorem OAI.Erdos3.quarticFaceCoordinate_word line 557
  50. def OAI.Erdos3.quarticPartitionCoordinate line 562
  51. def OAI.Erdos3.quarticAssignmentReindex line 568
  52. theorem OAI.Erdos3.quartic_product_reindex line 574
  53. def OAI.Erdos3.quarticSecondVector line 584
  54. theorem OAI.Erdos3.quarticSecondVector_eq line 591
  55. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_face_expansion line 603
  56. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_diagonal_self_equivalence line 631
  57. def OAI.Erdos3.quarticFirstReplica line 660
  58. def OAI.Erdos3.quarticAllCoordinates line 662
  59. def OAI.Erdos3.quarticDiagonalSampleInput line 665
  60. def OAI.Erdos3.quarticDiagonalCorner line 669
  61. theorem OAI.Erdos3.quarticDiagonalCorner_zero line 672
  62. theorem OAI.Erdos3.quarticDiagonalSample_sum line 678
  63. theorem OAI.Erdos3.quarticDiagonalSample_leaf line 687
  64. def OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalTensor line 708
  65. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalTensor_norm line 712
  66. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.quarticDiagonalTensor_unit line 718
  67. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_survivor_equivalence line 737
  68. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quartic_survivor_multilinearization line 839