theorem FABL.sum_sq_vectorFourierCoeff_eq_one
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f) :
  ∑ γ, FABL.vectorFourierCoeff f γ ^ 2 = 1

theorem FABL.exists_inv_card_le_sq_vectorFourierCoeff
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f) :
  ∃ γ,
    (2 ^ n)⁻¹ ≤
      FABL.vectorFourierCoeff f γ ^ 2

theorem FABL.exists_bent_extremal_coefficient
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hn : Even n)
  (hf : FABL.IsSignValued f) :
  ∃ γ,
    (2 ^ (n / 2))⁻¹ ≤
      |FABL.vectorFourierCoeff f γ|

theorem FABL.relativeHammingDist_affineSignFunction
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f)
  (σ : FABL.Sign) (γ : FABL.F₂Cube n) :
  FABL.relativeHammingDist f
      (FABL.affineSignFunction σ γ) =
    1 / 2 -
      FABL.signValue σ *
          FABL.vectorFourierCoeff f γ /
        2

theorem FABL.distanceToAffineSigns_eq {n : ℕ}
  {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f) :
  FABL.distanceToAffineSigns f =
    1 / 2 -
      FABL.spectralInfinityNorm f / 2

theorem FABL.distanceToAffineSigns_le_bentBound
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hn : Even n)
  (hf : FABL.IsSignValued f) :
  FABL.distanceToAffineSigns f ≤
    1 / 2 - (2 ^ (n / 2))⁻¹ / 2

theorem FABL.isBent_iff_distanceToAffineSigns_eq
  {n : ℕ} {f : FABL.F₂Cube n → ℝ}
  (hn : Even n)
  (hf : FABL.IsSignValued f) :
  FABL.IsBent f ↔
    FABL.distanceToAffineSigns f =
      1 / 2 - (2 ^ (n / 2))⁻¹ / 2

theorem FABL.isSignValued_innerProductModTwo
  (n : ℕ) :
  FABL.IsSignValued
    (FABL.innerProductModTwo n)

theorem FABL.isBent_innerProductModTwo (n : ℕ) :
  FABL.IsBent (FABL.innerProductModTwo n)

theorem FABL.isSignValued_completeQuadratic
  (n : ℕ) :
  FABL.IsSignValued
    (FABL.completeQuadratic n)

theorem FABL.isBent_completeQuadratic {n : ℕ}
  (hn : Even n) :
  FABL.IsBent (FABL.completeQuadratic n)

theorem FABL.IsSignValued.directProduct {n m : ℕ}
  {f : FABL.F₂Cube n → ℝ}
  {g : FABL.F₂Cube m → ℝ}
  (hf : FABL.IsSignValued f)
  (hg : FABL.IsSignValued g) :
  FABL.IsSignValued
    (FABL.bentDirectProduct f g)

theorem FABL.IsBent.directProduct {n m : ℕ}
  {f : FABL.F₂Cube n → ℝ}
  {g : FABL.F₂Cube m → ℝ} (hn : Even n)
  (hm : Even m) (hf : FABL.IsBent f)
  (hg : FABL.IsBent g) :
  FABL.IsBent (FABL.bentDirectProduct f g)

theorem FABL.vectorFourierCoeff_bentAffineModulation
  {n : ℕ} (σ : FABL.Sign)
  (a γ : FABL.F₂Cube n)
  (f : FABL.F₂Cube n → ℝ) :
  FABL.vectorFourierCoeff
      (FABL.bentAffineModulation σ a f)
      γ =
    FABL.signValue σ *
      FABL.vectorFourierCoeff f (a + γ)

theorem FABL.IsSignValued.affineModulation {n : ℕ}
  {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f)
  (σ : FABL.Sign) (a : FABL.F₂Cube n) :
  FABL.IsSignValued
    (FABL.bentAffineModulation σ a f)

theorem FABL.IsBent.affineModulation {n : ℕ}
  {f : FABL.F₂Cube n → ℝ} (_hn : Even n)
  (hf : FABL.IsBent f) (σ : FABL.Sign)
  (a : FABL.F₂Cube n) :
  FABL.IsBent
    (FABL.bentAffineModulation σ a f)

theorem FABL.vectorFourierCoeff_bentLinearReindex
  {n : ℕ}
  (M :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n)
  (f : FABL.F₂Cube n → ℝ)
  (γ : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.bentLinearReindex M f) γ =
    FABL.vectorFourierCoeff f
      (FABL.bentDualFrequency M γ)

theorem FABL.IsSignValued.linearReindex {n : ℕ}
  {f : FABL.F₂Cube n → ℝ}
  (hf : FABL.IsSignValued f)
  (M :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  FABL.IsSignValued
    (FABL.bentLinearReindex M f)

theorem FABL.IsBent.linearReindex {n : ℕ}
  {f : FABL.F₂Cube n → ℝ} (_hn : Even n)
  (hf : FABL.IsBent f)
  (M :
    FABL.F₂Cube n ≃ₗ[FABL.𝔽₂]
      FABL.F₂Cube n) :
  FABL.IsBent (FABL.bentLinearReindex M f)

theorem FABL.maioranaMcFarland_joinF₂CubeBlocks
  {n : ℕ} (g : FABL.F₂Cube n → FABL.Sign)
  (x y : FABL.F₂Cube n) :
  FABL.maioranaMcFarland g
      (FABL.joinF₂CubeBlocks x y) =
    FABL.binarySign
        (FABL.f₂DotProduct x y) *
      FABL.signValue (g y)

theorem FABL.vectorFourierCoeff_maioranaMcFarland_joinF₂CubeBlocks
  {n : ℕ} (g : FABL.F₂Cube n → FABL.Sign)
  (a b : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.maioranaMcFarland g)
      (FABL.joinF₂CubeBlocks a b) =
    (2 ^ n)⁻¹ * FABL.signValue (g a) *
      (FABL.vectorWalshCharacter b) a

theorem FABL.isSignValued_maioranaMcFarland
  {n : ℕ}
  (g : FABL.F₂Cube n → FABL.Sign) :
  FABL.IsSignValued
    (FABL.maioranaMcFarland g)

theorem FABL.isBent_maioranaMcFarland {n : ℕ}
  (g : FABL.F₂Cube n → FABL.Sign) :
  FABL.IsBent (FABL.maioranaMcFarland g)

theorem FABL.binaryExtensionField_finrank {ℓ : ℕ}
  (hℓ : ℓ ≠ 0) :
  Module.finrank FABL.𝔽₂
      (FABL.BinaryExtensionField ℓ) =
    ℓ

theorem FABL.binaryExtensionField_natCard {ℓ : ℕ}
  (hℓ : ℓ ≠ 0) :
  Nat.card (FABL.BinaryExtensionField ℓ) =
    2 ^ ℓ

theorem FABL.buildExecutableBinaryFieldModel_complete
  (ℓ : ℕ) (hℓ : 0 < ℓ)
  (x y : FABL.F₂Cube ℓ) :
  x ∈
      (FABL.buildExecutableBinaryFieldModel
          ℓ hℓ).elements ∧
    (x, y, FABL.binaryAdd x y) ∈
        (FABL.buildExecutableBinaryFieldModel
            ℓ hℓ).additionTable ∧
      (x, y,
          FABL.binaryMulMod hℓ
            (FABL.buildExecutableBinaryFieldModel
                ℓ hℓ).implementation
            x y) ∈
        (FABL.buildExecutableBinaryFieldModel
            ℓ hℓ).multiplicationTable

theorem FABL.binaryArithmeticWork_isBigO :
  (fun ℓ =>
      ↑(FABL.binaryArithmeticWork
          ℓ)) =O[Filter.atTop]
    fun ℓ => ↑((ℓ + 1) ^ 2)

theorem FABL.binaryFieldPreprocessingWork_isBigO :
  (fun ℓ =>
      ↑(FABL.binaryFieldPreprocessingWork
          ℓ)) =O[Filter.atTop]
    fun ℓ => ↑(2 ^ (8 * ℓ))

theorem FABL.buildExecutableBinaryFieldModel_resource_bounds
  (ℓ : ℕ) (hℓ : 0 < ℓ) :
  (FABL.buildExecutableBinaryFieldModel ℓ
            hℓ).elements.length =
      2 ^ ℓ ∧
    (FABL.buildExecutableBinaryFieldModel
              ℓ hℓ).additionTable.length =
        2 ^ (2 * ℓ) ∧
      (FABL.buildExecutableBinaryFieldModel
                ℓ
                hℓ).multiplicationTable.length =
          2 ^ (2 * ℓ) ∧
        FABL.binaryFieldRepresentationBits
              ℓ ≤
            FABL.binaryFieldPreprocessingWork
              ℓ ∧
          FABL.binaryFieldPreprocessingWork
                ℓ ≤
              2 ^ (8 * (ℓ + 1)) ∧
            FABL.binaryArithmeticWork ℓ ≤
              8 * (ℓ + 1) ^ 2

theorem FABL.ncard_rootSet_le_natDegree.{u_1}
  {K : Type u_1} [Field K]
  (p : Polynomial K) :
  (p.rootSet K).ncard ≤ p.natDegree

theorem FABL.smallBiasPolynomial_eval {n ℓ : ℕ}
  (γ : FABL.F₂Cube n)
  (r : FABL.BinaryExtensionField ℓ) :
  Polynomial.eval r
      (FABL.smallBiasPolynomial ℓ γ) =
    ∑ i, γ i • r ^ (↑i + 1)

theorem FABL.smallBiasPolynomial_ne_zero {n ℓ : ℕ}
  {γ : FABL.F₂Cube n} (hγ : γ ≠ 0) :
  FABL.smallBiasPolynomial ℓ γ ≠ 0

theorem FABL.smallBiasPolynomial_natDegree_le
  {n ℓ : ℕ} (γ : FABL.F₂Cube n) :
  (FABL.smallBiasPolynomial ℓ
        γ).natDegree ≤
    n

theorem FABL.smallBiasGenerator_characterExpectation_eq_rootProbability
  {n ℓ : ℕ} (hℓ : ℓ ≠ 0)
  {γ : FABL.F₂Cube n} (hγ : γ ≠ 0) :
  (Finset.univ.expect fun rs =>
      (FABL.vectorWalshCharacter γ)
        (FABL.smallBiasGenerator n hℓ rs.1
          rs.2)) =
    ↑((FABL.smallBiasPolynomial ℓ
                γ).rootSet
            (FABL.BinaryExtensionField
              ℓ)).ncard /
      2 ^ ℓ

theorem FABL.smallBiasGenerator_characterExpectation_nonneg
  {n ℓ : ℕ} (hℓ : ℓ ≠ 0)
  {γ : FABL.F₂Cube n} (hγ : γ ≠ 0) :
  0 ≤
    Finset.univ.expect fun rs =>
      (FABL.vectorWalshCharacter γ)
        (FABL.smallBiasGenerator n hℓ rs.1
          rs.2)

theorem FABL.smallBiasGenerator_characterExpectation_le
  {n ℓ : ℕ} (hℓ : ℓ ≠ 0)
  {γ : FABL.F₂Cube n} (hγ : γ ≠ 0) :
  (Finset.univ.expect fun rs =>
      (FABL.vectorWalshCharacter γ)
        (FABL.smallBiasGenerator n hℓ rs.1
          rs.2)) ≤
    ↑n / 2 ^ ℓ

theorem FABL.binaryLowPolynomial_injective
  {ℓ : ℕ} :
  Function.Injective
    FABL.binaryLowPolynomial

theorem FABL.binaryAdjoinRootEncode_injective
  {ℓ : ℕ} (m : FABL.F₂Cube ℓ) :
  Function.Injective
    (FABL.binaryAdjoinRootEncode m)