theorem FABL.functionAlgebraicDegree_le_dimension
  {n : ℕ} (f : FABL.F₂BooleanFunction n) :
  FABL.functionAlgebraicDegree f ≤ n

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

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

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

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

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

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

theorem FABL.functionAlgebraicDegree_add_le_max
  {n : ℕ}
  (f g : FABL.F₂BooleanFunction n) :
  FABL.functionAlgebraicDegree (f + g) ≤
    max (FABL.functionAlgebraicDegree f)
      (FABL.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 FABL.anfEval_affineCoefficients {n : ℕ}
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  FABL.anfEval
      (FABL.affineCoefficients b a) =
    FABL.affineFunction b a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem FABL.functionAlgebraicDegree_comp_affineEquiv
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  FABL.functionAlgebraicDegree (f ∘ ⇑L) =
    FABL.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 :
    FABL.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 :
    FABL.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 :
    FABL.functionAlgebraicDegree f ≤ d)
  (hg :
    FABL.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 :
    FABL.functionAlgebraicDegree f ≤ d)
  (hg :
    FABL.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