theorem CryptBoolean.carletMajority_apply_eq_one_iff
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.carletMajority n x = 1 ↔
    n ≤ 2 * (FABL.f₂Support x).card

theorem CryptBoolean.carletMajority_apply_eq_one_iff_ceiling_half
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.carletMajority n x = 1 ↔
    (n + 1) / 2 ≤ (FABL.f₂Support x).card

theorem CryptBoolean.carletMajority_eq_of_support_card_eq
  {n : ℕ} (x y : FABL.F₂Cube n)
  (hweight :
    (FABL.f₂Support x).card =
      (FABL.f₂Support y).card) :
  CryptBoolean.carletMajority n x =
    CryptBoolean.carletMajority n y

theorem CryptBoolean.carletMajority_symmetric
  {n : ℕ} :
  FABL.IsSymmetric fun x =>
    CryptBoolean.carletMajority n
      ((FABL.binaryCubeSignEquiv n).symm
        x)

theorem CryptBoolean.carletMajority_isKNormal
  {n : ℕ} (hn : 0 < n) :
  CryptBoolean.IsKNormal
    (CryptBoolean.carletMajority n)
    (n / 2)

theorem CryptBoolean.algebraicImmunity_carletMajority
  {n : ℕ} :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.carletMajority n) =
    (n + 1) / 2

theorem CryptBoolean.fourierInfinityNorm_majority_even
  (r : ℕ) :
  FABL.fourierInfinityNorm
      (FABL.majority (2 * r)).toReal =
    FABL.oddMajorityInfluence r

theorem CryptBoolean.fourierInfinityNorm_majority_odd
  (r : ℕ) :
  FABL.fourierInfinityNorm
      (FABL.majority (2 * r + 1)).toReal =
    FABL.oddMajorityInfluence r

theorem CryptBoolean.maxWalshMagnitude_carletStrictMajority_even
  (r : ℕ) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.carletStrictMajority
        (2 * r)) =
    (2 * r).choose r

theorem CryptBoolean.maxWalshMagnitude_carletStrictMajority_odd
  (r : ℕ) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.carletStrictMajority
        (2 * r + 1)) =
    2 * (2 * r).choose r

theorem CryptBoolean.nonlinearity_carletStrictMajority_odd
  (r : ℕ) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletStrictMajority
        (2 * r + 1)) =
    2 ^ (2 * r) - (2 * r).choose r

theorem CryptBoolean.nonlinearity_carletStrictMajority_even
  (r : ℕ) (hr : 0 < r) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletStrictMajority
        (2 * r)) =
    2 ^ (2 * r - 1) - (2 * r - 1).choose r

theorem CryptBoolean.nonlinearity_carletStrictMajority
  {n : ℕ} (hn : 0 < n) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletStrictMajority
        n) =
    2 ^ (n - 1) - (n - 1).choose (n / 2)

theorem CryptBoolean.nonlinearity_add_constant_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonlinearity (f + 1) =
    CryptBoolean.nonlinearity f

theorem CryptBoolean.nonlinearity_carletMajority_eq_strictMajority
  {n : ℕ} :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletMajority n) =
    CryptBoolean.nonlinearity
      (CryptBoolean.carletStrictMajority
        n)

theorem CryptBoolean.nonlinearity_carletMajority
  {n : ℕ} (hn : 0 < n) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletMajority n) =
    2 ^ (n - 1) - (n - 1).choose (n / 2)

theorem CryptBoolean.nonlinearity_carletMajority_of_even
  {n : ℕ} (hn : 0 < n) (_heven : Even n) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletMajority n) =
    2 ^ (n - 1) - (n - 1).choose (n / 2)

theorem CryptBoolean.nonlinearity_carletMajority_of_odd
  {n : ℕ} (hodd : Odd n) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletMajority n) =
    2 ^ (n - 1) -
      (n - 1).choose ((n - 1) / 2)

theorem CryptBoolean.binaryComplementAffineEquiv_apply
  {n : ℕ} (x : FABL.F₂Cube n) :
  (CryptBoolean.binaryComplementAffineEquiv
        n)
      x =
    FABL.binaryCubeComplement x

theorem CryptBoolean.f₂Support_binaryCubeComplement
  {n : ℕ} (x : FABL.F₂Cube n) :
  FABL.f₂Support
      (FABL.binaryCubeComplement x) =
    (FABL.f₂Support x)ᶜ

theorem CryptBoolean.card_f₂Support_binaryCubeComplement
  {n : ℕ} (x : FABL.F₂Cube n) :
  (FABL.f₂Support
        (FABL.binaryCubeComplement
          x)).card =
    n - (FABL.f₂Support x).card

theorem CryptBoolean.carletStrictMajority_apply_eq_one_iff
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.carletStrictMajority n x =
      1 ↔
    n < 2 * (FABL.f₂Support x).card

theorem CryptBoolean.carletStrictMinority_apply_eq_one_iff
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.carletStrictMinority n x =
      1 ↔
    2 * (FABL.f₂Support x).card < n

theorem CryptBoolean.carletWeakMinority_apply_eq_one_iff
  {n : ℕ} (x : FABL.F₂Cube n) :
  CryptBoolean.carletWeakMinority n x =
      1 ↔
    2 * (FABL.f₂Support x).card ≤ n

theorem CryptBoolean.carletStrictMinority_eq_affineReindexing
  {n : ℕ} :
  CryptBoolean.carletStrictMinority n =
    CryptBoolean.carletStrictMajority n ∘
      ⇑(CryptBoolean.binaryComplementAffineEquiv
          n)

theorem CryptBoolean.carletWeakMinority_eq_outputComplement
  {n : ℕ} :
  CryptBoolean.carletWeakMinority n =
    CryptBoolean.carletStrictMajority n +
      1

theorem CryptBoolean.carletMajority_eq_affineReindexing_add_one
  {n : ℕ} :
  CryptBoolean.carletMajority n =
    CryptBoolean.carletStrictMajority n ∘
        ⇑(CryptBoolean.binaryComplementAffineEquiv
            n) +
      1

theorem CryptBoolean.algebraicImmunity_carletStrictMajority
  {n : ℕ} :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.carletStrictMajority
        n) =
    (n + 1) / 2

theorem CryptBoolean.algebraicImmunity_carletStrictMinority
  {n : ℕ} :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.carletStrictMinority
        n) =
    (n + 1) / 2

theorem CryptBoolean.algebraicImmunity_carletWeakMinority
  {n : ℕ} :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.carletWeakMinority
        n) =
    (n + 1) / 2

theorem CryptBoolean.nonlinearity_carletWeakMinority
  {n : ℕ} (hn : 0 < n) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletWeakMinority
        n) =
    2 ^ (n - 1) - (n - 1).choose (n / 2)

theorem CryptBoolean.nonlinearity_carletStrictMinority
  {n : ℕ} (hn : 0 < n) :
  CryptBoolean.nonlinearity
      (CryptBoolean.carletStrictMinority
        n) =
    2 ^ (n - 1) - (n - 1).choose (n / 2)

theorem CryptBoolean.mem_carletFengSupport_iff
  {n : ℕ}
  (alpha x :
    CryptBoolean.BinaryGaloisField n) :
  x ∈
      CryptBoolean.carletFengSupport
        alpha ↔
    x = 0 ∨
      ∃ i < 2 ^ (n - 1) - 1, x = alpha ^ i

theorem CryptBoolean.carletFengSupport_card
  {n : ℕ} (hn : 2 ≤ n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  (CryptBoolean.carletFengSupport
        alpha).card =
    2 ^ (n - 1)

theorem CryptBoolean.support_carletFengBooleanFunction
  {n : ℕ}
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  (alpha :
    CryptBoolean.BinaryGaloisField n) :
  Finset.map θ.toEquiv.toEmbedding
      (CryptBoolean.support
        (CryptBoolean.carletFengBooleanFunction
          θ alpha)) =
    CryptBoolean.carletFengSupport alpha

theorem CryptBoolean.isBalanced_carletFengBooleanFunction
  {n : ℕ} (hn : 2 ≤ n)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  CryptBoolean.IsBalanced
    (CryptBoolean.carletFengBooleanFunction
      θ alpha)

theorem CryptBoolean.algebraicImmunity_carletFengBooleanFunction
  {n : ℕ} (hn : 2 ≤ n)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  CryptBoolean.algebraicImmunity
      (CryptBoolean.carletFengBooleanFunction
        θ alpha) =
    (n + 1) / 2

theorem CryptBoolean.carletFeng_balanced_and_algebraicImmunity
  {n : ℕ} (hn : 2 ≤ n)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  CryptBoolean.IsBalanced
      (CryptBoolean.carletFengBooleanFunction
        θ alpha) ∧
    CryptBoolean.algebraicImmunity
        (CryptBoolean.carletFengBooleanFunction
          θ alpha) =
      (n + 1) / 2

theorem CryptBoolean.coeff_carletFengUnivariateRepresentation
  {n i : ℕ} (hn : 2 ≤ n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1))
  (hi0 : 0 < i) (hi : i < 2 ^ n - 1) :
  (CryptBoolean.carletFengUnivariateRepresentation
          alpha).coeff
      i =
    alpha ^ i /
      (1 + alpha ^ i) ^ 2 ^ (n - 1)

theorem CryptBoolean.coeff_top_carletFengUnivariateRepresentation
  {n : ℕ} (hn : 2 ≤ n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  (CryptBoolean.carletFengUnivariateRepresentation
          alpha).coeff
      (2 ^ n - 1) =
    0

theorem CryptBoolean.carletFengUnivariateRepresentation_eq_closedPolynomial
  {n : ℕ} (hn : 2 ≤ n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  CryptBoolean.carletFengUnivariateRepresentation
      alpha =
    CryptBoolean.carletFengClosedPolynomial
      alpha

theorem CryptBoolean.carletFeng_relation_70
  {n : ℕ} (hn : 2 ≤ n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1))
  (x : CryptBoolean.BinaryGaloisField n) :
  (algebraMap FABL.𝔽₂
        (CryptBoolean.BinaryGaloisField
          n))
      (CryptBoolean.carletFengFieldFunction
        alpha x) =
    1 +
      ∑ i ∈ Finset.Ico 1 (2 ^ n - 1),
        alpha ^ i /
            (1 + alpha ^ i) ^
              2 ^ (n - 1) *
          x ^ i

theorem CryptBoolean.coeff_two_pow_sub_two_carletFengUnivariateRepresentation_ne_zero
  {n : ℕ} (hn : 2 ≤ n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  (CryptBoolean.carletFengUnivariateRepresentation
          alpha).coeff
      (2 ^ n - 2) ≠
    0

theorem CryptBoolean.functionAlgebraicDegree_carletFengBooleanFunction
  {n : ℕ} (hn : 2 ≤ n)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  {alpha :
    CryptBoolean.BinaryGaloisField n}
  (halpha :
    IsPrimitiveRoot alpha (2 ^ n - 1)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.carletFengBooleanFunction
        θ alpha) =
    n - 1

theorem CryptBoolean.maxWalshMagnitude_carletFengBooleanFunction_cast_le
  {n : ℕ} (hn : 2 ≤ n)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  {α : CryptBoolean.BinaryGaloisField n}
  (hα : IsPrimitiveRoot α (2 ^ n - 1)) :
  ↑(CryptBoolean.maxWalshMagnitude
        (CryptBoolean.carletFengBooleanFunction
          θ α)) ≤
    2 * (1 + ↑n * Real.log 2 * √(2 ^ n))

theorem CryptBoolean.nonlinearity_carletFengBooleanFunction_lower_bound
  {n : ℕ} (hn : 2 ≤ n)
  (θ :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField n)
  {α : CryptBoolean.BinaryGaloisField n}
  (hα : IsPrimitiveRoot α (2 ^ n - 1)) :
  2 ^ (n - 1) -
        ↑n * Real.log 2 * √(2 ^ n) -
      1 ≤
    ↑(CryptBoolean.nonlinearity
        (CryptBoolean.carletFengBooleanFunction
          θ α))