theorem CryptBoolean.support_mul {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.support (f * g) =
    CryptBoolean.support f ∩
      CryptBoolean.support g

theorem CryptBoolean.booleanFunction_mul_self
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  f * f = f

theorem CryptBoolean.booleanFunction_mul_complement
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  f * (f + 1) = 0

theorem CryptBoolean.mem_annihilatorIdeal_iff
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  g ∈ CryptBoolean.annihilatorIdeal f ↔
    f * g = 0

theorem CryptBoolean.isAnnihilator_iff_mem_annihilatorIdeal
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsAnnihilator f g ↔
    g ≠ 0 ∧
      g ∈ CryptBoolean.annihilatorIdeal f

theorem CryptBoolean.mem_algebraicImmunityCandidates
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  g ∈
      CryptBoolean.algebraicImmunityCandidates
        f ↔
    CryptBoolean.IsAlgebraicImmunityWitness
      f g

theorem CryptBoolean.algebraicImmunityCandidates_nonempty
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (CryptBoolean.algebraicImmunityCandidates
      f).Nonempty

theorem CryptBoolean.algebraicImmunity_le_functionAlgebraicDegree
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hg :
    CryptBoolean.IsAlgebraicImmunityWitness
      f g) :
  CryptBoolean.algebraicImmunity f ≤
    FABL.functionAlgebraicDegree g

theorem CryptBoolean.exists_witness_functionAlgebraicDegree_eq_algebraicImmunity
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∃ g,
    CryptBoolean.IsAlgebraicImmunityWitness
        f g ∧
      FABL.functionAlgebraicDegree g =
        CryptBoolean.algebraicImmunity f

theorem CryptBoolean.IsAnnihilator.comp_affineEquiv
  {n : ℕ}
  {f g : CryptBoolean.BooleanFunction n}
  (h : CryptBoolean.IsAnnihilator f g)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.IsAnnihilator (f ∘ ⇑L)
    (g ∘ ⇑L)

theorem CryptBoolean.IsAlgebraicImmunityWitness.comp_affineEquiv
  {n : ℕ}
  {f g : CryptBoolean.BooleanFunction n}
  (h :
    CryptBoolean.IsAlgebraicImmunityWitness
      f g)
  (L :
    FABL.F₂Cube n ≃ᵃ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  CryptBoolean.IsAlgebraicImmunityWitness
    (f ∘ ⇑L) (g ∘ ⇑L)

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

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

theorem CryptBoolean.exists_lowDegreeRelation_iff_exists_algebraicImmunityWitness
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (d : ℕ) :
  (∃ g h,
      g ≠ 0 ∧
        FABL.functionAlgebraicDegree g ≤
            d ∧
          FABL.functionAlgebraicDegree h ≤
              d ∧
            f * g = h) ↔
    ∃ q,
      q ≠ 0 ∧
        FABL.functionAlgebraicDegree q ≤
            d ∧
          (f * q = 0 ∨ (f + 1) * q = 0)

theorem CryptBoolean.mem_ker_annihilatorEvaluationLinearMap_iff
  {n d : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c :
    ↥(FABL.lowDegreeFourierFamily n d) →
      FABL.𝔽₂) :
  c ∈
      (CryptBoolean.annihilatorEvaluationLinearMap
          f d).ker ↔
    f *
        ↑((CryptBoolean.reedMullerAnfEquiv
                d n).symm
            c) =
      0

theorem CryptBoolean.annihilatorEvaluationLinearMap_domain_finrank
  (n d : ℕ) :
  Module.finrank FABL.𝔽₂
      (↥(FABL.lowDegreeFourierFamily n
            d) →
        FABL.𝔽₂) =
    ∑ i ∈ Finset.range (d + 1), n.choose i

theorem CryptBoolean.annihilatorEvaluationLinearMap_codomain_finrank
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Module.finrank FABL.𝔽₂
      (↥(CryptBoolean.support f) →
        FABL.𝔽₂) =
    CryptBoolean.hammingWeight f

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

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

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

theorem CryptBoolean.algebraicImmunity_comp_surjectiveAffineMap_le
  {m n : ℕ}
  (f : CryptBoolean.BooleanFunction m)
  (L :
    FABL.F₂Cube n →ᵃ[FABL.𝔽₂]
      FABL.F₂Cube m)
  (hL : Function.Surjective ⇑L) :
  CryptBoolean.algebraicImmunity
      (f ∘ ⇑L) ≤
    CryptBoolean.algebraicImmunity f

theorem CryptBoolean.algebraicImmunity_le_ceiling_half
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.algebraicImmunity f ≤
    (n + 1) / 2

theorem CryptBoolean.algebraicImmunity_le_ceiling_half_of_hasSurjectiveAffineFactorization
  {n k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf :
    CryptBoolean.HasSurjectiveAffineFactorization
      f k) :
  CryptBoolean.algebraicImmunity f ≤
    (k + 1) / 2

theorem CryptBoolean.hasSurjectiveAffineFactorization_of_hasSeparatedLinearStructureNormalForm
  {m k : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + k))
  (hf :
    CryptBoolean.HasSeparatedLinearStructureNormalForm
      f) :
  CryptBoolean.HasSurjectiveAffineFactorization
      f m ∨
    CryptBoolean.HasSurjectiveAffineFactorization
      f (m + 1)

theorem CryptBoolean.algebraicImmunity_le_ceiling_half_add_one_of_hasSeparatedLinearStructureNormalForm
  {m k : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + k))
  (hf :
    CryptBoolean.HasSeparatedLinearStructureNormalForm
      f) :
  CryptBoolean.algebraicImmunity f ≤
    (m + 2) / 2

theorem CryptBoolean.algebraicImmunity_le_ceiling_half_add_one_of_linearKernel_finrank_ge
  {m k : ℕ}
  (f :
    CryptBoolean.BooleanFunction (m + k))
  (hk :
    k ≤
      Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.linearKernel f)) :
  CryptBoolean.algebraicImmunity f ≤
    (m + 2) / 2

theorem CryptBoolean.two_pow_lt_sum_choose_add_sum_choose_of_add_ge
  (n e d : ℕ) (hed : n ≤ e + d) :
  2 ^ n <
    ∑ i ∈ Finset.range (e + 1),
        n.choose i +
      ∑ i ∈ Finset.range (d + 1),
        n.choose i

theorem CryptBoolean.sum_choose_add_sum_choose_gt_iff
  (n e d : ℕ) :
  2 ^ n <
      ∑ i ∈ Finset.range (e + 1),
          n.choose i +
        ∑ i ∈ Finset.range (d + 1),
          n.choose i ↔
    n ≤ e + d

theorem CryptBoolean.exists_fastAlgebraicRelation_of_add_ge
  {n e d : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hed : n ≤ e + d) :
  ∃ g h,
    g ≠ 0 ∧
      FABL.functionAlgebraicDegree g ≤ e ∧
        FABL.functionAlgebraicDegree h ≤
            d ∧
          f * g = h

theorem CryptBoolean.isFastAlgebraicallyOptimal_iff_no_lowDegreeRelation
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsFastAlgebraicallyOptimal
      f ↔
    ¬∃ g h,
        g ≠ 0 ∧
          f * g = h ∧
            FABL.functionAlgebraicDegree
                  g +
                FABL.functionAlgebraicDegree
                  h <
              n

theorem CryptBoolean.algebraicImmunity_le_degree_of_mul_eq_of_ne_zero
  {n : ℕ}
  (f g h : CryptBoolean.BooleanFunction n)
  (hrelation : f * g = h) (hh : h ≠ 0) :
  CryptBoolean.algebraicImmunity f ≤
    FABL.functionAlgebraicDegree h