OAI/Combinatorics/Progressions/Estimates/BooleanCubeProduct.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.mixedGowersMoment line 13
  2. theorem OAI.Erdos3.mixedGowersMoment_const line 18
  3. theorem OAI.Erdos3.mixedGowersMoment_one line 24
  4. theorem OAI.Erdos3.norm_mixedGowersMoment_le line 29
  5. def OAI.Erdos3.booleanWeight line 77
  6. theorem OAI.Erdos3.booleanWeight_cons_false line 80
  7. theorem OAI.Erdos3.booleanWeight_cons_true line 86
  8. def OAI.Erdos3.cubeShift line 94
  9. theorem OAI.Erdos3.cubeShift_cons_false line 97
  10. theorem OAI.Erdos3.cubeShift_cons_true line 101
  11. def OAI.Erdos3.mixedCubeProduct line 105
  12. theorem OAI.Erdos3.mixedCubeProduct_zero line 108
  13. theorem OAI.Erdos3.mixedCubeProduct_cons line 114
  14. theorem OAI.Erdos3.mixedCubeProduct_crossDerivative line 128
  15. theorem OAI.Erdos3.mixedGowersMoment_eq_expect_cube line 144
  16. theorem OAI.Erdos3.mixedGowersMoment_sum line 152
  17. theorem OAI.Erdos3.norm_gowersMoment line 172
  18. theorem OAI.Erdos3.gowersNorm_sum line 181
  19. theorem OAI.Erdos3.gowersNorm_add line 203
  20. theorem OAI.Erdos3.gowersMoment_translate line 221
  21. theorem OAI.Erdos3.gowersNorm_translate line 232
  22. theorem OAI.Erdos3.multiplicativeDerivative_const_mul line 237
  23. theorem OAI.Erdos3.gowersNorm_const_mul line 244
  24. theorem OAI.Erdos3.gowersNorm_le_succ line 261
  25. theorem OAI.Erdos3.norm_expect_le_gowersNorm line 281
  26. theorem OAI.Erdos3.gowersNorm_mul_character line 287
  27. theorem OAI.Erdos3.gowersNorm_const line 308
  28. theorem OAI.Erdos3.gowersNorm_zero line 313
  29. theorem OAI.Erdos3.gowersNorm_neg line 317
  30. theorem OAI.Erdos3.gowersNorm_sub_le line 321
  31. theorem OAI.Erdos3.norm_gowersMoment_le_mean_norm line 338
  32. theorem OAI.Erdos3.gowersNorm_pow_le_mean_norm line 357
  33. theorem OAI.Erdos3.gowersNorm_le_of_mean_norm_le_pow line 362
  34. def OAI.Erdos3.restrictTo line 380
  35. theorem OAI.Erdos3.restrictTo_empty line 384
  36. theorem OAI.Erdos3.expect_restrictTo line 390
  37. theorem OAI.Erdos3.norm_expect_restrict_one line 395
  38. theorem OAI.Erdos3.gowersNorm_restrict_one_pos line 400
  39. def OAI.Erdos3.restrictedGowersNorm line 408
  40. theorem OAI.Erdos3.restrictedGowersNorm_nonneg line 411
  41. theorem OAI.Erdos3.restrictedGowersNorm_one line 415
  42. theorem OAI.Erdos3.restrictedGowersNorm_degree_one line 419
  43. theorem OAI.Erdos3.gowersNorm_restrict_pow line 428
  44. theorem OAI.Erdos3.restrictTo_add line 439
  45. theorem OAI.Erdos3.restrictedGowersNorm_add line 444
  46. theorem OAI.Erdos3.norm_mixedGowersMoment_restrict_le line 451
  47. theorem OAI.Erdos3.multiplicativeDerivative_norm_le_one line 475
  48. theorem OAI.Erdos3.gowersNorm_le_one line 482
  49. def OAI.Erdos3.derivativeInverseBudget line 488
  50. theorem OAI.Erdos3.derivativeInverseBudget_ge_two line 490
  51. theorem OAI.Erdos3.exists_many_large_gowers_derivatives line 495
  52. def OAI.Erdos3.groupCubeSet line 549
  53. def OAI.Erdos3.groupCubeCount line 552
  54. theorem OAI.Erdos3.mixedCubeProduct_indicator line 555
  55. theorem OAI.Erdos3.gowersMoment_indicator_eq_cubeCount line 569
  56. theorem OAI.Erdos3.gowersMoment_indicator_re line 583
  57. theorem OAI.Erdos3.gowersNorm_restrict_cubeCount line 590
  58. theorem OAI.Erdos3.card_le_groupCubeCount line 596
  59. theorem OAI.Erdos3.groupCubeCount_pos line 612
  60. theorem OAI.Erdos3.cubeProduct_norm_le_one line 625
  61. theorem OAI.Erdos3.cubeProduct_mul line 633
  62. theorem OAI.Erdos3.cubeProduct_star line 641
  63. theorem OAI.Erdos3.cubeProduct_tuple_cons line 649
  64. def OAI.Erdos3.additiveQuadrupleCorrelation line 667
  65. theorem OAI.Erdos3.derivative_correlations_force_additive_quadruples line 670
  66. theorem OAI.Erdos3.additiveQuadrupleCorrelation_le_one line 707
  67. theorem OAI.Erdos3.derivative_correlation_energy_exchange line 729
  68. theorem OAI.Erdos3.exists_many_exchanged_derivative_correlations line 751
  69. theorem OAI.Erdos3.conjugationPower_norm line 819
  70. theorem OAI.Erdos3.cubeProduct_eq_mixedCubeProduct line 826
  71. theorem OAI.Erdos3.cubeProduct_eq_boolean_product line 835