theorem CryptBoolean.exists_affineEquiv_anfSupport_card_eq_algebraicThickness
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∃ L,
    (FABL.anfSupport
          (FABL.anfCoeff (f ∘ ⇑L))).card =
      CryptBoolean.algebraicThickness f

theorem CryptBoolean.IsConstantOnAffineFlat.isAffineOnAffineFlat
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)}
  {a : FABL.F₂Cube n}
  (h :
    CryptBoolean.IsConstantOnAffineFlat f
      H a) :
  CryptBoolean.IsAffineOnAffineFlat f H a

theorem CryptBoolean.normality_le_weakNormality
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.normality f ≤
    CryptBoolean.weakNormality f

theorem CryptBoolean.two_mul_two_pow_mul_kthNonhomomorphicity
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hk : 0 < k) :
  2 * 2 ^ n *
      ↑(CryptBoolean.kthNonhomomorphicity
          f k) =
    (2 ^ n) ^ k +
      ∑ a,
        ↑(CryptBoolean.walshTransform f
              a) ^
          k

theorem CryptBoolean.kthNonhomomorphicity_cast_eq_walshMoment
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hk : 0 < k) :
  ↑(CryptBoolean.kthNonhomomorphicity f
        k) =
    (2 ^ n) ^ (k - 1) / 2 +
      (∑ a,
          ↑(CryptBoolean.walshTransform f
                a) ^
            k) /
        (2 * 2 ^ n)

theorem CryptBoolean.kthNonhomomorphicity_cast_eq_carlet_formula
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hk : 0 < k) :
  ↑(CryptBoolean.kthNonhomomorphicity f
        k) =
    2 ^ ((k - 1) * n) / 2 +
      (∑ a,
          ↑(CryptBoolean.walshTransform f
                a) ^
            k) /
        2 ^ (n + 1)

theorem CryptBoolean.isAffineBooleanFunction_iff_nonlinearity_eq_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsAffineBooleanFunction f ↔
    CryptBoolean.nonlinearity f = 0

theorem CryptBoolean.abs_walshTransform_le_two_pow
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  |↑(CryptBoolean.walshTransform f a)| ≤
    2 ^ n

theorem CryptBoolean.sum_walshTransform_evenMoment_le
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (r : ℕ) (hr : 0 < r) :
  ∑ a,
      ↑(CryptBoolean.walshTransform f a) ^
        (2 * r) ≤
    (2 ^ n) ^ (2 * r)

theorem CryptBoolean.kthNonhomomorphicity_affineFunction
  {n k : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) (hkEven : Even k)
  (hk : 0 < k) :
  ↑(CryptBoolean.kthNonhomomorphicity
        (FABL.affineFunction b a) k) =
    (2 ^ n) ^ (k - 1)

theorem CryptBoolean.kthNonhomomorphicity_cast_le_max
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hkEven : Even k) (hkFour : 4 ≤ k) :
  ↑(CryptBoolean.kthNonhomomorphicity f
        k) ≤
    (2 ^ n) ^ (k - 1)

theorem CryptBoolean.kthNonhomomorphicity_cast_eq_max_iff_isAffine
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hkEven : Even k) (hkFour : 4 ≤ k) :
  ↑(CryptBoolean.kthNonhomomorphicity f
          k) =
      (2 ^ n) ^ (k - 1) ↔
    CryptBoolean.IsAffineBooleanFunction f

theorem CryptBoolean.carlet_kthNonhomomorphicity_cast_eq_max_iff_isAffine
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hkEven : Even k) (hkFour : 4 ≤ k)
  (_hkCard : k ≤ 2 ^ n) :
  ↑(CryptBoolean.kthNonhomomorphicity f
          k) =
      (2 ^ n) ^ (k - 1) ↔
    CryptBoolean.IsAffineBooleanFunction f

theorem CryptBoolean.two_pow_pow_succ_le_sum_walshTransform_evenMoment
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (r : ℕ) (hr : 2 ≤ r) :
  (2 ^ n) ^ (r + 1) ≤
    ∑ a,
      ↑(CryptBoolean.walshTransform f a) ^
        (2 * r)

theorem CryptBoolean.sum_walshTransform_evenMoment_eq_min_iff_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (r : ℕ) (hr : 2 ≤ r) :
  ∑ a,
        ↑(CryptBoolean.walshTransform f
              a) ^
          (2 * r) =
      (2 ^ n) ^ (r + 1) ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.kthNonhomomorphicity_cast_min_le
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hkEven : Even k) (hkFour : 4 ≤ k) :
  (2 ^ n) ^ (k - 1) / 2 +
      (2 ^ n) ^ (k / 2) / 2 ≤
    ↑(CryptBoolean.kthNonhomomorphicity f
        k)

theorem CryptBoolean.kthNonhomomorphicity_cast_eq_min_iff_isBent
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hkEven : Even k) (hkFour : 4 ≤ k) :
  ↑(CryptBoolean.kthNonhomomorphicity f
          k) =
      (2 ^ n) ^ (k - 1) / 2 +
        (2 ^ n) ^ (k / 2) / 2 ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.carlet_kthNonhomomorphicity_cast_eq_min_iff_isBent
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hkEven : Even k) (hkFour : 4 ≤ k)
  (_hkCard : k ≤ 2 ^ n) :
  ↑(CryptBoolean.kthNonhomomorphicity f
          k) =
      (2 ^ n) ^ (k - 1) / 2 +
        (2 ^ n) ^ (k / 2) / 2 ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.walshCoordinateLinearMap_injective
  {n : ℕ} (u : Fin n → FABL.F₂Cube n)
  (hu : LinearIndependent FABL.𝔽₂ u) :
  Function.Injective
    ⇑(CryptBoolean.walshCoordinateLinearMap
        u)

theorem CryptBoolean.bentDualFrequency_walshReindexLinearEquiv_single
  {n : ℕ} (u : Fin n → FABL.F₂Cube n)
  (hu : LinearIndependent FABL.𝔽₂ u)
  (i : Fin n) :
  FABL.bentDualFrequency
      (CryptBoolean.walshReindexLinearEquiv
        u hu)
      (FABL.f₂CubeOfFinset {i}) =
    u i

theorem CryptBoolean.walshTransform_linearReindex_cast
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (M :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (γ : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform (f ∘ ⇑M)
        γ) =
    ↑(CryptBoolean.walshTransform f
        (FABL.bentDualFrequency M γ))

theorem CryptBoolean.bentDualFrequency_zero
  {n : ℕ}
  (M :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  FABL.bentDualFrequency M 0 = 0

theorem CryptBoolean.isBalanced_linearReindex
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (M :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (hf : CryptBoolean.IsBalanced f) :
  CryptBoolean.IsBalanced (f ∘ ⇑M)

theorem CryptBoolean.exists_linearEquiv_isResilient_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : Fin n → FABL.F₂Cube n)
  (hu : LinearIndependent FABL.𝔽₂ u)
  (hbalanced : CryptBoolean.IsBalanced f)
  (hzero :
    ∀ (i : Fin n),
      CryptBoolean.walshTransform f
          (u i) =
        0) :
  ∃ M, CryptBoolean.IsResilient 1 (f ∘ ⇑M)