theorem FABL.variance_pBiasedRandomFunction_fourierCoeff
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Icc 0 1)
  (S : Finset (Fin n)) :
  ProbabilityTheory.variance
      (fun f =>
        FABL.fourierCoeff f.toReal S)
      (FABL.pBiasedRandomFunctionPMF n p
          hp).toMeasure =
    p * (1 - p) / 2 ^ n

theorem FABL.inv_two_pow_pred_le_variance_of_fourierDegree_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℕ) (hk : 0 < k)
  (hdegree :
    FABL.fourierDegree f.toReal ≤ k)
  (hnonconstant : ¬∃ c, f = fun x => c) :
  2⁻¹ ^ (k - 1) ≤ FABL.variance f.toReal

theorem FABL.pow_pred_mul_variance_le_totalStableInfluence_of_fourierDegree_le
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k)
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) :
  ρ ^ (k - 1) * FABL.variance f ≤
    FABL.totalStableInfluence ρ f

theorem FABL.totalStableInfluence_eq_sum_of_dependsOn
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n))
  (hdepends : DependsOn f ↑J) (ρ : ℝ) :
  FABL.totalStableInfluence ρ f =
    ∑ i ∈ J, FABL.stableInfluence ρ f i

theorem FABL.exists_stableInfluence_ge_of_isKJunta_of_nonconstant
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℕ) (hjunta : FABL.IsKJunta f k)
  (hnonconstant : ¬∃ c, f = fun x => c)
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1) :
  ∃ i,
    (1 / 2 - δ / 2) ^ (k - 1) / ↑k ≤
      FABL.stableInfluence (1 - δ)
        f.toReal i

theorem FABL.ProbabilityDensity.IsBiased.convolutionPower
  {n : ℕ} {φ : FABL.ProbabilityDensity n}
  {ε : ℝ} (hφ : φ.IsBiased ε) (d : ℕ) :
  (φ.convolutionPower d).IsBiased (ε ^ d)

theorem FABL.sq_fourierCoeff_le_influence_of_mem
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) (i : Fin n)
  (hi : i ∈ S) :
  FABL.fourierCoeff f S ^ 2 ≤
    FABL.influence f i

theorem FABL.HasSmallInfluences.isFourierRegular_sqrt
  {n : ℕ} {f : FABL.SignCube n → ℝ}
  {ε : ℝ}
  (hsmall : FABL.HasSmallInfluences ε f) :
  FABL.IsFourierRegular (√ε) f

theorem FABL.isFourierRegular_innerProductModTwoBoolean
  (m : ℕ) :
  FABL.IsFourierRegular (2 ^ m)⁻¹
    (FABL.innerProductModTwoBoolean
        m).toReal

theorem FABL.influence_innerProductModTwoBoolean_eq_half
  (m : ℕ) (hm : 0 < m) (i : Fin (m + m)) :
  FABL.influence
      (FABL.innerProductModTwoBoolean
          m).toReal
      i =
    1 / 2

theorem FABL.exists_isFourierRegular_not_hasSmallInfluences_of_even
  (n : ℕ) (hn : Even n) (hnpos : 0 < n) :
  ∃ f,
    FABL.IsFourierRegular (2 ^ (n / 2))⁻¹
        f.toReal ∧
      ∀ {ε : ℝ},
        ε < 1 / 2 →
          ¬FABL.HasSmallInfluences ε
              f.toReal

theorem FABL.exists_hasSmallStableInfluences_not_isFourierRegular
  (n : ℕ) (hn : 0 < n) (δ : ℝ)
  (_hδ : δ ∈ Set.Icc 0 1) :
  ∃ f,
    FABL.HasSmallStableInfluences
        ((1 - δ) ^ (n - 1)) δ f.toReal ∧
      ∀ {ε : ℝ},
        ε < 1 →
          ¬FABL.IsFourierRegular ε
              f.toReal

theorem FABL.fourierCoeff_leadingCoordinateTimes_tailFrequency_eq_zero
  {n : ℕ} (g : FABL.BooleanFunction n)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff
      (FABL.leadingCoordinateTimes
          g).toReal
      (FABL.tailFrequency S) =
    0

theorem FABL.stableInfluence_leadingCoordinateTimes_eq_stabilityCurve
  {n : ℕ} (g : FABL.BooleanFunction n)
  (ρ : ℝ) :
  FABL.stableInfluence ρ
      (FABL.leadingCoordinateTimes
          g).toReal
      0 =
    FABL.stabilityCurve g.toReal ρ

theorem FABL.stableInfluence_leadingCoordinateTimes_majority_odd_eq_noiseStability
  (m : ℕ) (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 1) :
  FABL.stableInfluence (1 - δ)
      (FABL.leadingCoordinateTimes
          (FABL.majority
            (2 * m + 1))).toReal
      0 =
    FABL.noiseStability (1 - δ) ⋯
      (FABL.majority (2 * m + 1)).toReal

theorem FABL.one_sub_sqrt_le_of_hasSmallStableInfluences_leadingCoordinateTimes_majority_odd
  (m : ℕ) {ε δ : ℝ} (hδ : δ ∈ Set.Ioo 0 1)
  (hsmall :
    FABL.HasSmallStableInfluences ε δ
      (FABL.leadingCoordinateTimes
          (FABL.majority
            (2 * m + 1))).toReal) :
  1 - √δ ≤ ε

theorem FABL.isBalanced_majority_odd (m : ℕ) :
  FABL.IsBalanced
    (FABL.majority (2 * m + 1)).toReal

theorem FABL.IsFourierRegular.leadingCoordinateTimes_of_isBalanced
  {n : ℕ} {g : FABL.BooleanFunction n}
  {ε : ℝ}
  (hregular :
    FABL.IsFourierRegular ε g.toReal)
  (hbalanced : FABL.IsBalanced g.toReal)
  (hε : 0 ≤ ε) :
  FABL.IsFourierRegular ε
    (FABL.leadingCoordinateTimes g).toReal

theorem FABL.isFourierRegular_leadingCoordinateTimes_majority_odd
  (m : ℕ) :
  FABL.IsFourierRegular
    (1 / √↑(2 * m + 1))
    (FABL.leadingCoordinateTimes
        (FABL.majority
          (2 * m + 1))).toReal

theorem FABL.rho_pow_card_sub_one_mul_sq_fourierCoeff_le_stableInfluence
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ρ : ℝ) (hρ : 0 ≤ ρ)
  (S : Finset (Fin n)) (i : Fin n)
  (hi : i ∈ S) :
  ρ ^ (S.card - 1) *
      FABL.fourierCoeff f S ^ 2 ≤
    FABL.stableInfluence ρ f i

theorem FABL.HasSmallStableInfluences.isLowDegreeFourierRegular
  {n : ℕ} {f : FABL.SignCube n → ℝ}
  {ε δ : ℝ} {k : ℕ}
  (hsmall :
    FABL.HasSmallStableInfluences ε δ f)
  (hδ : δ ∈ Set.Ico 0 1) :
  FABL.IsLowDegreeFourierRegular
    (√(ε / (1 - δ) ^ (k - 1))) k f

theorem FABL.stableInfluence_zero_eq_sq_fourierCoeff_singleton
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) :
  FABL.stableInfluence 0 f i =
    FABL.fourierCoeff f {i} ^ 2

theorem FABL.hasSmallStableInfluences_one_iff_isLowDegreeFourierRegular_one
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (ε : ℝ) (hε : 0 ≤ ε) :
  FABL.HasSmallStableInfluences ε 1 f ↔
    FABL.IsLowDegreeFourierRegular (√ε) 1
      f

theorem FABL.abs_fourierCoeff_le_influence_of_monotone
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) (S : Finset (Fin n))
  (i : Fin n) (hi : i ∈ S) :
  |FABL.fourierCoeff f.toReal S| ≤
    FABL.influence f.toReal i

theorem FABL.IsLowDegreeFourierRegular.isFourierRegular_and_hasSmallInfluences_of_monotone
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) {ε : ℝ}
  (hregular :
    FABL.IsLowDegreeFourierRegular ε 1
      f.toReal) :
  FABL.IsFourierRegular ε f.toReal ∧
    FABL.HasSmallInfluences ε f.toReal

theorem FABL.mean_signRestriction_eq_restrictionFourierCoeff_empty
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J) :
  FABL.mean (FABL.signRestriction f J z) =
    FABL.restrictionFourierCoeff f J ∅ z

theorem FABL.variance_mean_signRestriction_eq_sum_sq_fixed
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (J : Finset (Fin n)) :
  (FABL.variance fun z =>
      FABL.mean
        (FABL.signRestriction f J z)) =
    ∑ T with T ≠ ∅,
      FABL.fourierCoeff f
          (FABL.liftFixedFrequency T) ^
        2

theorem FABL.exists_signRestriction_mean_change_gt_via_variance
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  {ε : ℝ} {k : ℕ}
  (hregular :
    ¬FABL.IsLowDegreeFourierRegular ε k
        f) :
  ∃ J,
    Fintype.card (FABL.FixedIndex J) ≤ k ∧
      ∃ z,
        ε <
          |FABL.mean
                (FABL.signRestriction f J
                  z) -
              FABL.mean f|

theorem FABL.abs_vectorFourierCoeff_innerProductModTwoSupportDensity
  (m : ℕ) (hm : 0 < m)
  (γ : FABL.F₂Cube (m + m)) (hγ : γ ≠ 0) :
  |FABL.vectorFourierCoeff
        (FABL.innerProductModTwoSupportDensity
            m hm).toFun
        γ| =
    (2 ^ m)⁻¹ / (1 - (2 ^ m)⁻¹)

theorem FABL.innerProductModTwoSupportDensity_isBiased_iff
  (m : ℕ) (hm : 0 < m) (ε : ℝ) :
  (FABL.innerProductModTwoSupportDensity m
          hm).IsBiased
      ε ↔
    (2 ^ m)⁻¹ / (1 - (2 ^ m)⁻¹) ≤ ε

theorem FABL.forall_coordinate_eq_iff_eq_zero_or_eq_one
  {n : ℕ} (hn : 0 < n)
  (x : FABL.F₂Cube n) :
  (∀ (i j : Fin n), x i = x j) ↔
    x = 0 ∨ x = 1

theorem FABL.f₂EqualityFunction_eq_pointIndicators
  {n : ℕ} (hn : 0 < n)
  (x : FABL.F₂Cube n) :
  FABL.f₂EqualityFunction x =
    FABL.f₂PointIndicator 0 x +
      FABL.f₂PointIndicator 1 x

theorem FABL.two_pow_sub_le_hammingNorm_of_functionAlgebraicDegree_le
  {n k : ℕ} (f : FABL.F₂BooleanFunction n)
  (hf : f ≠ 0)
  (hdeg :
    FABL.functionAlgebraicDegree f ≤ k) :
  2 ^ (n - k) ≤ hammingNorm f

theorem FABL.uniformProbability_ne_zero_eq_hammingNorm_ratio
  {n : ℕ} (f : FABL.F₂BooleanFunction n) :
  (FABL.uniformProbability fun x =>
      f x ≠ 0) =
    ↑(hammingNorm f) / 2 ^ n

theorem FABL.inv_two_pow_le_uniformProbability_ne_zero_of_functionAlgebraicDegree_le
  {n k : ℕ} (f : FABL.F₂BooleanFunction n)
  (hf : f ≠ 0)
  (hdeg :
    FABL.functionAlgebraicDegree f ≤ k) :
  2⁻¹ ^ k ≤
    FABL.uniformProbability fun x =>
      f x ≠ 0

theorem FABL.two_pow_functionAlgebraicDegree_le_spectralSparsity_booleanRealEmbedding
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (hf : f ≠ 0) :
  2 ^ FABL.functionAlgebraicDegree f ≤
    FABL.spectralSparsity
      (FABL.booleanRealEmbedding f)

theorem FABL.functionAlgebraicDegree_le_of_isVectorFourierGranular_booleanRealEmbedding
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (k : ℕ)
  (hgranular :
    FABL.IsVectorFourierGranular
      (FABL.booleanRealEmbedding f)
      (2 ^ k)⁻¹) :
  FABL.functionAlgebraicDegree f ≤ k

theorem FABL.realSignEncodedFunction_eq_one_sub_two_booleanRealEmbedding
  {n : ℕ} (f : FABL.F₂BooleanFunction n) :
  FABL.realSignEncodedFunction f =
    fun x =>
    1 - 2 * FABL.booleanRealEmbedding f x

theorem FABL.restrictionFourierCoeff_realSignEncodedFunction_eq_neg_two_mul
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (J : Finset (Fin n)) (A : Finset ↥J)
  (hA : A.Nonempty)
  (z : FABL.FixedSignCube J) :
  FABL.restrictionFourierCoeff
      (FABL.binaryFunctionOnSignCube
        (FABL.realSignEncodedFunction f))
      J A z =
    -2 *
      FABL.restrictionFourierCoeff
        (FABL.binaryFunctionOnSignCube
          (FABL.booleanRealEmbedding f))
        J A z

theorem FABL.functionAlgebraicDegree_le_half_of_isBent
  {n : ℕ} (f : FABL.F₂BooleanFunction n)
  (hn : Even n) (hnTwo : 2 < n)
  (hf :
    FABL.IsBent
      (FABL.realSignEncodedFunction f)) :
  FABL.functionAlgebraicDegree f ≤ n / 2