OAI/Combinatorics/SquareDifference/LiftMoments.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LiftTheory.SquareDifference.sum_range_two line 21
  2. lemma OAI.LiftTheory.SquareDifference.choose_le_two_pow line 30
  3. lemma OAI.LiftTheory.SquareDifference.even_sum_binomial line 37
  4. lemma OAI.LiftTheory.SquareDifference.two_point_moment line 63
  5. lemma OAI.LiftTheory.SquareDifference.expect_pow_zero line 87
  6. lemma OAI.LiftTheory.SquareDifference.expect_add_pow_le line 96
  7. lemma OAI.LiftTheory.SquareDifference.expect_update_bool line 135
  8. lemma OAI.LiftTheory.SquareDifference.expect_bool line 149
  9. def OAI.LiftTheory.SquareDifference.boolSign line 152
  10. def OAI.LiftTheory.SquareDifference.walsh line 154
  11. def OAI.LiftTheory.SquareDifference.walshEnergy line 158
  12. lemma OAI.LiftTheory.SquareDifference.walsh_update line 161
  13. lemma OAI.LiftTheory.SquareDifference.walsh_insert line 174
  14. lemma OAI.LiftTheory.SquareDifference.walshEnergy_insert line 186
  15. lemma OAI.LiftTheory.SquareDifference.walshEnergy_nonneg line 198
  16. lemma OAI.LiftTheory.SquareDifference.walsh_hypercontractivity line 202
  17. lemma OAI.LiftTheory.SquareDifference.expect_update_dep line 237
  18. def OAI.LiftTheory.SquareDifference.patch line 252
  19. lemma OAI.LiftTheory.SquareDifference.patch_empty line 255
  20. lemma OAI.LiftTheory.SquareDifference.patch_univ line 258
  21. lemma OAI.LiftTheory.SquareDifference.patch_insert_update line 261
  22. def OAI.LiftTheory.SquareDifference.ExactSupport line 269
  23. lemma OAI.LiftTheory.SquareDifference.expect_pow_le line 275
  24. lemma OAI.LiftTheory.SquareDifference.expect_even_pow_le line 286
  25. lemma OAI.LiftTheory.SquareDifference.exactSupport_congr line 294
  26. def OAI.LiftTheory.SquareDifference.hybrid line 313
  27. def OAI.LiftTheory.SquareDifference.boolMul line 316
  28. lemma OAI.LiftTheory.SquareDifference.boolMul_symm line 318
  29. lemma OAI.LiftTheory.SquareDifference.boolMul_self line 320
  30. lemma OAI.LiftTheory.SquareDifference.boolSign_mul line 322
  31. lemma OAI.LiftTheory.SquareDifference.hybrid_hybrid line 325
  32. def OAI.LiftTheory.SquareDifference.copySwapEquiv line 330
  33. lemma OAI.LiftTheory.SquareDifference.expect_copySwap line 339
  34. lemma OAI.LiftTheory.SquareDifference.expect_hybrid line 347
  35. def OAI.LiftTheory.SquareDifference.boolMulEquiv line 353
  36. def OAI.LiftTheory.SquareDifference.boolChar line 359
  37. lemma OAI.LiftTheory.SquareDifference.boolChar_mul line 362
  38. lemma OAI.LiftTheory.SquareDifference.boolChar_sq line 366
  39. lemma OAI.LiftTheory.SquareDifference.exactSupport_hybrid_expect line 370
  40. lemma OAI.LiftTheory.SquareDifference.expect_prod_pi line 394
  41. lemma OAI.LiftTheory.SquareDifference.expect_prod_pi_finset line 401
  42. lemma OAI.LiftTheory.SquareDifference.bool_indicator_char line 412
  43. def OAI.LiftTheory.SquareDifference.copyDifference line 434
  44. lemma OAI.LiftTheory.SquareDifference.copyDifference_mean line 438
  45. lemma OAI.LiftTheory.SquareDifference.copyDifference_swap line 451
  46. lemma OAI.LiftTheory.SquareDifference.copyDifference_square line 463
  47. lemma OAI.LiftTheory.SquareDifference.sum_powerset_family line 472
  48. lemma OAI.LiftTheory.SquareDifference.walsh_family line 483
  49. lemma OAI.LiftTheory.SquareDifference.walshEnergy_family line 490
  50. lemma OAI.LiftTheory.SquareDifference.difference_energy_bound line 497