OAI/Combinatorics/BooleanFunctions/Walsh.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Bool encodes a sign: false is +1 and true is -1. The average is uniform, and degree is ordinary real Fourier degree, not F₂ degree or threshold degree.

  1. abbrev OAI.SquareRootDegree.Cube line 16

    Also declared: ComparatorChallenges/SquareRootDegree.lean:16 (same declaration text).

  2. def OAI.SquareRootDegree.sign line 18

    Also declared: ComparatorChallenges/SquareRootDegree.lean:18 (same declaration text).

  3. def OAI.SquareRootDegree.average line 20

    Also declared: ComparatorChallenges/SquareRootDegree.lean:20 (same declaration text).

  4. def OAI.SquareRootDegree.character line 23

    Also declared: ComparatorChallenges/SquareRootDegree.lean:23 (same declaration text).

  5. def OAI.SquareRootDegree.fourierCoeff line 26

    Also declared: ComparatorChallenges/SquareRootDegree.lean:26 (same declaration text).

  6. def OAI.SquareRootDegree.fourierDegree line 30

    Also declared: ComparatorChallenges/SquareRootDegree.lean:30 (same declaration text).

  7. def OAI.SquareRootDegree.IsBoolean line 34

    Also declared: ComparatorChallenges/SquareRootDegree.lean:34 (same declaration text).

  8. def OAI.SquareRootDegree.Nonconstant line 37

    Also declared: ComparatorChallenges/SquareRootDegree.lean:37 (same declaration text).

  9. def OAI.SquareRootDegree.singletonSum line 40

    Also declared: ComparatorChallenges/SquareRootDegree.lean:40 (same declaration text).

  10. def OAI.SquareRootDegree.absoluteSingletonSum line 43

    Also declared: ComparatorChallenges/SquareRootDegree.lean:43 (same declaration text).

  11. def OAI.SquareRootDegree.SignedViolations line 46

    Also declared: ComparatorChallenges/SquareRootDegree.lean:46 (same declaration text).

  12. def OAI.SquareRootDegree.AbsoluteRatios line 50

    Also declared: ComparatorChallenges/SquareRootDegree.lean:50 (same declaration text).

  13. theorem OAI.SquareRootDegree.sign_false line 59
  14. theorem OAI.SquareRootDegree.sign_true line 60
  15. theorem OAI.SquareRootDegree.sign_sq line 62
  16. theorem OAI.SquareRootDegree.sign_ne_zero line 65
  17. theorem OAI.SquareRootDegree.sign_xor line 68
  18. theorem OAI.SquareRootDegree.sign_injective line 71
  19. theorem OAI.SquareRootDegree.average_zero line 75
  20. theorem OAI.SquareRootDegree.average_add line 78
  21. theorem OAI.SquareRootDegree.average_sub line 82
  22. theorem OAI.SquareRootDegree.average_mul_const line 86
  23. theorem OAI.SquareRootDegree.average_const_mul line 90
  24. theorem OAI.SquareRootDegree.average_sum line 94
  25. theorem OAI.SquareRootDegree.average_const line 99
  26. theorem OAI.SquareRootDegree.average_nonneg line 103
  27. theorem OAI.SquareRootDegree.average_mono line 107
  28. theorem OAI.SquareRootDegree.average_equiv line 112
  29. theorem OAI.SquareRootDegree.character_empty line 116
  30. theorem OAI.SquareRootDegree.character_singleton line 119
  31. theorem OAI.SquareRootDegree.character_ne_zero line 122
  32. theorem OAI.SquareRootDegree.character_sq line 126
  33. def OAI.SquareRootDegree.reflection line 130
  34. theorem OAI.SquareRootDegree.reflection_involutive line 142
  35. theorem OAI.SquareRootDegree.character_reflection line 145
  36. theorem OAI.SquareRootDegree.fourierCoeff_reflection line 149
  37. theorem OAI.SquareRootDegree.fourierDegree_reflection line 163
  38. def OAI.SquareRootDegree.positiveMask line 169
  39. theorem OAI.SquareRootDegree.fourierCoeff_positive_reflection line 173
  40. theorem OAI.SquareRootDegree.singletonSum_positive_reflection line 183
  41. theorem OAI.SquareRootDegree.isBoolean_reflection line 188
  42. theorem OAI.SquareRootDegree.nonconstant_reflection line 191
  43. theorem OAI.SquareRootDegree.singletonSum_le_absoluteSingletonSum line 196
  44. theorem OAI.SquareRootDegree.character_kernel line 200
  45. theorem OAI.SquareRootDegree.fourier_inversion line 221
  46. theorem OAI.SquareRootDegree.fourierCoeff_eq_zero_of_degree_lt line 238
  47. theorem OAI.SquareRootDegree.fourierDegree_le_iff line 247
  48. theorem OAI.SquareRootDegree.positive_degree_of_nonconstant line 259
  49. theorem OAI.SquareRootDegree.coordinate_reflection line 277

    Source documentation

    Coordinate reflection exactly identifies the signed and absolute linear sums, without changing the ordinary real Fourier degree or Boolean/nonconstant status.

    theorem coordinate_reflection {ι : Type*} [Fintype ι] (f : Cube ι → ℝ)
    (hf : IsBoolean f) (hn : Nonconstant f) :
    ∃ g : Cube ι → ℝ, IsBoolean g ∧ Nonconstant g ∧
      fourierDegree g = fourierDegree f ∧ singletonSum g = absoluteSingletonSum f := by
…

    Mentions: OAI.SquareRootDegree.Cube, OAI.SquareRootDegree.IsBoolean, OAI.SquareRootDegree.Nonconstant, OAI.SquareRootDegree.fourierDegree, OAI.SquareRootDegree.singletonSum, OAI.SquareRootDegree.absoluteSingletonSum

  50. theorem OAI.SquareRootDegree.absolute_unbounded_of_signed line 285
  51. def OAI.SquareRootDegree.DependsOn line 307
  52. theorem OAI.SquareRootDegree.fourierCoeff_add line 310
  53. theorem OAI.SquareRootDegree.fourierCoeff_const_mul line 314
  54. theorem OAI.SquareRootDegree.fourierCoeff_sum line 319
  55. theorem OAI.SquareRootDegree.fourierDegree_sum_le line 324
  56. theorem OAI.SquareRootDegree.fourierDegree_const_mul_le line 334
  57. theorem OAI.SquareRootDegree.fourierCoeff_eq_zero_of_not_subset line 340
  58. theorem OAI.SquareRootDegree.fourierDegree_le_card_of_dependsOn line 358
  59. theorem OAI.SquareRootDegree.character_dependsOn line 365
  60. theorem OAI.SquareRootDegree.dependsOn_mul line 369
  61. theorem OAI.SquareRootDegree.fourierDegree_mul_le line 377
  62. theorem OAI.SquareRootDegree.fourierDegree_const line 416
  63. theorem OAI.SquareRootDegree.fourierDegree_prod_le line 421