OAI/Combinatorics/Progressions/Geometry/SupportedCubeEquivTransport.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.cubeShift_false line 13
  2. def OAI.Erdos3.cubeAxis line 16
  3. theorem OAI.Erdos3.cubeShift_axis line 18
  4. theorem OAI.Erdos3.map_cubeShift line 21
  5. def OAI.Erdos3.ReflectsPairSums line 28
  6. theorem OAI.Erdos3.ReflectsPairSums.injOn line 32
  7. abbrev OAI.Erdos3.SupportedCube line 37
  8. theorem OAI.Erdos3.SupportedCube.base_mem line 40
  9. theorem OAI.Erdos3.SupportedCube.axis_mem line 43
  10. def OAI.Erdos3.SupportedCube.map line 47
  11. theorem OAI.Erdos3.SupportedCube.map_injective line 52
  12. theorem OAI.Erdos3.exists_lift_cube line 67
  13. theorem OAI.Erdos3.SupportedCube.map_surjective line 115
  14. def OAI.Erdos3.supportedCubeEquiv line 124
  15. def OAI.Erdos3.SupportedCube.points line 141
  16. theorem OAI.Erdos3.SupportedCube.points_injective line 144
  17. instance OAI.Erdos3.supportedCubeFinite line 156
  18. instance OAI.Erdos3.supportedCubeFintype line 159
  19. def OAI.Erdos3.supportedCubeSum line 162
  20. def OAI.Erdos3.supportedCubeFinsetEquiv line 170
  21. theorem OAI.Erdos3.card_supportedCube line 174
  22. theorem OAI.Erdos3.supportedCubeSum_eq_sum line 179
  23. theorem OAI.Erdos3.mixedCubeProduct_restrictTo line 186
  24. theorem OAI.Erdos3.mixedGowersMoment_restrict_eq_supportedCubeSum line 203
  25. theorem OAI.Erdos3.supportedCubeSum_eq_tsum line 222
  26. theorem OAI.Erdos3.card_supportedCube_le line 241
  27. def OAI.Erdos3.imageExtension line 259
  28. theorem OAI.Erdos3.imageExtension_apply line 263
  29. theorem OAI.Erdos3.imageExtension_eq_zero line 274
  30. theorem OAI.Erdos3.mixedCubeProduct_imageExtension line 281
  31. theorem OAI.Erdos3.restrictTo_imageExtension line 296
  32. theorem OAI.Erdos3.supportedCubeSum_imageExtension line 308
  33. theorem OAI.Erdos3.mixedGowersMoment_imageExtension line 318
  34. def OAI.Erdos3.cubeDifferenceSupport line 342
  35. theorem OAI.Erdos3.mem_cubeDifferenceSupport line 345
  36. theorem OAI.Erdos3.SupportedCube.first_mem_difference line 357
  37. def OAI.Erdos3.SupportedCube.tail line 362
  38. def OAI.Erdos3.SupportedCube.cons line 373
  39. def OAI.Erdos3.supportedCubeDerivativeEquiv line 383
  40. theorem OAI.Erdos3.card_supportedCube_succ line 396
  41. theorem OAI.Erdos3.supportedCubeSum_derivative line 404
  42. def OAI.Erdos3.finiteSupportGowersNorm line 437
  43. theorem OAI.Erdos3.supportedCubeSum_one line 441
  44. theorem OAI.Erdos3.finiteSupportGowersNorm_one line 447
  45. theorem OAI.Erdos3.imageExtension_add line 458
  46. theorem OAI.Erdos3.card_supportedCube_image line 470
  47. theorem OAI.Erdos3.gowersMoment_imageExtension_re line 477
  48. theorem OAI.Erdos3.restrictedGowersNorm_imageExtension_pow line 485
  49. theorem OAI.Erdos3.finiteSupportGowersNorm_eq_restricted line 496
  50. theorem OAI.Erdos3.finiteSupportGowersNorm_add_of_embedding line 505
  51. theorem OAI.Erdos3.norm_supportedCubeSum_le_of_embedding line 512
  52. theorem OAI.Erdos3.finiteSupportGowersNorm_ambient_comparison line 525
  53. theorem OAI.Erdos3.finiteSupportGowersNorm_degree_one_of_embedding line 534
  54. theorem OAI.Erdos3.ReflectsPairSums.mono line 560
  55. theorem OAI.Erdos3.card_supportedCube_pos line 565
  56. theorem OAI.Erdos3.sum_supportedCube_weights line 574
  57. theorem OAI.Erdos3.finiteSupportGowersNorm_pow_mul_count line 584
  58. theorem OAI.Erdos3.finiteSupportGowersNorm_derivative_mul_count line 594
  59. theorem OAI.Erdos3.finiteSupportGowersNorm_derivative line 613
  60. theorem OAI.Erdos3.supportedCubeSum_congr_on line 643
  61. theorem OAI.Erdos3.finiteSupportGowersNorm_congr_on line 654
  62. theorem OAI.Erdos3.reflectsPairSums_of_addEquiv line 659
  63. theorem OAI.Erdos3.card_supportedCube_image_eq line 666
  64. theorem OAI.Erdos3.finiteSupportGowersNorm_imageExtension line 671
  65. theorem OAI.Erdos3.finiteSupportGowersNorm_addEquiv line 678
  66. theorem OAI.Erdos3.finiteCorrelation_addEquiv line 690