theorem CryptBoolean.coordinateBooleanFunction_dependsOn
  {n : ℕ} (I : Finset (Fin n))
  (g :
    CryptBoolean.CoordinateSignChoice I) :
  DependsOn
    (CryptBoolean.coordinateBooleanFunction
      I g)
    ↑I

theorem CryptBoolean.exists_coordinateSignChoice_iff_dependsOn
  {n : ℕ} (I : Finset (Fin n))
  (g : CryptBoolean.BooleanFunction n) :
  (∃ q,
      CryptBoolean.coordinateBooleanFunction
          I q =
        g) ↔
    DependsOn g ↑I

theorem CryptBoolean.normalizedCorrelation_eq_one_sub_two_mul_hammingDistance
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.normalizedCorrelation f g =
    1 -
      2 *
          ↑(CryptBoolean.hammingDistance f
              g) /
        2 ^ n

theorem CryptBoolean.distanceToCoordinateFunctions_cast_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  ↑(CryptBoolean.distanceToCoordinateFunctions
        f I) =
    2 ^ n / 2 *
      (1 -
        CryptBoolean.maximumCorrelation f
          I)

theorem CryptBoolean.higherOrderNonlinearity_le_distanceToCoordinateFunctions
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.higherOrderNonlinearity
      I.card f ≤
    CryptBoolean.distanceToCoordinateFunctions
      f I

theorem CryptBoolean.maximumCorrelation_eq_restrictionMaximumCorrelation
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.maximumCorrelation f I =
    CryptBoolean.restrictionMaximumCorrelation
      f I

theorem CryptBoolean.maximumCorrelation_eq_sum_abs_restrictionRawImbalance_div_two_pow
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.maximumCorrelation f I =
    (∑ z,
        |CryptBoolean.restrictionRawImbalance
            f I z|) /
      2 ^ n

theorem CryptBoolean.maximumCorrelation_eq_zero_iff_restrictions_balanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.maximumCorrelation f I =
      0 ↔
    ∀ (z : FABL.FixedSignCube Iᶜ),
      FABL.IsBalanced
        (FABL.signRestriction
          (CryptBoolean.signCubeView
              f).toReal
          Iᶜ z)

theorem CryptBoolean.restrictedWalshSquareSum_eq_sum_filter
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.restrictedWalshSquareSum f
      I =
    ∑ u with FABL.f₂Support u ⊆ I,
      ↑(CryptBoolean.walshTransform f u) ^
        2

theorem CryptBoolean.two_pow_sq_mul_expect_restrictionMean_sq_eq_restrictedWalshSquareSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  ((2 ^ n) ^ 2 *
      Finset.univ.expect fun z =>
        FABL.mean
            (FABL.signRestriction
              (CryptBoolean.signCubeView
                  f).toReal
              Iᶜ z) ^
          2) =
    CryptBoolean.restrictedWalshSquareSum
      f I

theorem CryptBoolean.maximumCorrelation_le_sqrt_restrictedWalshSquareSum_div
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.maximumCorrelation f I ≤
    √(CryptBoolean.restrictedWalshSquareSum
          f I) /
      2 ^ n

theorem CryptBoolean.restrictedWalshSquareSum_le_card_mul_maxWalshMagnitude_sq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.restrictedWalshSquareSum f
      I ≤
    2 ^ I.card *
      ↑(CryptBoolean.maxWalshMagnitude
            f) ^
        2

theorem CryptBoolean.sqrt_restrictedWalshSquareSum_le
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  √(CryptBoolean.restrictedWalshSquareSum
        f I) ≤
    √(2 ^ I.card) *
      ↑(CryptBoolean.maxWalshMagnitude f)

theorem CryptBoolean.relation_40_maximumCorrelation_bound
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  CryptBoolean.maximumCorrelation f I ≤
      √(CryptBoolean.restrictedWalshSquareSum
            f I) /
        2 ^ n ∧
    CryptBoolean.maximumCorrelation f I ≤
      2 ^ (-↑n + ↑I.card / 2) *
        (2 ^ n -
          2 *
            ↑(CryptBoolean.nonlinearity
                f))

theorem CryptBoolean.distanceToCoordinateFunctions_cast_ge_walshSquare
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  2 ^ n / 2 -
      √(CryptBoolean.restrictedWalshSquareSum
            f I) /
        2 ≤
    ↑(CryptBoolean.distanceToCoordinateFunctions
        f I)

theorem CryptBoolean.distanceToCoordinateFunctions_cast_ge_maxWalshMagnitude
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (I : Finset (Fin n)) :
  2 ^ n / 2 -
      2 ^ (↑I.card / 2 - 1) *
        ↑(CryptBoolean.maxWalshMagnitude
            f) ≤
    ↑(CryptBoolean.distanceToCoordinateFunctions
        f I)

theorem CryptBoolean.mem_zeroDerivativeKernel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : FABL.F₂Cube n) :
  e ∈
      CryptBoolean.zeroDerivativeKernel
        f ↔
    CryptBoolean.IsZeroDerivativeDirection
      f e

theorem CryptBoolean.zeroDerivativeKernel_le_linearKernel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.zeroDerivativeKernel f ≤
    CryptBoolean.linearKernel f

theorem CryptBoolean.finrank_zeroDerivativeKernel_comp_affineEquiv
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  Module.finrank FABL.𝔽₂
      ↥(CryptBoolean.zeroDerivativeKernel
          (f ∘ ⇑L)) =
    Module.finrank FABL.𝔽₂
      ↥(CryptBoolean.zeroDerivativeKernel
          f)

theorem CryptBoolean.zeroDerivativeKernel_zero
  {n : ℕ} :
  CryptBoolean.zeroDerivativeKernel 0 = ⊤

theorem CryptBoolean.finrank_zeroDerivativeKernel_zero
  {n : ℕ} :
  Module.finrank FABL.𝔽₂
      ↥(CryptBoolean.zeroDerivativeKernel
          0) =
    n

theorem CryptBoolean.largeZeroDerivativeFunctions_nonempty
  {n : ℕ} (k : ℕ) (hk : k ≤ n) :
  (CryptBoolean.largeZeroDerivativeFunctions
      k).Nonempty

theorem CryptBoolean.mem_largeZeroDerivativeFunctions_comp_affineEquiv_iff
  {n : ℕ}
  (g : CryptBoolean.BooleanFunction n)
  (k : ℕ)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  g ∘ ⇑L ∈
      CryptBoolean.largeZeroDerivativeFunctions
        k ↔
    g ∈
      CryptBoolean.largeZeroDerivativeFunctions
        k

theorem CryptBoolean.generalizedLinearStructureDistance_comp_affineEquiv_le
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) (hk : k ≤ n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.generalizedLinearStructureDistance
      (f ∘ ⇑L) k hk ≤
    CryptBoolean.generalizedLinearStructureDistance
      f k hk

theorem CryptBoolean.generalizedLinearStructureDistance_comp_affineEquiv
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) (hk : k ≤ n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.generalizedLinearStructureDistance
      (f ∘ ⇑L) k hk =
    CryptBoolean.generalizedLinearStructureDistance
      f k hk