theorem CryptBoolean.isLinearStructure_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsLinearStructure f 0

theorem CryptBoolean.booleanDerivative_add_direction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e d x : FABL.F₂Cube n) :
  FABL.booleanDerivative f (e + d) x =
    FABL.booleanDerivative f e (x + d) +
      FABL.booleanDerivative f d x

theorem CryptBoolean.IsLinearStructure.add {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {e d : FABL.F₂Cube n}
  (he :
    CryptBoolean.IsLinearStructure f e)
  (hd :
    CryptBoolean.IsLinearStructure f d) :
  CryptBoolean.IsLinearStructure f (e + d)

theorem CryptBoolean.IsLinearStructure.smul
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {e : FABL.F₂Cube n}
  (he :
    CryptBoolean.IsLinearStructure f e)
  (c : FABL.𝔽₂) :
  CryptBoolean.IsLinearStructure f (c • e)

theorem CryptBoolean.mem_linearKernel {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : FABL.F₂Cube n) :
  e ∈ CryptBoolean.linearKernel f ↔
    CryptBoolean.IsLinearStructure f e

theorem CryptBoolean.finrank_linearKernel_ge_iff_hasSeparatedLinearStructureNormalForm
  {m k : ℕ}
  (f :
    CryptBoolean.BooleanFunction
      (m + k)) :
  k ≤
      Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.linearKernel f) ↔
    CryptBoolean.HasSeparatedLinearStructureNormalForm
      f

theorem CryptBoolean.exists_nonzero_linearStructure_iff_exists_single_coordinate_normalForm
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction
      (m + 1)) :
  (∃ e,
      e ≠ 0 ∧
        CryptBoolean.IsLinearStructure f
          e) ↔
    ∃ L g ε,
      ∀ (x : FABL.F₂Cube m) (a : FABL.𝔽₂),
        f (L (Fin.append x ![a])) =
          g x + ε * a

theorem CryptBoolean.nonlinearity_cast_le_of_finrank_linearKernel_eq
  {m k : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + k))
  (hker :
    Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.linearKernel f) =
      k) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ (↑(m + k) - 1) -
      2 ^ ((↑(m + k) + ↑k - 2) / 2)

theorem CryptBoolean.nonlinearity_cast_le_of_exists_nonzero_linearStructure
  {m : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + 1))
  (hstructure :
    ∃ e,
      e ≠ 0 ∧
        CryptBoolean.IsLinearStructure f
          e) :
  ↑(CryptBoolean.nonlinearity f) ≤
    2 ^ (↑(m + 1) - 1) -
      2 ^ ((↑(m + 1) - 1) / 2)

theorem CryptBoolean.mem_walshHyperplane_iff
  {n : ℕ} (e u : FABL.F₂Cube n) :
  u ∈ CryptBoolean.walshHyperplane e ↔
    FABL.f₂DotProduct u e = 0

theorem CryptBoolean.natCard_walshHyperplane
  {n : ℕ} (e : FABL.F₂Cube n)
  (he : e ≠ 0) :
  Nat.card
      ↥(CryptBoolean.walshHyperplane e) =
    2 ^ (n - 1)

theorem CryptBoolean.sum_walshTransform_sq_hyperplane_coset
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e a : FABL.F₂Cube n) (he : e ≠ 0) :
  ∑ u,
      ↑(CryptBoolean.walshTransform f
            (a + ↑u)) ^
        2 =
    2 ^ (n - 1) *
      (2 ^ n +
        (FABL.vectorWalshCharacter a) e *
          CryptBoolean.autocorrelation f
            e)

theorem CryptBoolean.mem_walshSupport {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) :
  u ∈ CryptBoolean.walshSupport f ↔
    CryptBoolean.walshTransform f u ≠ 0

theorem CryptBoolean.booleanDerivative_eq_zero_iff_walshSupport_subset_hyperplane
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : FABL.F₂Cube n) (he : e ≠ 0) :
  FABL.booleanDerivative f e = 0 ↔
    ↑(CryptBoolean.walshSupport f) ⊆
      ↑(CryptBoolean.walshHyperplane e)

theorem CryptBoolean.booleanDerivative_eq_one_iff_walshSupport_subset_hyperplane_compl
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : FABL.F₂Cube n) (he : e ≠ 0) :
  FABL.booleanDerivative f e = 1 ↔
    ↑(CryptBoolean.walshSupport f) ⊆
      (↑(CryptBoolean.walshHyperplane e))ᶜ

theorem CryptBoolean.isBalanced_of_booleanDerivative_eq_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : FABL.F₂Cube n)
  (hderivative :
    FABL.booleanDerivative f e = 1) :
  CryptBoolean.IsBalanced f

theorem CryptBoolean.isLinearStructure_iff_booleanDerivative_eq_zero_of_not_balanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : FABL.F₂Cube n)
  (hf : ¬CryptBoolean.IsBalanced f) :
  CryptBoolean.IsLinearStructure f e ↔
    FABL.booleanDerivative f e = 0

theorem CryptBoolean.no_nonzero_null_derivative_iff_walshSupportSpan_eq_top
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (∀ (e : FABL.F₂Cube n),
      e ≠ 0 →
        FABL.booleanDerivative f e ≠ 0) ↔
    CryptBoolean.walshSupportSpan f = ⊤

theorem CryptBoolean.walshSupportRank_eq_n_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.walshSupportRank f = n ↔
    CryptBoolean.walshSupportSpan f = ⊤

theorem CryptBoolean.no_nonzero_linearStructure_iff_walshSupportRank_eq_n_of_not_balanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf : ¬CryptBoolean.IsBalanced f) :
  (∀ (e : FABL.F₂Cube n),
      e ≠ 0 →
        ¬CryptBoolean.IsLinearStructure f
            e) ↔
    CryptBoolean.walshSupportRank f = n

theorem CryptBoolean.distanceToLinearStructures_le_hammingDistance
  {n : ℕ} (hn : 0 < n)
  (f g : CryptBoolean.BooleanFunction n)
  (hg :
    CryptBoolean.HasNonzeroLinearStructure
      g) :
  CryptBoolean.distanceToLinearStructures
      f ≤
    CryptBoolean.hammingDistance f g

theorem CryptBoolean.exists_hammingDistance_eq_distanceToLinearStructures
  {n : ℕ} (hn : 0 < n)
  (f : CryptBoolean.BooleanFunction n) :
  ∃ g,
    CryptBoolean.HasNonzeroLinearStructure
        g ∧
      CryptBoolean.hammingDistance f g =
        CryptBoolean.distanceToLinearStructures
          f

theorem CryptBoolean.abs_autocorrelation_le_absoluteIndicator
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  {e : FABL.F₂Cube n} (he : e ≠ 0) :
  |CryptBoolean.autocorrelation f e| ≤
    CryptBoolean.absoluteIndicator f

theorem CryptBoolean.distanceToLinearStructures_cast_eq
  {n : ℕ} (hn : 2 ≤ n)
  (f : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.distanceToLinearStructures
        f) =
    2 ^ n / 4 -
      CryptBoolean.absoluteIndicator f / 4

theorem CryptBoolean.distanceToLinearStructures_le_nonlinearity
  {n : ℕ} (hn : 2 ≤ n)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.distanceToLinearStructures
      f ≤
    CryptBoolean.nonlinearity f

theorem CryptBoolean.distanceToLinearStructures_le_two_pow
  {n : ℕ} (hn : 2 ≤ n)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.distanceToLinearStructures
      f ≤
    2 ^ (n - 2)

theorem CryptBoolean.absoluteIndicator_eq_zero_iff_isBent
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.absoluteIndicator f = 0 ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.distanceToLinearStructures_eq_two_pow_iff_isBent
  {n : ℕ} (hn : 2 ≤ n)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.distanceToLinearStructures
        f =
      2 ^ (n - 2) ↔
    CryptBoolean.IsBent f