theorem CryptBoolean.functionAlgebraicDegree_le_dimension
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.functionAlgebraicDegree f ≤
    n

theorem CryptBoolean.algebraicDegree_le_iff
  {n : ℕ}
  (c : CryptBoolean.ANFCoefficients n)
  (r : ℕ) :
  CryptBoolean.algebraicDegree c ≤ r ↔
    ∀ (S : Finset (Fin n)),
      c S ≠ 0 → S.card ≤ r

theorem CryptBoolean.anfCoeff_zero {n : ℕ} :
  CryptBoolean.anfCoeff 0 = fun x => 0

theorem CryptBoolean.algebraicDegree_zero
  {n : ℕ} :
  (CryptBoolean.algebraicDegree fun x =>
      0) =
    0

theorem CryptBoolean.functionAlgebraicDegree_zero
  {n : ℕ} :
  CryptBoolean.functionAlgebraicDegree 0 =
    0

theorem CryptBoolean.anfCoeff_add {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.anfCoeff (f + g) = fun S =>
    CryptBoolean.anfCoeff f S +
      CryptBoolean.anfCoeff g S

theorem CryptBoolean.algebraicDegree_add_le_max
  {n : ℕ}
  (c d : CryptBoolean.ANFCoefficients n) :
  (CryptBoolean.algebraicDegree fun S =>
      c S + d S) ≤
    max (CryptBoolean.algebraicDegree c)
      (CryptBoolean.algebraicDegree d)

theorem CryptBoolean.functionAlgebraicDegree_add_le_max
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.functionAlgebraicDegree
      (f + g) ≤
    max
      (CryptBoolean.functionAlgebraicDegree
        f)
      (CryptBoolean.functionAlgebraicDegree
        g)

theorem CryptBoolean.hammingDistance_eq_hammingWeight_add
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hammingDistance f g =
    CryptBoolean.hammingWeight (f + g)

theorem CryptBoolean.hammingDistance_eq_two_pow_mul_relativeHammingDist
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  ↑(CryptBoolean.hammingDistance f g) =
    2 ^ n * FABL.relativeHammingDist f g

theorem CryptBoolean.anfEval_affineCoefficients
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) :
  CryptBoolean.anfEval
      (CryptBoolean.affineCoefficients b
        a) =
    CryptBoolean.affineFunction b a

theorem CryptBoolean.anfCoeff_affineFunction
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) :
  CryptBoolean.anfCoeff
      (CryptBoolean.affineFunction b a) =
    CryptBoolean.affineCoefficients b a

theorem CryptBoolean.functionAlgebraicDegree_affineFunction_le_one
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) :
  CryptBoolean.functionAlgebraicDegree
      (CryptBoolean.affineFunction b a) ≤
    1

theorem CryptBoolean.exists_affineFunction_of_functionAlgebraicDegree_le_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    CryptBoolean.functionAlgebraicDegree
        f ≤
      1) :
  ∃ b a,
    f = CryptBoolean.affineFunction b a

theorem CryptBoolean.anfMonomial_mul {n : ℕ}
  (S T : Finset (Fin n))
  (x : FABL.F₂Cube n) :
  CryptBoolean.anfMonomial S x *
      CryptBoolean.anfMonomial T x =
    CryptBoolean.anfMonomial (S ∪ T) x

theorem CryptBoolean.anfEval_anfMul {n : ℕ}
  (c d : CryptBoolean.ANFCoefficients n)
  (x : FABL.F₂Cube n) :
  CryptBoolean.anfEval
      (CryptBoolean.anfMul c d) x =
    CryptBoolean.anfEval c x *
      CryptBoolean.anfEval d x

theorem CryptBoolean.algebraicDegree_anfMul_le_add
  {n : ℕ}
  (c d : CryptBoolean.ANFCoefficients n) :
  CryptBoolean.algebraicDegree
      (CryptBoolean.anfMul c d) ≤
    CryptBoolean.algebraicDegree c +
      CryptBoolean.algebraicDegree d

theorem CryptBoolean.anfCoeff_mul {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.anfCoeff (f * g) =
    CryptBoolean.anfMul
      (CryptBoolean.anfCoeff f)
      (CryptBoolean.anfCoeff g)

theorem CryptBoolean.functionAlgebraicDegree_mul_le_add
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.functionAlgebraicDegree
      (f * g) ≤
    CryptBoolean.functionAlgebraicDegree
        f +
      CryptBoolean.functionAlgebraicDegree
        g

theorem CryptBoolean.functionAlgebraicDegree_one
  {n : ℕ} :
  CryptBoolean.functionAlgebraicDegree 1 =
    0

theorem CryptBoolean.functionAlgebraicDegree_finset_prod_le.{u_1}
  {n : ℕ} {ι : Type u_1} (s : Finset ι)
  (g :
    ι → CryptBoolean.BooleanFunction n) :
  CryptBoolean.functionAlgebraicDegree
      (∏ i ∈ s, g i) ≤
    ∑ i ∈ s,
      CryptBoolean.functionAlgebraicDegree
        (g i)

theorem CryptBoolean.functionAlgebraicDegree_finset_sum_le.{u_1}
  {n : ℕ} {ι : Type u_1} (s : Finset ι)
  (g : ι → CryptBoolean.BooleanFunction n)
  (r : ℕ)
  (hg :
    ∀ i ∈ s,
      CryptBoolean.functionAlgebraicDegree
          (g i) ≤
        r) :
  CryptBoolean.functionAlgebraicDegree
      (∑ i ∈ s, g i) ≤
    r

theorem CryptBoolean.functionAlgebraicDegree_affineMap_coordinate_le_one
  {n : ℕ}
  (L :
    FABL.F₂Cube n →ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (i : Fin n) :
  (CryptBoolean.functionAlgebraicDegree
      fun x => L x i) ≤
    1

theorem CryptBoolean.functionAlgebraicDegree_anfMonomial_comp_affineMap_le_card
  {n : ℕ}
  (L :
    FABL.F₂Cube n →ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (S : Finset (Fin n)) :
  (CryptBoolean.functionAlgebraicDegree
      fun x =>
      CryptBoolean.anfMonomial S (L x)) ≤
    S.card

theorem CryptBoolean.functionAlgebraicDegree_comp_affineMap_le
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (L :
    FABL.F₂Cube n →ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.functionAlgebraicDegree
      (f ∘ ⇑L) ≤
    CryptBoolean.functionAlgebraicDegree f

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

theorem CryptBoolean.card_powerset_filter_card_le
  {n : ℕ} (U : Finset (Fin n)) (k : ℕ) :
  {S ∈ U.powerset | S.card ≤ k}.card =
    ∑ i ∈ Finset.range (k + 1),
      U.card.choose i

theorem CryptBoolean.card_intermediate_subsets_le
  {n : ℕ} (T U : Finset (Fin n)) (d : ℕ)
  (hTU : T ⊆ U) (hTd : T.card ≤ d) :
  {S ∈ U.powerset |
        T ⊆ S ∧ S.card ≤ d}.card =
    ∑ i ∈ Finset.range (d - T.card + 1),
      (U.card - T.card).choose i

theorem CryptBoolean.restrictionRecoveryFormula_f₂CubeOfFinset
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (d : ℕ)
  (hdegree :
    CryptBoolean.functionAlgebraicDegree
        f ≤
      d)
  (U : Finset (Fin n)) :
  f (FABL.f₂CubeOfFinset U) =
    ∑ T ∈ U.powerset,
      if T.card ≤ d then
        f (FABL.f₂CubeOfFinset T) *
          ↑(∑
              i ∈
                Finset.range
                  (d - T.card + 1),
              (U.card - T.card).choose i)
      else 0

theorem CryptBoolean.restrictionRecoveryFormula
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (d : ℕ)
  (hdegree :
    CryptBoolean.functionAlgebraicDegree
        f ≤
      d)
  (_hdn : d < n) (x : FABL.F₂Cube n) :
  f x =
    ∑
      y ∈
        CryptBoolean.lowWeightInputs
          d with
      CryptBoolean.supportPrecedes y x,
      f y *
        CryptBoolean.restrictionRecoveryCoefficient
          d x y

theorem CryptBoolean.eq_of_eq_on_lowWeightInputs
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (d : ℕ)
  (hf :
    CryptBoolean.functionAlgebraicDegree
        f ≤
      d)
  (hg :
    CryptBoolean.functionAlgebraicDegree
        g ≤
      d)
  (hdn : d < n)
  (hfg :
    ∀ y ∈ CryptBoolean.lowWeightInputs d,
      f y = g y) :
  f = g

theorem CryptBoolean.eq_of_eq_on_affineImage_lowWeightInputs
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (d : ℕ)
  (hf :
    CryptBoolean.functionAlgebraicDegree
        f ≤
      d)
  (hg :
    CryptBoolean.functionAlgebraicDegree
        g ≤
      d)
  (hdn : d < n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (hfg :
    ∀
      z ∈
        Finset.image (fun y => L y)
          (CryptBoolean.lowWeightInputs
            d),
      f z = g z) :
  f = g