theorem FABL.two_mul_variance_le_totalInfluence_of_even
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (hf : Function.Even f) :
  2 * FABL.variance f ≤
    FABL.totalInfluence f

theorem FABL.rademacherNorm_even.{u_1} {n : ℕ}
  {V : Type u_1} [NormedAddCommGroup V]
  [NormedSpace ℝ V] (w : Fin n → V) :
  Function.Even (FABL.rademacherNorm w)

theorem FABL.laplacian_rademacherNorm_le.{u_1}
  {n : ℕ} {V : Type u_1}
  [NormedAddCommGroup V] [NormedSpace ℝ V]
  (w : Fin n → V) (x : FABL.SignCube n) :
  FABL.laplacian (FABL.rademacherNorm w)
      x ≤
    FABL.rademacherNorm w x

theorem FABL.two_mul_variance_rademacherNorm_le_secondMoment.{u_1}
  {n : ℕ} {V : Type u_1}
  [NormedAddCommGroup V] [NormedSpace ℝ V]
  (w : Fin n → V) :
  2 *
      FABL.variance
        (FABL.rademacherNorm w) ≤
    Finset.univ.expect fun x =>
      FABL.rademacherNorm w x ^ 2

theorem FABL.khintchineKahane.{u_1} {n : ℕ}
  {V : Type u_1} [NormedAddCommGroup V]
  [NormedSpace ℝ V] (w : Fin n → V) :
  1 / √2 *
      √(Finset.univ.expect fun x =>
          FABL.rademacherNorm w x ^ 2) ≤
    Finset.univ.expect fun x =>
      FABL.rademacherNorm w x

theorem FABL.rademacherNorm_two_equal_weights_moments :
  (Finset.univ.expect fun x =>
        FABL.rademacherNorm (fun x => 1)
          x) =
      1 ∧
    (Finset.univ.expect fun x =>
        FABL.rademacherNorm (fun x => 1)
            x ^
          2) =
      2

theorem FABL.khintchineKahane_constant_le_inv_sqrt_two
  (c : ℝ)
  (h :
    c *
        √(Finset.univ.expect fun x =>
            FABL.rademacherNorm
                (fun x => 1) x ^
              2) ≤
      Finset.univ.expect fun x =>
        FABL.rademacherNorm (fun x => 1)
          x) :
  c ≤ 1 / √2

theorem FABL.abs_fourierCoeff_le_uniformLpNorm_one
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  |FABL.fourierCoeff f S| ≤
    FABL.uniformLpNorm 1 f

theorem FABL.abs_apply_le_fourierOneNorm {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  |f x| ≤ FABL.fourierOneNorm f

theorem FABL.f₂CubeBlockEquiv_joinF₂CubeBlocks
  {n : ℕ} (x y : FABL.F₂Cube n) :
  (FABL.f₂CubeBlockEquiv n)
      (FABL.joinF₂CubeBlocks x y) =
    (x, y)

theorem FABL.joinF₂CubeBlocks_castAdd {n : ℕ}
  (x y : FABL.F₂Cube n) (i : Fin n) :
  FABL.joinF₂CubeBlocks x y
      (Fin.castAdd n i) =
    x i

theorem FABL.joinF₂CubeBlocks_natAdd {n : ℕ}
  (x y : FABL.F₂Cube n) (i : Fin n) :
  FABL.joinF₂CubeBlocks x y
      (Fin.natAdd n i) =
    y i

theorem FABL.joinF₂CubeBlocks_addNat {n : ℕ}
  (x y : FABL.F₂Cube n) (i : Fin n) :
  FABL.joinF₂CubeBlocks x y (i.addNat n) =
    y i

theorem FABL.innerProductModTwoBit_joinF₂CubeBlocks
  {n : ℕ} (x y : FABL.F₂Cube n) :
  FABL.innerProductModTwoBit
      (FABL.joinF₂CubeBlocks x y) =
    FABL.f₂DotProduct x y

theorem FABL.f₂DotProduct_joinF₂CubeBlocks {n : ℕ}
  (a b x y : FABL.F₂Cube n) :
  FABL.f₂DotProduct
      (FABL.joinF₂CubeBlocks a b)
      (FABL.joinF₂CubeBlocks x y) =
    FABL.f₂DotProduct a x +
      FABL.f₂DotProduct b y

theorem FABL.innerProductModTwo_joinF₂CubeBlocks
  {n : ℕ} (x y : FABL.F₂Cube n) :
  FABL.innerProductModTwo n
      (FABL.joinF₂CubeBlocks x y) =
    FABL.binarySign
      (FABL.f₂DotProduct x y)

theorem FABL.vectorWalshCharacter_joinF₂CubeBlocks
  {n : ℕ} (a b x y : FABL.F₂Cube n) :
  (FABL.vectorWalshCharacter
        (FABL.joinF₂CubeBlocks a b))
      (FABL.joinF₂CubeBlocks x y) =
    (FABL.vectorWalshCharacter a) x *
      (FABL.vectorWalshCharacter b) y

theorem FABL.vectorFourierCoeff_innerProductModTwo_joinF₂CubeBlocks
  {n : ℕ} (a b : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.innerProductModTwo n)
      (FABL.joinF₂CubeBlocks a b) =
    (2 ^ n)⁻¹ *
      FABL.binarySign
        (FABL.f₂DotProduct a b)

theorem FABL.abs_vectorFourierCoeff_innerProductModTwo
  {n : ℕ} (γ : FABL.F₂Cube (n + n)) :
  |FABL.vectorFourierCoeff
        (FABL.innerProductModTwo n) γ| =
    (2 ^ n)⁻¹

theorem FABL.innerProductModTwoBoolean_toReal
  (n : ℕ) :
  (FABL.innerProductModTwoBoolean
        n).toReal =
    FABL.binaryFunctionOnSignCube
      (FABL.innerProductModTwo n)

theorem FABL.abs_fourierCoeff_innerProductModTwoBoolean
  {n : ℕ} (S : Finset (Fin (n + n))) :
  |FABL.fourierCoeff
        (FABL.innerProductModTwoBoolean
            n).toReal
        S| =
    (2 ^ n)⁻¹

theorem FABL.exists_integer_linearThresholdRepresentation
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f) :
  ∃ a₀ a,
    (∀ (x : FABL.SignCube n),
        f x =
          FABL.thresholdSign
            (↑a₀ +
              ∑ i,
                ↑(a i) *
                  FABL.signValue (x i))) ∧
      ∀ (x : FABL.SignCube n),
        ↑a₀ +
            ∑ i,
              ↑(a i) *
                FABL.signValue (x i) ≠
          0

theorem FABL.exists_integer_polynomialThresholdRepresentation
  {n : ℕ} (f : FABL.BooleanFunction n)
  (d : ℕ)
  (hf : FABL.IsPolynomialThreshold f d) :
  ∃ p,
    FABL.IsPolynomialThresholdRepresentation
        f p ∧
      FABL.fourierDegree p ≤ d ∧
        (∀ (S : Finset (Fin n)),
            ∃ z,
              FABL.fourierCoeff p S =
                ↑z) ∧
          ∀ (x : FABL.SignCube n), p x ≠ 0

theorem FABL.eq_of_isLinearThreshold_of_fourierCoeff_eq
  {n : ℕ} (f g : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f)
  (hcoeff :
    ∀ (S : Finset (Fin n)),
      S.card ≤ 1 →
        FABL.fourierCoeff g.toReal S =
          FABL.fourierCoeff f.toReal S) :
  g = f

theorem FABL.homogenizedAffineLinearForm_fin_cons
  {n : ℕ} (a₀ : ℝ) (a : Fin n → ℝ)
  (b : FABL.Sign) (x : FABL.SignCube n) :
  FABL.homogenizedAffineLinearForm a₀ a
      (Fin.cons b x) =
    a₀ * FABL.signValue b +
      FABL.linearForm a x

theorem FABL.uniformLpNorm_one_homogenizedAffineLinearForm
  {n : ℕ} (a₀ : ℝ) (a : Fin n → ℝ) :
  FABL.uniformLpNorm 1
      (FABL.homogenizedAffineLinearForm a₀
        a) =
    FABL.uniformLpNorm 1
      (FABL.affineLinearForm a₀ a)

theorem FABL.uniformLpNorm_two_sq_homogenizedAffineLinearForm
  {n : ℕ} (a₀ : ℝ) (a : Fin n → ℝ) :
  FABL.uniformLpNorm 2
        (FABL.homogenizedAffineLinearForm
          a₀ a) ^
      2 =
    FABL.uniformLpNorm 2
        (FABL.affineLinearForm a₀ a) ^
      2

theorem FABL.uniformLpNorm_two_homogenizedAffineLinearForm
  {n : ℕ} (a₀ : ℝ) (a : Fin n → ℝ) :
  FABL.uniformLpNorm 2
      (FABL.homogenizedAffineLinearForm a₀
        a) =
    FABL.uniformLpNorm 2
      (FABL.affineLinearForm a₀ a)

theorem FABL.affineKhintchineKahane {n : ℕ}
  (a₀ : ℝ) (a : Fin n → ℝ) :
  1 / √2 *
      FABL.uniformLpNorm 2
        (FABL.affineLinearForm a₀ a) ≤
    FABL.uniformLpNorm 1
      (FABL.affineLinearForm a₀ a)

theorem FABL.fourierDegree_affineLinearForm_le_one
  {n : ℕ} (a₀ : ℝ) (a : Fin n → ℝ) :
  FABL.fourierDegree
      (FABL.affineLinearForm a₀ a) ≤
    1

theorem FABL.one_half_le_fourierWeightAtMost_one_of_isLinearThreshold
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f) :
  1 / 2 ≤
    FABL.fourierWeightAtMost 1 f.toReal

theorem FABL.fourBitEquality_polynomialThresholdRepresentation :
  FABL.IsPolynomialThresholdRepresentation
    FABL.fourBitEquality
    FABL.fourBitEqualityPolynomial

theorem FABL.fourierDegree_fourBitEqualityPolynomial_le :
  FABL.fourierDegree
      FABL.fourBitEqualityPolynomial ≤
    2

theorem FABL.fourBitEquality_isPolynomialThreshold :
  FABL.IsPolynomialThreshold
    FABL.fourBitEquality 2

theorem FABL.polynomialSparsity_fourBitEqualityPolynomial :
  FABL.polynomialSparsity
      FABL.fourBitEqualityPolynomial =
    7

theorem FABL.exists_polynomialThreshold_relativeHammingDist_le_three_mul_noiseSensitivity
  {n : ℕ} (f : FABL.BooleanFunction n)
  {δ : ℝ} (hδpos : 0 < δ)
  (hδhalf : δ ≤ 1 / 2) :
  ∃ g,
    FABL.IsPolynomialThreshold g
        ⌊1 / δ⌋₊ ∧
      ↑⌊1 / δ⌋₊ ≤ 1 / δ ∧
        FABL.relativeHammingDist f g ≤
          3 * FABL.noiseSensitivity δ ⋯ f

theorem FABL.eq_of_polynomialThresholdRepresentation_of_fourierCoeff_eq
  {n : ℕ} (f g : FABL.BooleanFunction n)
  (p : FABL.SignCube n → ℝ) (k : ℕ)
  (hrep :
    FABL.IsPolynomialThresholdRepresentation
      f p)
  (hdegree : FABL.fourierDegree p ≤ k)
  (hp : ∀ (x : FABL.SignCube n), p x ≠ 0)
  (hcoeff :
    ∀ (S : Finset (Fin n)),
      S.card ≤ k →
        FABL.fourierCoeff g.toReal S =
          FABL.fourierCoeff f.toReal S) :
  g = f

theorem FABL.eq_of_isPolynomialThreshold_of_fourierCoeff_eq
  {n : ℕ} (f g : FABL.BooleanFunction n)
  (k : ℕ)
  (hf : FABL.IsPolynomialThreshold f k)
  (hcoeff :
    ∀ (S : Finset (Fin n)),
      S.card ≤ k →
        FABL.fourierCoeff g.toReal S =
          FABL.fourierCoeff f.toReal S) :
  g = f