theorem FABL.measure_pBiasedRandomFunction_fourierFailure_le
  (n : ℕ) (hn : 1 < n) (p : ℝ)
  (hp : p ∈ Set.Icc 0 1) :
  (FABL.pBiasedRandomFunctionPMF n p
            hp).toMeasure.real
      {f |
        FABL.randomBooleanFourierThreshold
              n <
            |FABL.fourierCoeff f.toReal
                  ∅ -
                p| ∨
          ∃ S,
            S.Nonempty ∧
              FABL.randomBooleanFourierThreshold
                  n <
                |FABL.fourierCoeff
                    f.toReal S|} ≤
    2 ^ (-↑n)

theorem FABL.isFourierRegular_uniformLpNorm_one
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.IsFourierRegular
    (FABL.uniformLpNorm 1 f) f

theorem FABL.measure_pBiasedRandomFunction_not_isFourierRegular_le
  (n : ℕ) (hn : 1 < n) (p : ℝ)
  (hp : p ∈ Set.Icc 0 1) :
  (FABL.pBiasedRandomFunctionPMF n p
            hp).toMeasure.real
      {f |
        ¬FABL.IsFourierRegular
            (FABL.randomBooleanFourierThreshold
              n)
            f.toReal} ≤
    2 ^ (-↑n)

theorem FABL.isFourierRegular_zero_iff_exists_const
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.IsFourierRegular 0 f ↔
    ∃ c, f = fun x => c

theorem FABL.isFourierRegular_setIndicator_binaryAffineSubspace_of_codimension
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) (k : ℕ)
  (hcodim : FABL.f₂Codimension H = k) :
  FABL.IsFourierRegular (2 ^ k)⁻¹
    (FABL.binaryFunctionOnSignCube
      (FABL.setIndicator
        ↑(FABL.binaryAffineSubspace H a)))

theorem FABL.isFourierRegular_innerProductModTwo_zeroOne
  (m : ℕ) :
  FABL.IsFourierRegular (2 ^ (m + 1))⁻¹
    (FABL.binaryFunctionOnSignCube
      (FABL.booleanRealEmbedding
        (FABL.booleanFunctionF₂Encoding
          (FABL.innerProductModTwoBoolean
            m))))

theorem FABL.isFourierRegular_completeQuadratic_zeroOne
  (n : ℕ) (hn : Even n) :
  FABL.IsFourierRegular
    (2 ^ (n / 2 + 1))⁻¹
    (FABL.binaryFunctionOnSignCube
      (FABL.booleanRealEmbedding
        (FABL.booleanFunctionF₂Encoding
          (FABL.completeQuadraticBoolean
            n))))

theorem FABL.parityFunction_not_isFourierRegular_of_lt_one
  {n : ℕ} (S : Finset (Fin n))
  (hS : S.Nonempty) {ε : ℝ} (hε : ε < 1) :
  ¬FABL.IsFourierRegular ε
      (FABL.parityFunction S).toReal

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

theorem FABL.ProbabilityDensity.isBiased_iff_expectation
  {n : ℕ} (φ : FABL.ProbabilityDensity n)
  (ε : ℝ) :
  φ.IsBiased ε ↔
    ∀ (γ : FABL.F₂Cube n),
      γ ≠ 0 →
        |φ.expectation fun x =>
              (FABL.vectorWalshCharacter
                  γ)
                x| ≤
          ε

theorem FABL.ProbabilityDensity.vectorFourierCoeff_coordinateMarginal
  {n : ℕ} (φ : FABL.ProbabilityDensity n)
  (J : Finset (Fin n))
  (γ : FABL.F₂Cube J.card) :
  FABL.vectorFourierCoeff
      (φ.coordinateMarginal J).toFun γ =
    FABL.vectorFourierCoeff φ.toFun
      (FABL.coordinateFrequencyLift J γ)

theorem FABL.ProbabilityDensity.IsBiased.coordinateMarginal
  {n : ℕ} {φ : FABL.ProbabilityDensity n}
  {ε : ℝ} (hφ : φ.IsBiased ε)
  (J : Finset (Fin n)) :
  (φ.coordinateMarginal J).IsBiased ε

theorem FABL.ProbabilityDensity.isBiased_one
  {n : ℕ}
  (φ : FABL.ProbabilityDensity n) :
  φ.IsBiased 1

theorem FABL.ProbabilityDensity.isBiased_zero_iff_eq_uniform
  {n : ℕ}
  (φ : FABL.ProbabilityDensity n) :
  φ.IsBiased 0 ↔ φ.toFun = fun x => 1

theorem FABL.ProbabilityDensity.affineSubspaceDensity_not_isBiased_of_lt_one
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) (hH : H ≠ ⊤) {ε : ℝ}
  (hε : ε < 1) :
  ¬(FABL.subsetDensity
          ↑(FABL.binaryAffineSubspace H a)
          ⋯).IsBiased
      ε

theorem FABL.ProbabilityDensity.constantPairDensity_not_isBiased_of_two_le
  {n : ℕ} (hn : 2 ≤ n) {ε : ℝ}
  (hε : ε < 1) :
  ¬(FABL.ProbabilityDensity.constantPairDensity
          n).IsBiased
      ε

theorem FABL.ProbabilityDensity.constantPairDensity_one_isBiased_zero :
  (FABL.ProbabilityDensity.constantPairDensity
        1).IsBiased
    0

theorem FABL.vectorFourierFourthMoment_sub_mean_pow_four_le
  {n : ℕ} (f : FABL.F₂Cube n → ℝ) {ε : ℝ}
  (hregular :
    FABL.IsFourierRegular ε
      (FABL.binaryFunctionOnSignCube f)) :
  FABL.vectorFourierFourthMoment f -
      FABL.mean f ^ 4 ≤
    ε ^ 2 * FABL.variance f

theorem FABL.epsilon_pow_four_le_vectorFourierFourthMoment_sub_mean_pow_four
  {n : ℕ} (f : FABL.F₂Cube n → ℝ) {ε : ℝ}
  (hε : 0 ≤ ε)
  (hregular :
    ¬FABL.IsFourierRegular ε
        (FABL.binaryFunctionOnSignCube
          f)) :
  ε ^ 4 ≤
    FABL.vectorFourierFourthMoment f -
      FABL.mean f ^ 4

theorem FABL.vectorFourierFourthMoment_eq_additiveEnergy
  {n : ℕ} (f : FABL.F₂Cube n → ℝ) :
  FABL.vectorFourierFourthMoment f =
    Finset.univ.expect fun x =>
      Finset.univ.expect fun y =>
        Finset.univ.expect fun z =>
          f x * f y * f z * f (x + y + z)

theorem FABL.pmfExpectation_uniformBooleanFunction_stableInfluence_one_sub
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (i : Fin n) :
  (FABL.pmfExpectation
      (FABL.uniformPMF
        (FABL.BooleanFunction n))
      fun f =>
      FABL.stableInfluence (1 - δ)
        f.toReal i) =
    (1 - δ / 2) ^ n / (2 - δ)

theorem FABL.stableInfluence_one_eq_influence
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) :
  FABL.stableInfluence 1 f i =
    FABL.influence f i

theorem FABL.hasSmallInfluences_iff {n : ℕ}
  (ε : ℝ) (f : FABL.SignCube n → ℝ) :
  FABL.HasSmallInfluences ε f ↔
    ∀ (i : Fin n), FABL.influence f i ≤ ε

theorem FABL.const_hasSmallStableInfluences_zero_zero
  {n : ℕ} (c : ℝ) :
  FABL.HasSmallStableInfluences 0 0
    fun x => c

theorem FABL.hasSmallInfluences_zero_iff_exists_const
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.HasSmallInfluences 0 f ↔
    ∃ c, f = fun x => c

theorem FABL.majority_hasSmallInfluences (n : ℕ) :
  FABL.HasSmallInfluences (1 / √↑n)
    (FABL.majority n).toReal

theorem FABL.stableInfluence_parityFunction
  {n : ℕ} (ρ : ℝ) (S : Finset (Fin n))
  (i : Fin n) :
  FABL.stableInfluence ρ
      (FABL.parityFunction S).toReal i =
    if i ∈ S then ρ ^ (S.card - 1) else 0

theorem FABL.parityFunction_hasSmallStableInfluences_of_log_bound
  {n : ℕ} (S : Finset (Fin n)) (ε δ : ℝ)
  (hε : 0 < ε) (hδ : δ ∈ Set.Ioc 0 1)
  (hcard :
    Real.log (Real.exp 1 / ε) / δ ≤
      ↑S.card) :
  FABL.HasSmallStableInfluences ε δ
    (FABL.parityFunction S).toReal

theorem FABL.exists_stableInfluence_ge_of_isKJunta_of_balanced
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℕ) (hk : 0 < k)
  (hjunta : FABL.IsKJunta f k)
  (hbalanced : FABL.IsBalanced f.toReal)
  (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 1) :
  ∃ i,
    (1 - δ) ^ (k - 1) / ↑k ≤
      FABL.stableInfluence (1 - δ)
        f.toReal i

theorem FABL.not_hasSmallStableInfluences_of_isKJunta_of_balanced
  {n : ℕ} (f : FABL.BooleanFunction n)
  (k : ℕ) (hk : 0 < k)
  (hjunta : FABL.IsKJunta f k)
  (hbalanced : FABL.IsBalanced f.toReal)
  (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 1) :
  ¬FABL.HasSmallStableInfluences
      ((1 - δ) ^ k / ↑k) δ f.toReal

theorem FABL.one_sub_sqrt_le_stableInfluence_leadingCoordinateTimes_majority_odd
  (m : ℕ) (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1) :
  1 - √δ ≤
    FABL.stableInfluence (1 - δ)
      (FABL.leadingCoordinateTimes
          (FABL.majority
            (2 * m + 1))).toReal
      0

theorem FABL.IsFourierRegular.isLowDegreeFourierRegular
  {n : ℕ} {ε : ℝ}
  {f : FABL.SignCube n → ℝ}
  (h : FABL.IsFourierRegular ε f)
  (k : ℕ) :
  FABL.IsLowDegreeFourierRegular ε k f

theorem FABL.isLowDegreeFourierRegular_dimension_iff
  {n : ℕ} (ε : ℝ)
  (f : FABL.SignCube n → ℝ) :
  FABL.IsLowDegreeFourierRegular ε n f ↔
    FABL.IsFourierRegular ε f

theorem FABL.IsLowDegreeFourierRegular.abs_mean_signRestriction_sub_mean_le
  {n : ℕ} {ε : ℝ} {k : ℕ}
  {f : FABL.SignCube n → ℝ}
  (hregular :
    FABL.IsLowDegreeFourierRegular ε k f)
  (hε : 0 ≤ ε) (J : Finset (Fin n))
  (z : FABL.FixedSignCube J)
  (hJ :
    Fintype.card (FABL.FixedIndex J) ≤
      k) :
  |FABL.mean
          (FABL.signRestriction f J z) -
        FABL.mean f| ≤
    2 ^ k * ε

theorem FABL.exists_signRestriction_mean_change_gt_of_not_isLowDegreeFourierRegular
  {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|