OAI/Combinatorics/Progressions/Estimates/CorrelationDerivative.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.multiplicativeDerivative line 16
  2. def OAI.Erdos3.gowersMoment line 19
  3. theorem OAI.Erdos3.expect_star line 24
  4. theorem OAI.Erdos3.expect_re line 28
  5. theorem OAI.Erdos3.expect_im line 32
  6. theorem OAI.Erdos3.expect_translate line 35
  7. theorem OAI.Erdos3.multiplicativeDerivative_comm line 39
  8. theorem OAI.Erdos3.gowersMoment_one line 47
  9. theorem OAI.Erdos3.gowersMoment_re_nonneg line 59
  10. theorem OAI.Erdos3.gowersMoment_im_zero line 71
  11. theorem OAI.Erdos3.gowersMoment_const_one line 82
  12. def OAI.Erdos3.gowersNorm line 93
  13. theorem OAI.Erdos3.gowersNorm_nonneg line 96
  14. theorem OAI.Erdos3.gowersNorm_pow line 99
  15. theorem OAI.Erdos3.gowersNorm_one line 104
  16. theorem OAI.Erdos3.gowersNorm_const_one line 115
  17. theorem OAI.Erdos3.gowersNorm_derivative line 118
  18. def OAI.Erdos3.conjugationPower line 134
  19. theorem OAI.Erdos3.conjugationPower_star line 138
  20. def OAI.Erdos3.cubeProduct line 148
  21. theorem OAI.Erdos3.cubeProduct_nil line 151
  22. theorem OAI.Erdos3.cubeProduct_cons line 154
  23. theorem OAI.Erdos3.cubeProduct_derivative line 164
  24. theorem OAI.Erdos3.cubeProduct_cons_eq_derivative line 174
  25. def OAI.Erdos3.cubeAverage line 180
  26. theorem OAI.Erdos3.cubeAverage_eq_expect_tuple line 187
  27. theorem OAI.Erdos3.cubeAverage_re line 202
  28. theorem OAI.Erdos3.cubeAverage_comm_expect line 207
  29. theorem OAI.Erdos3.cubeAverage_norm_inner_sq_le line 214
  30. theorem OAI.Erdos3.gowersMoment_eq_cubeAverage line 220
  31. theorem OAI.Erdos3.expect_pair_sub_real line 239
  32. theorem OAI.Erdos3.gowersNorm_pow_lower_of_pair_detector line 249
  33. theorem OAI.Erdos3.exists_quartic_diagonal_weights line 286
  34. def OAI.Erdos3.FiniteProbabilityWeights.complexMean line 360
  35. theorem OAI.Erdos3.FiniteProbabilityWeights.correlation_eq_complexMean line 362
  36. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_eq_correlation_one line 365
  37. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_mul_left line 369
  38. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_re line 377
  39. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_complexMean_sq_le line 381
  40. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_norm_sq_le_one line 387
  41. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_correlation_le_one line 392
  42. theorem OAI.Erdos3.FiniteProbabilityWeights.correlation_mul_phases line 399
  43. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_correlation_mul_phases line 409
  44. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_average line 416
  45. theorem OAI.Erdos3.FiniteProbabilityWeights.correlation_average_left line 422
  46. theorem OAI.Erdos3.FiniteProbabilityWeights.correlation_average_right line 428
  47. def OAI.Erdos3.finiteWeightedTest line 444
  48. theorem OAI.Erdos3.finiteWeightedTest_real line 455
  49. theorem OAI.Erdos3.finite_weighted_model_score_transfer line 463
  50. def OAI.Erdos3.crossDerivative line 492
  51. theorem OAI.Erdos3.crossDerivative_self line 496
  52. theorem OAI.Erdos3.cubeProduct_crossDerivative line 500
  53. theorem OAI.Erdos3.expect_crossDerivative line 510
  54. theorem OAI.Erdos3.expect_gowersMoment_crossDerivative line 521
  55. theorem OAI.Erdos3.mul_star_re_eq_norm_sq line 534
  56. theorem OAI.Erdos3.gowersMoment_eq_average_square line 538
  57. theorem OAI.Erdos3.norm_expect_gowersMoment_crossDerivative_sq_le line 546
  58. theorem OAI.Erdos3.expect_cross_gowersNorm_pow_le line 553
  59. def OAI.Erdos3.FiniteProbabilityWeights.pi line 587
  60. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_pi_product line 599
  61. theorem OAI.Erdos3.FiniteProbabilityWeights.correlation_pi_product line 608
  62. theorem OAI.Erdos3.density_large_values_of_expect line 628
  63. theorem OAI.Erdos3.correlation_sq_eq_expect_derivative line 646
  64. theorem OAI.Erdos3.correlation_sq_le_expect_norm_derivative line 665
  65. theorem OAI.Erdos3.norm_derivativeCorrelation_le line 672
  66. theorem OAI.Erdos3.density_correlating_derivatives line 685