OAI/Combinatorics/SquareDifference/WalshMoments.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LiftAnalysis.SquareDifference.sum_range_two line 17
  2. lemma OAI.LiftAnalysis.SquareDifference.choose_le_two_pow line 26
  3. lemma OAI.LiftAnalysis.SquareDifference.even_sum_binomial line 33
  4. lemma OAI.LiftAnalysis.SquareDifference.two_point_moment line 59
  5. lemma OAI.LiftAnalysis.SquareDifference.expect_pow_zero line 83
  6. lemma OAI.LiftAnalysis.SquareDifference.expect_add_pow_le line 92
  7. lemma OAI.LiftAnalysis.SquareDifference.expect_update_bool line 131
  8. lemma OAI.LiftAnalysis.SquareDifference.expect_bool line 145
  9. def OAI.LiftAnalysis.SquareDifference.boolSign line 148
  10. def OAI.LiftAnalysis.SquareDifference.walsh line 150
  11. def OAI.LiftAnalysis.SquareDifference.walshEnergy line 154
  12. lemma OAI.LiftAnalysis.SquareDifference.walsh_update line 157
  13. lemma OAI.LiftAnalysis.SquareDifference.walsh_insert line 170
  14. lemma OAI.LiftAnalysis.SquareDifference.walshEnergy_insert line 182
  15. lemma OAI.LiftAnalysis.SquareDifference.walshEnergy_nonneg line 194
  16. lemma OAI.LiftAnalysis.SquareDifference.walsh_hypercontractivity line 198
  17. lemma OAI.LiftAnalysis.SquareDifference.expect_update_dep line 233
  18. def OAI.LiftAnalysis.SquareDifference.patch line 248
  19. lemma OAI.LiftAnalysis.SquareDifference.patch_empty line 251
  20. lemma OAI.LiftAnalysis.SquareDifference.patch_univ line 254
  21. lemma OAI.LiftAnalysis.SquareDifference.patch_insert_update line 257
  22. def OAI.LiftAnalysis.SquareDifference.ExactSupport line 265
  23. lemma OAI.LiftAnalysis.SquareDifference.expect_pow_le line 271
  24. lemma OAI.LiftAnalysis.SquareDifference.expect_even_pow_le line 282
  25. lemma OAI.LiftAnalysis.SquareDifference.exactSupport_congr line 290
  26. def OAI.LiftAnalysis.SquareDifference.hybrid line 309
  27. def OAI.LiftAnalysis.SquareDifference.boolMul line 312
  28. lemma OAI.LiftAnalysis.SquareDifference.boolMul_symm line 314
  29. lemma OAI.LiftAnalysis.SquareDifference.boolMul_self line 316
  30. lemma OAI.LiftAnalysis.SquareDifference.boolSign_mul line 318
  31. lemma OAI.LiftAnalysis.SquareDifference.hybrid_hybrid line 321
  32. def OAI.LiftAnalysis.SquareDifference.copySwapEquiv line 326
  33. lemma OAI.LiftAnalysis.SquareDifference.expect_copySwap line 335
  34. lemma OAI.LiftAnalysis.SquareDifference.expect_hybrid line 343
  35. def OAI.LiftAnalysis.SquareDifference.boolMulEquiv line 349
  36. def OAI.LiftAnalysis.SquareDifference.boolChar line 355
  37. lemma OAI.LiftAnalysis.SquareDifference.boolChar_mul line 358
  38. lemma OAI.LiftAnalysis.SquareDifference.boolChar_sq line 362
  39. lemma OAI.LiftAnalysis.SquareDifference.exactSupport_hybrid_expect line 366
  40. lemma OAI.LiftAnalysis.SquareDifference.expect_prod_pi line 390
  41. lemma OAI.LiftAnalysis.SquareDifference.expect_prod_pi_finset line 397
  42. lemma OAI.LiftAnalysis.SquareDifference.bool_indicator_char line 408
  43. def OAI.LiftAnalysis.SquareDifference.copyDifference line 430
  44. lemma OAI.LiftAnalysis.SquareDifference.copyDifference_mean line 434
  45. lemma OAI.LiftAnalysis.SquareDifference.copyDifference_swap line 447
  46. lemma OAI.LiftAnalysis.SquareDifference.copyDifference_square line 459
  47. lemma OAI.LiftAnalysis.SquareDifference.sum_powerset_family line 468
  48. lemma OAI.LiftAnalysis.SquareDifference.walsh_family line 479
  49. lemma OAI.LiftAnalysis.SquareDifference.walshEnergy_family line 486
  50. lemma OAI.LiftAnalysis.SquareDifference.difference_energy_bound line 493