theorem CryptBoolean.mem_rawFourierSupport {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (u : FABL.F₂Cube n) :
  u ∈ CryptBoolean.rawFourierSupport φ ↔
    CryptBoolean.rawFourierTransform φ u ≠
      0

theorem CryptBoolean.mem_rawFourierSupport_iff_vectorFourierCoeff_ne_zero
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (u : FABL.F₂Cube n) :
  u ∈ CryptBoolean.rawFourierSupport φ ↔
    FABL.vectorFourierCoeff φ u ≠ 0

theorem CryptBoolean.mem_indexedRawFourierSupport.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (φ : FABL.IndexedSignCube ι → ℝ)
  (S : Finset ι) :
  S ∈
      CryptBoolean.indexedRawFourierSupport
        φ ↔
    CryptBoolean.indexedRawFourierTransform
        φ S ≠
      0

theorem CryptBoolean.indexedRawFourierTransform_eq_card_mul_indexedFourierCoeff.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (φ : FABL.IndexedSignCube ι → ℝ)
  (S : Finset ι) :
  CryptBoolean.indexedRawFourierTransform
      φ S =
    ↑(Fintype.card
          (FABL.IndexedSignCube ι)) *
      FABL.indexedFourierCoeff φ S

theorem CryptBoolean.mem_indexedRawFourierSupport_iff_indexedFourierCoeff_ne_zero.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (φ : FABL.IndexedSignCube ι → ℝ)
  (S : Finset ι) :
  S ∈
      CryptBoolean.indexedRawFourierSupport
        φ ↔
    FABL.indexedFourierCoeff φ S ≠ 0

theorem CryptBoolean.card_indexedRawFourierSupport_signRestriction_le
  {n : ℕ} (φ : FABL.SignCube n → ℝ)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  (CryptBoolean.indexedRawFourierSupport
        (FABL.signRestriction φ J
          z)).card ≤
    (CryptBoolean.indexedRawFourierSupport
        φ).card

theorem CryptBoolean.card_indexedRawFourierSupport_binaryFunctionOnSignCube
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  (CryptBoolean.indexedRawFourierSupport
        (FABL.binaryFunctionOnSignCube
          φ)).card =
    (CryptBoolean.rawFourierSupport
        φ).card

theorem CryptBoolean.card_rawFourierSupport_coordinateRestriction_le
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  (CryptBoolean.indexedRawFourierSupport
        (FABL.signRestriction
          (FABL.binaryFunctionOnSignCube
            φ)
          J z)).card ≤
    (CryptBoolean.rawFourierSupport
        φ).card

theorem CryptBoolean.two_pow_functionAlgebraicDegree_le_card_rawFourierSupport_booleanRealEmbedding
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : f ≠ 0) :
  2 ^ FABL.functionAlgebraicDegree f ≤
    (CryptBoolean.rawFourierSupport
        (FABL.booleanRealEmbedding
          f)).card

theorem FABL.mem_numericalSupport {n : ℕ}
  (c : FABL.NumericalCoefficients n)
  (S : Finset (Fin n)) :
  S ∈ FABL.numericalSupport c ↔ c S ≠ 0

theorem FABL.numericalDegree_le_iff {n : ℕ}
  (c : FABL.NumericalCoefficients n)
  (D : ℕ) :
  FABL.numericalDegree c ≤ D ↔
    ∀ (S : Finset (Fin n)),
      c S ≠ 0 → S.card ≤ D

theorem CryptBoolean.numericalMonomial_eq_setIndicator_coordinateSubcube
  {n : ℕ} (S : Finset (Fin n)) :
  FABL.numericalMonomial S =
    FABL.setIndicator
      (FABL.F₂DecisionTree.coordinateSubcube
        S (FABL.f₂CubeOfFinset S))

theorem CryptBoolean.f₂Support_subset_of_vectorFourierCoeff_numericalMonomial_ne_zero
  {n : ℕ} (S : Finset (Fin n))
  (u : FABL.F₂Cube n)
  (hu :
    FABL.vectorFourierCoeff
        (FABL.numericalMonomial S) u ≠
      0) :
  FABL.f₂Support u ⊆ S

theorem CryptBoolean.vectorFourierCoeff_numericalEval
  {n : ℕ}
  (c : FABL.NumericalCoefficients n)
  (u : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.numericalEval c) u =
    ∑ S,
      c S *
        FABL.vectorFourierCoeff
          (FABL.numericalMonomial S) u

theorem CryptBoolean.f₂Support_card_le_functionNumericalDegree_of_mem_rawFourierSupport
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (u : FABL.F₂Cube n)
  (hu :
    u ∈
      CryptBoolean.rawFourierSupport φ) :
  (FABL.f₂Support u).card ≤
    FABL.functionNumericalDegree φ

theorem CryptBoolean.card_lowWeightInputs
  (n D : ℕ) :
  (CryptBoolean.lowWeightInputs D).card =
    ∑ i ∈ Finset.range (D + 1), n.choose i

theorem CryptBoolean.card_rawFourierSupport_le_sum_choose_functionNumericalDegree
  {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  (CryptBoolean.rawFourierSupport
        φ).card ≤
    ∑
      i ∈
        Finset.range
          (FABL.functionNumericalDegree
              φ +
            1),
      n.choose i

theorem CryptBoolean.vectorFourierCoeff_booleanRealEmbedding_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.booleanRealEmbedding f) a =
    ((if FABL.f₂Support a = ∅ then 1
        else 0) -
        FABL.vectorFourierCoeff
          (CryptBoolean.realSignView f)
          a) /
      2

theorem CryptBoolean.functionAlgebraicDegree_le_of_two_pow_dvd_walshTransform
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) (_hn : 2 ≤ n) (_hk : 1 ≤ k)
  (hkn : k ≤ n)
  (hdiv :
    ∀ (a : FABL.F₂Cube n),
      2 ^ k ∣
        CryptBoolean.walshTransform f a) :
  FABL.functionAlgebraicDegree f ≤
    n - k + 1