theorem FABL.fourierDegree_parityFunction_univ
  {n : ℕ} :
  FABL.fourierDegree
      (FABL.parityFunction
          Finset.univ).toReal =
    n

theorem FABL.booleanFunctionF₂Encoding_parityFunction
  {n : ℕ} (S : Finset (Fin n)) :
  FABL.booleanFunctionF₂Encoding
      (FABL.parityFunction S) =
    ⇑(FABL.coordinateSum S)

theorem FABL.functionAlgebraicDegree_booleanFunctionF₂Encoding_parityFunction_univ
  {n : ℕ} (hn : 0 < n) :
  FABL.functionAlgebraicDegree
      (FABL.booleanFunctionF₂Encoding
        (FABL.parityFunction
          Finset.univ)) =
    1

theorem FABL.f₂PointIndicator_eq_ite {n : ℕ}
  (a x : FABL.F₂Cube n) :
  FABL.f₂PointIndicator a x =
    if x = a then 1 else 0

theorem FABL.f₂Interpolation {n : ℕ}
  (f : FABL.F₂BooleanFunction n)
  (x : FABL.F₂Cube n) :
  ∑ a, f a * FABL.f₂PointIndicator a x =
    f x

theorem FABL.threeBitParity_integer_interpolation
  (x₁ x₂ x₃ : ℤ) :
  (1 - x₁) * (1 - x₂) * x₃ +
          (1 - x₁) * x₂ * (1 - x₃) +
        x₁ * (1 - x₂) * (1 - x₃) +
      x₁ * x₂ * x₃ =
    x₁ + x₂ + x₃ -
        2 *
          (x₁ * x₂ + x₁ * x₃ + x₂ * x₃) +
      4 * (x₁ * x₂ * x₃)

theorem FABL.threeBitParity_f₂_interpolation
  (x₁ x₂ x₃ : FABL.𝔽₂) :
  (1 - x₁) * (1 - x₂) * x₃ +
          (1 - x₁) * x₂ * (1 - x₃) +
        x₁ * (1 - x₂) * (1 - x₃) +
      x₁ * x₂ * x₃ =
    x₁ + x₂ + x₃

theorem FABL.anfEval_anfCoeff {n : ℕ}
  (f : FABL.F₂BooleanFunction n) :
  FABL.anfEval (FABL.anfCoeff f) = f

theorem FABL.anfEval_injective {n : ℕ}
  {c d : FABL.ANFCoefficients n}
  (h : FABL.anfEval c = FABL.anfEval d) :
  c = d

theorem FABL.existsUnique_anfEval {n : ℕ}
  (f : FABL.F₂BooleanFunction n) :
  ∃! c, FABL.anfEval c = f

theorem FABL.f₂AndFunction_apply {n : ℕ}
  (x : FABL.F₂Cube n) :
  FABL.f₂AndFunction n x = ∏ i, x i

theorem FABL.functionAlgebraicDegree_f₂AndFunction
  {n : ℕ} :
  FABL.functionAlgebraicDegree
      (FABL.f₂AndFunction n) =
    n

theorem FABL.innerProductModTwoBit_joinF₂CubeBlocks_eq_sum
  {n : ℕ} (x y : FABL.F₂Cube n) :
  FABL.innerProductModTwoBit
      (FABL.joinF₂CubeBlocks x y) =
    ∑ i, x i * y i

theorem FABL.innerProductModTwoBit_eq_sum_anfMonomial
  (n : ℕ) :
  FABL.innerProductModTwoBit =
    ∑ i,
      FABL.anfMonomial
        {Fin.castAdd n i, Fin.natAdd n i}

theorem FABL.functionAlgebraicDegree_innerProductModTwoBit
  (n : ℕ) (hn : 0 < n) :
  FABL.functionAlgebraicDegree
      FABL.innerProductModTwoBit =
    2

theorem FABL.existsUnique_numericalEval {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n) :
  ∃! c, FABL.numericalEval c = φ

theorem FABL.numericalCoeff_eq_mobius_sum {n : ℕ}
  (φ : FABL.PseudoBooleanFunction n)
  (S : Finset (Fin n)) :
  FABL.numericalCoeff φ S =
    ∑ T ∈ S.powerset,
      (-1) ^ (S.card - T.card) *
        φ (FABL.f₂CubeOfFinset T)

theorem FABL.functionAlgebraicDegree_eq_dimension_iff_zero_or_card_f₂OneSupport_odd
  {n : ℕ} (f : FABL.F₂BooleanFunction n) :
  FABL.functionAlgebraicDegree f = n ↔
    n = 0 ∨ Odd (FABL.f₂OneSupport f).card

theorem FABL.functionAlgebraicDegree_eq_dimension_iff_card_f₂OneSupport_odd
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (hn : 0 < n) :
  FABL.functionAlgebraicDegree f = n ↔
    Odd (FABL.f₂OneSupport f).card

theorem FABL.signEncode_booleanFunctionF₂Encoding
  {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  FABL.signEncode
      (FABL.booleanFunctionF₂Encoding f
        x) =
    f ((FABL.binaryCubeSignEquiv n) x)

theorem FABL.booleanRealEmbedding_booleanFunctionF₂Encoding_apply
  {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.F₂Cube n) :
  FABL.booleanRealEmbedding
      (FABL.booleanFunctionF₂Encoding f)
      x =
    (1 -
        f.toReal
          ((FABL.binaryCubeSignEquiv n)
            x)) /
      2

theorem FABL.binaryFunctionOnSignCube_booleanRealEmbedding_booleanFunctionF₂Encoding
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.binaryFunctionOnSignCube
      (FABL.booleanRealEmbedding
        (FABL.booleanFunctionF₂Encoding
          f)) =
    fun x => (1 - f.toReal x) / 2

theorem FABL.numericalEval_fourierSubstitutionCoeff
  {n : ℕ} (p : FABL.SignCube n → ℝ) :
  FABL.numericalEval
      (FABL.fourierSubstitutionCoeff p) =
    FABL.fourierSubstitution p

theorem FABL.numericalCoeff_fourierToF₂Polynomial
  {n : ℕ} (p : FABL.SignCube n → ℝ) :
  FABL.numericalCoeff
      (FABL.fourierToF₂Polynomial p) =
    FABL.fourierToF₂Coeff p

theorem FABL.numericalDegree_fourierSubstitutionCoeff
  {n : ℕ} (p : FABL.SignCube n → ℝ) :
  FABL.numericalDegree
      (FABL.fourierSubstitutionCoeff p) =
    FABL.fourierDegree p

theorem FABL.numericalDegree_fourierToF₂Coeff
  {n : ℕ} (p : FABL.SignCube n → ℝ) :
  FABL.numericalDegree
      (FABL.fourierToF₂Coeff p) =
    FABL.fourierDegree p

theorem FABL.numericalCoeff_booleanRealEmbedding_eq_intCast
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (S : Finset (Fin n)) :
  FABL.numericalCoeff
      (FABL.booleanRealEmbedding f) S =
    ↑(FABL.booleanNumericalCoeffInt f S)

theorem FABL.booleanNumericalCoeffInt_cast_f₂_eq_anfCoeff
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (S : Finset (Fin n)) :
  ↑(FABL.booleanNumericalCoeffInt f S) =
    FABL.anfCoeff f S

theorem FABL.algebraicDegree_intCastModTwo_le_numericalDegree
  {n : ℕ} (z : Finset (Fin n) → ℤ) :
  (FABL.algebraicDegree fun S => ↑(z S)) ≤
    FABL.numericalDegree fun S => ↑(z S)

theorem FABL.functionAlgebraicDegree_booleanFunctionF₂Encoding_le_fourierDegree_viaPolynomial
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.functionAlgebraicDegree
      (FABL.booleanFunctionF₂Encoding f) ≤
    FABL.fourierDegree f.toReal

theorem FABL.functionAlgebraicDegree_booleanFunctionF₂Encoding_le_fourierDegree
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.functionAlgebraicDegree
      (FABL.booleanFunctionF₂Encoding f) ≤
    FABL.fourierDegree f.toReal

theorem FABL.functionAlgebraicDegree_booleanFunctionF₂Encoding_le_of_isResilient
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℕ) (hf : FABL.IsResilient k f)
  (hk : k < n - 1) :
  FABL.functionAlgebraicDegree
      (FABL.booleanFunctionF₂Encoding f) ≤
    n - k - 1

theorem FABL.functionAlgebraicDegree_booleanFunctionF₂Encoding_le_of_isCorrelationImmune
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℕ)
  (hf : FABL.IsCorrelationImmune k f)
  (hk : k < n) :
  FABL.functionAlgebraicDegree
      (FABL.booleanFunctionF₂Encoding f) ≤
    n - k

theorem FABL.fourierCoeff_pointwise_mul {n : ℕ}
  (f g : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff (fun x => f x * g x)
      S =
    ∑ T,
      FABL.fourierCoeff f (symmDiff T S) *
        FABL.fourierCoeff g T

theorem FABL.fourierCoeff_sq_eq_two_mul_empty_mul_of_large_support
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) (hS : S.Nonempty)
  (hScoeff : FABL.fourierCoeff f S ≠ 0)
  (hlarge :
    ∀ (T : Finset (Fin n)),
      T.Nonempty →
        FABL.fourierCoeff f T ≠ 0 →
          2 * n < 3 * T.card) :
  FABL.fourierCoeff (fun x => f x * f x)
      S =
    2 * FABL.fourierCoeff f ∅ *
      FABL.fourierCoeff f S

theorem FABL.correlationImmune_not_resilient_three_mul_succ_le_two_mul_dimension
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℕ)
  (himmune : FABL.IsCorrelationImmune k f)
  (hnotResilient : ¬FABL.IsResilient k f)
  (hnonconstant :
    ¬∃ c, f.toReal = fun x => c) :
  3 * (k + 1) ≤ 2 * n

theorem FABL.vectorFourierCoeff_bentDirectProduct_append
  {n m : ℕ} (f : FABL.F₂Cube n → ℝ)
  (g : FABL.F₂Cube m → ℝ)
  (a : FABL.F₂Cube n)
  (b : FABL.F₂Cube m) :
  FABL.vectorFourierCoeff
      (FABL.bentDirectProduct f g)
      (Fin.append a b) =
    FABL.vectorFourierCoeff f a *
      FABL.vectorFourierCoeff g b