theorem CryptBoolean.rawFourierTransform_eq_two_pow_mul_vectorFourierCoeff
  {n : ℕ} (φ : FABL.F₂Cube n → ℝ)
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform φ a =
    2 ^ n * FABL.vectorFourierCoeff φ a

theorem CryptBoolean.vectorFourierCoeff_mul_vectorWalshCharacter
  {n : ℕ} (φ : FABL.F₂Cube n → ℝ)
  (a u : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (fun x =>
        (FABL.vectorWalshCharacter a) x *
          φ x)
      u =
    FABL.vectorFourierCoeff φ (a + u)

theorem CryptBoolean.rawFourierTransform_modulate_translate
  {n : ℕ} (φ : FABL.F₂Cube n → ℝ)
  (a b u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (fun x =>
        (FABL.vectorWalshCharacter a) x *
          φ (x + b))
      u =
    (FABL.vectorWalshCharacter (a + u))
        b *
      CryptBoolean.rawFourierTransform φ
        (a + u)

theorem CryptBoolean.rawFourierTransform_involution
  {n : ℕ} (φ : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (CryptBoolean.rawFourierTransform φ)
      x =
    2 ^ n * φ x

theorem CryptBoolean.two_pow_mul_inversePerpendicularCard_eq_card
  {n : ℕ}
  (E :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  2 ^ n *
      FABL.inversePerpendicularCard E =
    ↑(Nat.card ↥E)

theorem CryptBoolean.rawFourierTransform_setIndicator_submodule
  {n : ℕ}
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (u : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (FABL.setIndicator ↑E) u =
    if
        u ∈
          FABL.perpendicularSubspace
            E then
      ↑(Nat.card ↥E)
    else 0

theorem FABL.poissonSummationFormula {n : ℕ}
  (f : FABL.F₂Cube n → ℝ)
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (z : FABL.F₂Cube n) :
  (Finset.univ.expect fun h =>
      f (↑h + z)) =
    ∑ γ,
      (FABL.vectorWalshCharacter ↑γ) z *
        FABL.vectorFourierCoeff f ↑γ

theorem CryptBoolean.rawPoissonSummationFormula
  {n : ℕ} (φ : FABL.F₂Cube n → ℝ)
  (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a b : FABL.F₂Cube n) :
  ∑ u,
      (FABL.vectorWalshCharacter b)
          (a + ↑u) *
        CryptBoolean.rawFourierTransform φ
          (a + ↑u) =
    ↑(Nat.card ↥E) *
        (FABL.vectorWalshCharacter b) a *
      ∑ x,
        (FABL.vectorWalshCharacter a)
            (b + ↑x) *
          φ (b + ↑x)

theorem CryptBoolean.rawConvolution_eq_two_pow_mul_convolution
  {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  CryptBoolean.rawConvolution φ ψ x =
    2 ^ n * FABL.convolution φ ψ x

theorem CryptBoolean.rawFourierTransform_rawConvolution
  {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ)
  (a : FABL.F₂Cube n) :
  CryptBoolean.rawFourierTransform
      (CryptBoolean.rawConvolution φ ψ)
      a =
    CryptBoolean.rawFourierTransform φ a *
      CryptBoolean.rawFourierTransform ψ a

theorem CryptBoolean.sum_rawFourierTransform_mul
  {n : ℕ} (φ ψ : FABL.F₂Cube n → ℝ) :
  ∑ a,
      CryptBoolean.rawFourierTransform φ
          a *
        CryptBoolean.rawFourierTransform ψ
          a =
    2 ^ n * ∑ x, φ x * ψ x

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

theorem CryptBoolean.mem_rawFourierSupport_iff_vectorFourierCoeff_ne_zero
  {n : ℕ}
  (φ :
    CryptBoolean.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 : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction
      n) :
  (CryptBoolean.indexedRawFourierSupport
        (FABL.binaryFunctionOnSignCube
          φ)).card =
    (CryptBoolean.rawFourierSupport
        φ).card

theorem CryptBoolean.card_rawFourierSupport_coordinateRestriction_le
  {n : ℕ}
  (φ :
    CryptBoolean.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 ^
      CryptBoolean.functionAlgebraicDegree
        f ≤
    (CryptBoolean.rawFourierSupport
        (CryptBoolean.booleanRealEmbedding
          f)).card

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

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

theorem CryptBoolean.numericalMonomial_eq_setIndicator_coordinateSubcube
  {n : ℕ} (S : Finset (Fin n)) :
  CryptBoolean.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
        (CryptBoolean.numericalMonomial S)
        u ≠
      0) :
  FABL.f₂Support u ⊆ S

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

theorem CryptBoolean.f₂Support_card_le_functionNumericalDegree_of_mem_rawFourierSupport
  {n : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction n)
  (u : FABL.F₂Cube n)
  (hu :
    u ∈
      CryptBoolean.rawFourierSupport φ) :
  (FABL.f₂Support u).card ≤
    CryptBoolean.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 : ℕ}
  (φ :
    CryptBoolean.PseudoBooleanFunction
      n) :
  (CryptBoolean.rawFourierSupport
        φ).card ≤
    ∑
      i ∈
        Finset.range
          (CryptBoolean.functionNumericalDegree
              φ +
            1),
      n.choose i