theorem FABL.homogeneousLinearThreshold_isOdd_and_isBalanced
  {n : ℕ} (f : FABL.BooleanFunction n)
  (a : Fin n → ℝ)
  (hrep :
    ∀ (x : FABL.SignCube n),
      f x =
        FABL.thresholdSign
          (FABL.affineLinearForm 0 a x))
  (hmargin :
    ∀ (x : FABL.SignCube n),
      FABL.affineLinearForm 0 a x ≠ 0) :
  Function.Odd f ∧
    FABL.IsBalanced f.toReal

theorem FABL.zero_homogeneousLinearThreshold_counterexample :
  have f := fun x => 1;
  have a := fun x => 0;
  (∀ (x : FABL.SignCube 1),
      f x =
        FABL.thresholdSign
          (FABL.affineLinearForm 0 a x)) ∧
    ¬Function.Odd f ∧
      FABL.mean f.toReal = 1

theorem FABL.mean_nonneg_of_nonnegative_linearThresholdBias
  {n : ℕ} (f : FABL.BooleanFunction n)
  (a₀ : ℝ) (a : Fin n → ℝ)
  (hrep :
    ∀ (x : FABL.SignCube n),
      f x =
        FABL.thresholdSign
          (FABL.affineLinearForm a₀ a x))
  (ha₀ : 0 ≤ a₀) : 0 ≤ FABL.mean f.toReal

theorem FABL.nonnegative_mean_negative_bias_counterexample :
  ∃ f a₀ a,
    a₀ < 0 ∧
      (∀ (x : FABL.SignCube 1),
          f x =
            FABL.thresholdSign
              (FABL.affineLinearForm a₀ a
                x)) ∧
        0 ≤ FABL.mean f.toReal

theorem FABL.exists_homogeneousLinearThresholdRepresentation_of_isBalanced
  {n : ℕ} (g : FABL.BooleanFunction n)
  (hg : FABL.IsLinearThreshold g)
  (hbalanced : FABL.IsBalanced g.toReal) :
  ∃ c,
    ∀ (x : FABL.SignCube n),
      g x =
        FABL.thresholdSign
          (FABL.affineLinearForm 0 c x)

theorem FABL.influence_le_of_abs_linearThresholdWeight_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  (a₀ : ℝ) (a : Fin n → ℝ)
  (hrep :
    ∀ (x : FABL.SignCube n),
      f x =
        FABL.thresholdSign
          (FABL.affineLinearForm a₀ a x))
  {i j : Fin n}
  (hweight : |a i| ≤ |a j|) :
  FABL.influence f.toReal i ≤
    FABL.influence f.toReal j

theorem FABL.natCard_polynomialThresholdFunction_le_profileCount
  (n k : ℕ) :
  Nat.card
      (FABL.PolynomialThresholdFunction n
        k) ≤
    (2 ^ n + 1) ^
      (FABL.lowDegreeFourierFamily n
          k).card

theorem FABL.natCard_linearThresholdFunction_le_profileCount
  (n : ℕ) :
  Nat.card
      (FABL.LinearThresholdFunction n) ≤
    (2 ^ n + 1) ^
      (FABL.lowDegreeFourierFamily n
          1).card

theorem FABL.natCard_linearThresholdFunction_le_two_pow_sq
  (n : ℕ) :
  Nat.card
      (FABL.LinearThresholdFunction n) ≤
    2 ^ (n + 1) ^ 2

theorem FABL.card_lowDegreeFourierFamily_le_leadingTerm
  (n k : ℕ) (hn : 0 < n) :
  (FABL.lowDegreeFourierFamily n k).card ≤
    n ^ k + k * n ^ (k - 1)

theorem FABL.natCard_polynomialThresholdFunction_le_two_pow_bookBound
  (n k : ℕ) :
  Nat.card
      (FABL.PolynomialThresholdFunction n
        k) ≤
    2 ^
      (n ^ (k + 1) + (2 * k + 1) * n ^ k +
        1)

theorem FABL.exists_one_div_sqrt_two_mul_dimension_le_influence_of_balanced_linearThreshold
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 1 ≤ n)
  (hbalanced : FABL.IsBalanced f.toReal)
  (hthreshold :
    FABL.IsLinearThreshold f) :
  ∃ i,
    1 / √(2 * ↑n) ≤
      FABL.influence f.toReal i

theorem FABL.pmfExpectation_apply_left_mul_right_eq_fourierCoeff_mul_correlation
  {n : ℕ}
  (p :
    Fin n → PMF (FABL.Sign × FABL.Sign))
  (ρ : Fin n → ℝ)
  (ha :
    ∀ (i : Fin n),
      (FABL.pmfExpectation (p i) fun z =>
          FABL.signValue z.1) =
        0)
  (hb :
    ∀ (i : Fin n),
      (FABL.pmfExpectation (p i) fun z =>
          FABL.signValue z.2) =
        0)
  (hab :
    ∀ (i : Fin n),
      (FABL.pmfExpectation (p i) fun z =>
          FABL.signValue z.1 *
            FABL.signValue z.2) =
        ρ i)
  (f : FABL.BooleanFunction n)
  (i : Fin n) :
  (FABL.pmfExpectation
      (FABL.independentProductPMF p)
      fun ω =>
      f.toReal
          (FABL.signPairFamilyLeft ω) *
        FABL.signValue
          (FABL.signPairFamilyRight ω
            i)) =
    FABL.fourierCoeff f.toReal {i} * ρ i

theorem FABL.hasEqualSingletonFourierCoefficients_majority
  (n : ℕ) :
  FABL.HasEqualSingletonFourierCoefficients
    (FABL.majority n)

theorem FABL.fourierCoeff_singleton_le_majority_of_equal
  {n : ℕ} (hn : 0 < n)
  (f : FABL.BooleanFunction n)
  (hf :
    FABL.HasEqualSingletonFourierCoefficients
      f)
  (i : Fin n) :
  FABL.fourierCoeff f.toReal {i} ≤
    FABL.fourierCoeff
      (FABL.majority n).toReal {i}

theorem FABL.measure_randomBooleanFunction_fourierInfinityNorm_gt_le
  (n : ℕ) (hn : 2 ≤ n) :
  (FABL.uniformPMF
            (FABL.BooleanFunction
              n)).toMeasure.real
      {f |
        FABL.randomBooleanFourierThreshold
            n <
          FABL.fourierInfinityNorm
            f.toReal} ≤
    2 ^ (-↑n)

theorem FABL.not_isPolynomialThreshold_parityFunction_univ_pred
  {n : ℕ} (hn : 0 < n) :
  ¬FABL.IsPolynomialThreshold
      (FABL.parityFunction Finset.univ)
      (n - 1)

theorem FABL.isPolynomialThreshold_pred_of_ne_parityFunction_univ
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n)
  (hparity :
    f ≠ FABL.parityFunction Finset.univ)
  (hnegParity :
    f ≠
      -FABL.parityFunction Finset.univ) :
  FABL.IsPolynomialThreshold f (n - 1)

theorem FABL.onePointFlippedParity_isPolynomialThreshold
  (k : ℕ) :
  FABL.IsPolynomialThreshold
    (FABL.onePointFlippedParity k) k

theorem FABL.fourierCoeff_onePointFlippedParity
  (k : ℕ) (S : Finset (Fin (k + 1))) :
  FABL.fourierCoeff
      (FABL.onePointFlippedParity
          k).toReal
      S =
    (if Finset.univ = S then 1 else 0) -
      2⁻¹ ^ k

theorem FABL.fourierWeightAtMost_onePointFlippedParity
  (k : ℕ) :
  FABL.fourierWeightAtMost k
      (FABL.onePointFlippedParity
          k).toReal =
    ↑(2 ^ (k + 1) - 1) * (2⁻¹ ^ k) ^ 2

theorem FABL.exists_polynomialThreshold_fourierWeightAtMost_lt_two_mul_invPow
  (k : ℕ) :
  ∃ f,
    FABL.IsPolynomialThreshold f k ∧
      FABL.fourierWeightAtMost k
          f.toReal <
        2 * 2⁻¹ ^ k

theorem FABL.symmetric_hasRealSumOfLinearThresholdsSizeAtMost_two_mul
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsSymmetric f) :
  FABL.HasRealSumOfLinearThresholdsSizeAtMost
    f (2 * n)

theorem FABL.parityFunction_isRealSumOfLinearThresholds
  {n : ℕ} (S : Finset (Fin n)) :
  FABL.IsRealSumOfLinearThresholds
    (FABL.parityFunction S) (n * 2)

theorem FABL.polynomialThresholdRepresentation_hasThresholdOfThresholdsSizeAtMost
  {n : ℕ} (f : FABL.BooleanFunction n)
  (p : FABL.SignCube n → ℝ)
  (hrep :
    FABL.IsPolynomialThresholdRepresentation
      f p) :
  FABL.HasThresholdOfThresholdsSizeAtMost
    f (2 * n * FABL.polynomialSparsity p)

theorem FABL.thresholdOfParities_hasThresholdOfThresholdsSizeAtMost
  {n : ℕ} (f : FABL.BooleanFunction n)
  (s : ℕ)
  (h : FABL.IsThresholdOfParities f s) :
  FABL.HasThresholdOfThresholdsSizeAtMost
    f (2 * n * s)

theorem FABL.completeQuadratic_apply {n : ℕ}
  (x : FABL.F₂Cube n) :
  FABL.completeQuadratic n x =
    FABL.binarySign
      (FABL.completeQuadraticBit x)

theorem FABL.completeQuadraticBoolean_binaryCubeSignEquiv
  {n : ℕ} (x : FABL.F₂Cube n) :
  FABL.completeQuadraticBoolean n
      ((FABL.binaryCubeSignEquiv n) x) =
    FABL.signEncode
      (FABL.completeQuadraticBit x)

theorem FABL.completeQuadraticBoolean_isSymmetric
  {n : ℕ} :
  FABL.IsSymmetric
    (FABL.completeQuadraticBoolean n)

theorem FABL.completeQuadraticBoolean_hasThresholdOfThresholdsSizeAtMost_two_mul
  {n : ℕ} :
  FABL.HasThresholdOfThresholdsSizeAtMost
    (FABL.completeQuadraticBoolean n)
    (2 * n)

theorem FABL.abs_vectorFourierCoeff_completeQuadratic
  {n : ℕ} (hn : Even n)
  (γ : FABL.F₂Cube n) :
  |FABL.vectorFourierCoeff
        (FABL.completeQuadratic n) γ| =
    (2 ^ (n / 2))⁻¹

theorem FABL.completeQuadraticBoolean_toReal
  (n : ℕ) :
  (FABL.completeQuadraticBoolean
        n).toReal =
    FABL.binaryFunctionOnSignCube
      (FABL.completeQuadratic n)

theorem FABL.abs_fourierCoeff_completeQuadraticBoolean
  {n : ℕ} (hn : Even n)
  (S : Finset (Fin n)) :
  |FABL.fourierCoeff
        (FABL.completeQuadraticBoolean
            n).toReal
        S| =
    (2 ^ (n / 2))⁻¹

theorem FABL.pow_two_half_le_polynomialSparsity_completeQuadraticBoolean_of_pos
  {n : ℕ} (hn : Even n) (hnPos : 0 < n)
  (p : FABL.SignCube n → ℝ)
  (hrep :
    FABL.IsPolynomialThresholdRepresentation
      (FABL.completeQuadraticBoolean n)
      p) :
  2 ^ (n / 2) ≤ FABL.polynomialSparsity p

theorem FABL.pow_two_half_le_thresholdOfParitiesSize_completeQuadraticBoolean
  {n : ℕ} (hn : Even n) (hnPos : 0 < n)
  (s : ℕ)
  (h :
    FABL.IsThresholdOfParities
      (FABL.completeQuadraticBoolean n)
      s) :
  2 ^ (n / 2) ≤ s

theorem FABL.DNFTerm.trueIndicator_eq_one_iff
  {n : ℕ} (T : FABL.DNFTerm n)
  (x : FABL.SignCube n) :
  T.trueIndicator x = 1 ↔ T.eval x = -1

theorem FABL.DNFTerm.trueIndicator_nonneg {n : ℕ}
  (T : FABL.DNFTerm n)
  (x : FABL.SignCube n) :
  0 ≤ T.trueIndicator x

theorem FABL.DNFTerm.fourierOneNorm_trueIndicator
  {n : ℕ} (T : FABL.DNFTerm n) :
  FABL.fourierOneNorm T.trueIndicator = 1

theorem FABL.DNFFormula.satisfiedTermCount_eq_zero_of_no_satisfied_term
  {n : ℕ} (φ : FABL.DNFFormula n)
  (x : FABL.SignCube n)
  (hnone :
    ¬∃ T ∈ φ.terms, T.eval x = -1) :
  φ.satisfiedTermCount x = 0