theorem CryptBoolean.natAbs_walshTransform_eq_two_pow_half_of_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (a : FABL.F₂Cube n) :
  (CryptBoolean.walshTransform f
        a).natAbs =
    2 ^ (n / 2)

theorem CryptBoolean.maxWalshMagnitude_eq_two_pow_half_of_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.maxWalshMagnitude f =
    2 ^ (n / 2)

theorem CryptBoolean.nonlinearity_eq_two_pow_sub_two_pow_half_of_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (hn : 2 ≤ n) :
  CryptBoolean.nonlinearity f =
    2 ^ (n - 1) - 2 ^ (n / 2 - 1)

theorem CryptBoolean.isBent_iff_forall_natAbs_walshTransform_eq_two_pow_half
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    ∀ (a : FABL.F₂Cube n),
      (CryptBoolean.walshTransform f
            a).natAbs =
        2 ^ (n / 2)

theorem CryptBoolean.isBent_add_affineFunction_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  CryptBoolean.IsBent
      (f + FABL.affineFunction b a) ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.isBent_comp_affineEquiv_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.IsBent (f ∘ ⇑L) ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.abs_hammingDistance_affine_sub_half_of_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.IsBent f)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  |↑(CryptBoolean.hammingDistance f
            (FABL.affineFunction b a)) -
        2 ^ n / 2| =
    2 ^ (n / 2) / 2

theorem CryptBoolean.isBent_iff_forall_walshTransform_modeq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : Even n) (_hnTwo : 2 ≤ n) :
  CryptBoolean.IsBent f ↔
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f a ≡
        2 ^ (n / 2) [ZMOD 2 ^ (n / 2 + 1)]

theorem CryptBoolean.isBent_iff_forall_nonzero_derivative_isBalanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        CryptBoolean.IsBalanced
          (FABL.booleanDerivative f a)

theorem CryptBoolean.isBent_iff_satisfiesPropagationCriterion_dimension
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.SatisfiesPropagationCriterion
      n f

theorem CryptBoolean.hammingNorm_eq_sum_f₂BitWeight.{u_1}
  {ι : Type u_1} [Fintype ι]
  (x : ι → FABL.𝔽₂) :
  hammingNorm x =
    ∑ i, CryptBoolean.f₂BitWeight (x i)

theorem CryptBoolean.hammingNorm_add_restrictSupport_identity.{u_1}
  {ι : Type u_1} [Fintype ι]
  (x y : ι → FABL.𝔽₂) :
  (hammingNorm (x + y) +
      2 * hammingNorm fun j => y ↑j) =
    hammingNorm x + hammingNorm y

theorem CryptBoolean.bentSignMatrix_mul_conjTranspose_apply
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x z : FABL.F₂Cube n) :
  (CryptBoolean.bentSignMatrix f *
        (CryptBoolean.bentSignMatrix
            f).conjTranspose)
      x z =
    CryptBoolean.autocorrelation f (x + z)

theorem CryptBoolean.isBent_iff_bentSignMatrix_isHadamard
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBent f ↔
    (CryptBoolean.bentSignMatrix
        f).IsHadamard

theorem CryptBoolean.differenceMultiplicity_support_eq_hammingNorm_restriction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.differenceMultiplicity
      (CryptBoolean.support f) a =
    hammingNorm fun x => f (↑x + a)

theorem CryptBoolean.hammingWeight_booleanDerivative_add_two_mul_differenceMultiplicity
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.hammingWeight
        (FABL.booleanDerivative f a) +
      2 *
        CryptBoolean.differenceMultiplicity
          (CryptBoolean.support f) a =
    2 * CryptBoolean.hammingWeight f

theorem CryptBoolean.isBent_iff_support_isHadamardDifferenceSet
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (_hnEven : Even n) (hn : 2 ≤ n) :
  CryptBoolean.IsBent f ↔
    CryptBoolean.IsHadamardDifferenceSet
      (CryptBoolean.support f)

theorem CryptBoolean.booleanCayleyGraph_adj
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (x y : FABL.F₂Cube n) :
  (CryptBoolean.booleanCayleyGraph f).Adj
      x y ↔
    x ≠ y ∧ f (x + y) = 1

theorem CryptBoolean.card_commonNeighbors_booleanCayleyGraph
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hfZero : f 0 = 0)
  (v w : FABL.F₂Cube n) :
  Nat.card
      ↑((CryptBoolean.booleanCayleyGraph
              f).commonNeighbors
          v w) =
    CryptBoolean.differenceMultiplicity
      (CryptBoolean.support f) (v + w)

theorem CryptBoolean.degree_booleanCayleyGraph
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hfZero : f 0 = 0) (v : FABL.F₂Cube n) :
  (CryptBoolean.booleanCayleyGraph
          f).degree
      v =
    (CryptBoolean.support f).card

theorem CryptBoolean.isSRGWith_booleanCayleyGraph_of_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hnEven : Even n) (hn : 2 ≤ n)
  (hfZero : f 0 = 0)
  (hf : CryptBoolean.IsBent f) :
  (CryptBoolean.booleanCayleyGraph
        f).IsSRGWith
    (2 ^ n) (CryptBoolean.support f).card
    ((CryptBoolean.support f).card -
      2 ^ (n - 2))
    ((CryptBoolean.support f).card -
      2 ^ (n - 2))

theorem CryptBoolean.supportCodewordWeight_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.supportCodewordWeight f 0 =
    0

theorem CryptBoolean.supportCodewordWeight_eq_card_filter
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (v : FABL.F₂Cube n) :
  CryptBoolean.supportCodewordWeight f v =
    {x ∈ CryptBoolean.support f |
        FABL.f₂DotProduct v x = 1}.card

theorem CryptBoolean.codeCharacterSum_support_eq_card_sub_two_weight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (v : FABL.F₂Cube n) :
  CryptBoolean.codeCharacterSum
      (CryptBoolean.support f) v =
    ↑(CryptBoolean.support f).card -
      2 *
        ↑(CryptBoolean.supportCodewordWeight
            f v)

theorem CryptBoolean.four_mul_supportCodewordWeight_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (v : FABL.F₂Cube n) (hv : v ≠ 0) :
  4 *
      ↑(CryptBoolean.supportCodewordWeight
          f v) =
    2 ^ n +
        CryptBoolean.walshTransform f v -
      CryptBoolean.walshTransform f 0

theorem CryptBoolean.isBent_iff_supportCode_finrank_and_two_nonzero_weights
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hnEven : Even n) (hn : 4 ≤ n) :
  CryptBoolean.IsBent f ↔
    Module.finrank FABL.𝔽₂
          ↥(CryptBoolean.supportCode f) =
        n ∧
      CryptBoolean.SupportCodeHasExactlyTwoNonzeroWeights
        f

theorem CryptBoolean.finrank_supportCode_eq_n_iff_injective
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.supportCode f) =
      n ↔
    Function.Injective
      ⇑(CryptBoolean.supportCodeMap f)

theorem CryptBoolean.supportCodeWeightSumAlternative_not_characterize_bent :
  CryptBoolean.HasSupportCodeWeightSumAlternative
      CryptBoolean.supportCodeWeightSumCounterexample ∧
    ¬CryptBoolean.IsBent
        CryptBoolean.supportCodeWeightSumCounterexample

theorem CryptBoolean.supportCodeEvenLengthQuarterWeightAlternative_not_characterize_bent :
  CryptBoolean.HasSupportCodeEvenLengthQuarterWeightAlternative
      CryptBoolean.supportCodeQuarterWeightCounterexample ∧
    ¬CryptBoolean.IsBent
        CryptBoolean.supportCodeQuarterWeightCounterexample