theorem CryptBoolean.realSignView_affineFunction
  {n : ℕ} (b : FABL.𝔽₂)
  (a x : FABL.F₂Cube n) :
  CryptBoolean.realSignView
      (CryptBoolean.affineFunction b a)
      x =
    FABL.binarySign b *
      (FABL.vectorWalshCharacter a) x

theorem CryptBoolean.isBalanced_affineFunction_of_ne_zero
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) (ha : a ≠ 0) :
  CryptBoolean.IsBalanced
    (CryptBoolean.affineFunction b a)

theorem CryptBoolean.hammingWeight_affineFunction_of_ne_zero
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) (ha : a ≠ 0) :
  CryptBoolean.hammingWeight
      (CryptBoolean.affineFunction b a) =
    2 ^ (n - 1)

theorem CryptBoolean.mem_reedMuller_iff {n r : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  f ∈ CryptBoolean.reedMuller r n ↔
    CryptBoolean.functionAlgebraicDegree
        f ≤
      r

theorem CryptBoolean.reedMuller_mono {n r s : ℕ}
  (hrs : r ≤ s) :
  CryptBoolean.reedMuller r n ≤
    CryptBoolean.reedMuller s n

theorem CryptBoolean.affineFunction_mem_reedMuller_one
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) :
  CryptBoolean.affineFunction b a ∈
    CryptBoolean.reedMuller 1 n

theorem CryptBoolean.reedMuller_distance_pos
  {n r : ℕ}
  {f g : CryptBoolean.BooleanFunction n}
  (_hf : f ∈ CryptBoolean.reedMuller r n)
  (_hg : g ∈ CryptBoolean.reedMuller r n)
  (hfg : f ≠ g) :
  0 < CryptBoolean.hammingDistance f g

theorem CryptBoolean.hammingWeight_affineFunction_one_zero
  {n : ℕ} :
  CryptBoolean.hammingWeight
      (CryptBoolean.affineFunction 1 0) =
    2 ^ n

theorem CryptBoolean.two_pow_sub_one_le_hammingWeight_of_degree_le_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    CryptBoolean.functionAlgebraicDegree
        f ≤
      1)
  (hf : f ≠ 0) :
  2 ^ (n - 1) ≤
    CryptBoolean.hammingWeight f

theorem CryptBoolean.reedMuller_one_distance_lower_bound
  {n : ℕ}
  {f g : CryptBoolean.BooleanFunction n}
  (hf : f ∈ CryptBoolean.reedMuller 1 n)
  (hg : g ∈ CryptBoolean.reedMuller 1 n)
  (hfg : f ≠ g) :
  2 ^ (n - 1) ≤
    CryptBoolean.hammingDistance f g

theorem CryptBoolean.two_pow_sub_le_hammingWeight_of_degree_le
  {n r : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    CryptBoolean.functionAlgebraicDegree
        f ≤
      r)
  (hf : f ≠ 0) :
  2 ^ (n - r) ≤
    CryptBoolean.hammingWeight f

theorem CryptBoolean.reedMuller_distance_lower_bound
  {n r : ℕ}
  {f g : CryptBoolean.BooleanFunction n}
  (hf : f ∈ CryptBoolean.reedMuller r n)
  (hg : g ∈ CryptBoolean.reedMuller r n)
  (hfg : f ≠ g) :
  2 ^ (n - r) ≤
    CryptBoolean.hammingDistance f g

theorem CryptBoolean.reedMuller_card {n r : ℕ} :
  Nat.card
      ↥(CryptBoolean.reedMuller r n) =
    2 ^
      ∑ j ∈ Finset.range (r + 1),
        n.choose j

theorem CryptBoolean.reedMuller_finrank
  {n r : ℕ} :
  Module.finrank FABL.𝔽₂
      ↥(CryptBoolean.reedMuller r n) =
    ∑ j ∈ Finset.range (r + 1), n.choose j

theorem CryptBoolean.booleanFunctionPairing_apply
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  ((CryptBoolean.booleanFunctionPairing n)
        f)
      g =
    ∑ x, f x * g x

theorem CryptBoolean.booleanFunctionPairing_nondegenerate
  {n : ℕ} :
  (CryptBoolean.booleanFunctionPairing
      n).Nondegenerate

theorem CryptBoolean.reedMuller_complement_le_dual
  {n r : ℕ} (h : r < n) :
  CryptBoolean.reedMuller (n - r - 1) n ≤
    CryptBoolean.reedMullerDual r n

theorem CryptBoolean.reedMullerDual_eq {n r : ℕ}
  (h : r < n) :
  CryptBoolean.reedMullerDual r n =
    CryptBoolean.reedMuller (n - r - 1) n