theorem FABL.bonamiLemma_fourthMoment {n k : ℕ}
  (f : FABL.SignCube n → ℝ)
  (hdegree : FABL.fourierDegree f ≤ k) :
  (Finset.univ.expect fun x => f x ^ 4) ≤
    9 ^ k *
      (Finset.univ.expect fun x =>
          f x ^ 2) ^
        2

theorem FABL.twoQHypercontractivity_of_two_lt
  {n : ℕ} (q : ℝ) (hq : 2 < q)
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm q
      ((FABL.noiseOperator (1 / √(q - 1)))
        f) ≤
    FABL.uniformLpNorm 2 f

theorem FABL.twoQHypercontractivity {n : ℕ}
  (q : ℝ) (hq : 2 ≤ q)
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm q
      ((FABL.noiseOperator (1 / √(q - 1)))
        f) ≤
    FABL.uniformLpNorm 2 f

theorem FABL.pTwoHypercontractivity {n : ℕ}
  (p : ℝ) (hp1 : 1 ≤ p) (hp2 : p ≤ 2)
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm 2
      ((FABL.noiseOperator √(p - 1)) f) ≤
    FABL.uniformLpNorm p f

theorem FABL.noiseStability_pSubOne_le_uniformLpNorm_sq
  (n : ℕ) (p : ℝ) (hp1 : 1 ≤ p)
  (hp2 : p ≤ 2)
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformInner f
      ((FABL.noiseOperator (p - 1)) f) ≤
    FABL.uniformLpNorm p f ^ 2

theorem FABL.isReasonable_const_mul_iff.{u_1}
  {Ω : Type u_1} [Fintype Ω] (p : PMF Ω)
  (B c : ℝ) (hc : c ≠ 0) (X : Ω → ℝ) :
  (FABL.IsReasonable p B fun x =>
      c * X x) ↔
    FABL.IsReasonable p B X

theorem FABL.uniformSign_isReasonable :
  FABL.IsReasonable
    (FABL.uniformPMF FABL.Sign) 1
    FABL.signValue

theorem FABL.sparseBernoulli_isReasonable
  (n : ℕ) :
  let q := 1 / 2 ^ n;
  have hq := ⋯;
  FABL.IsReasonable
    (FABL.pBiasedBitPMF q hq) (2 ^ n)
    FABL.zeroOneValue

theorem FABL.sparseBernoulli_not_reasonable_of_lt
  (n : ℕ) {B : ℝ} (hB : B < 2 ^ n) :
  let q := 1 / 2 ^ n;
  have hq := ⋯;
  ¬FABL.IsReasonable
      (FABL.pBiasedBitPMF q hq) B
      FABL.zeroOneValue

theorem FABL.standardGaussian_secondMoment :
  ∫ (x : ℝ),
      x ^
        2 ∂ProbabilityTheory.gaussianReal
        0 1 =
    1

theorem FABL.standardGaussian_fourthMoment :
  ∫ (x : ℝ),
      x ^
        4 ∂ProbabilityTheory.gaussianReal
        0 1 =
    3

theorem FABL.standardGaussian_isThreeReasonable :
  FABL.IsReasonableMeasure
    (ProbabilityTheory.gaussianReal 0 1) 3
    fun x => x

theorem FABL.integral_pow_uniformIntervalMeasure
  (m : ℕ) :
  ∫ (x : ℝ),
      x ^ m ∂FABL.uniformIntervalMeasure =
    FABL.uniformIntervalMoment m

theorem FABL.uniformIntervalMoment_two :
  FABL.uniformIntervalMoment 2 = 1 / 3

theorem FABL.uniformIntervalMoment_four :
  FABL.uniformIntervalMoment 4 = 1 / 5

theorem FABL.uniformInterval_isNineFifthsReasonable :
  FABL.uniformIntervalMoment 4 ≤
    9 / 5 *
      FABL.uniformIntervalMoment 2 ^ 2

theorem FABL.uniformIntervalMeasure_isNineFifthsReasonable :
  FABL.IsReasonableMeasure
    FABL.uniformIntervalMeasure (9 / 5)
    fun x => x

theorem FABL.reasonable_tail_le.{u_1}
  {Ω : Type u_1} [Fintype Ω] (p : PMF Ω)
  (B : ℝ) (X : Ω → ℝ)
  (hX : FABL.IsReasonable p B X)
  (hne : FABL.NonzeroUnder p X) (t : ℝ)
  (ht : 0 < t) :
  (FABL.pmfEventProbability p fun x =>
      t *
          √(FABL.pmfExpectation p fun y =>
              X y ^ 2) ≤
        |X x|) ≤
    B / t ^ 4

theorem FABL.pmfPaleyZygmund.{u_1} {Ω : Type u_1}
  [Fintype Ω] (p : PMF Ω) (Y : Ω → ℝ)
  (hY : ∀ (x : Ω), 0 ≤ Y x) (θ : ℝ)
  (hθ₀ : 0 ≤ θ) (hθ₁ : θ < 1) :
  (1 - θ) ^ 2 *
      FABL.pmfExpectation p Y ^ 2 ≤
    (FABL.pmfEventProbability p fun x =>
        θ * FABL.pmfExpectation p Y <
          Y x) *
      FABL.pmfExpectation p fun x =>
        Y x ^ 2

theorem FABL.reasonable_anticoncentration.{u_1}
  {Ω : Type u_1} [Fintype Ω] (p : PMF Ω)
  (B : ℝ) (X : Ω → ℝ)
  (hX : FABL.IsReasonable p B X)
  (hne : FABL.NonzeroUnder p X) (t : ℝ)
  (ht : t ∈ Set.Icc 0 1) :
  (1 - t ^ 2) ^ 2 / B ≤
    FABL.pmfEventProbability p fun x =>
      t *
          √(FABL.pmfExpectation p fun y =>
              X y ^ 2) <
        |X x|

theorem FABL.minimumPositiveAtom_pos.{u_1}
  {Ω : Type u_1} [Fintype Ω] (p : PMF Ω) :
  0 < FABL.minimumPositiveAtom p

theorem FABL.reasonable_of_minimumPositiveAtom.{u_1}
  {Ω : Type u_1} [Fintype Ω] (p : PMF Ω)
  (X : Ω → ℝ) :
  FABL.IsReasonable p
    (1 / FABL.minimumPositiveAtom p) X

theorem FABL.equation9_1_expect_fourth {n : ℕ}
  (d e : FABL.SignCube n → ℝ)
  (f : FABL.SignCube (n + 1) → ℝ)
  (hf :
    ∀ (b : FABL.Sign)
      (x : Fin n → FABL.Sign),
      f (Fin.cons b x) =
        FABL.signValue b * d x + e x) :
  (Finset.univ.expect fun x => f x ^ 4) =
    ((Finset.univ.expect fun x =>
          d x ^ 4) +
        6 *
          Finset.univ.expect fun x =>
            d x ^ 2 * e x ^ 2) +
      Finset.univ.expect fun x => e x ^ 4

theorem FABL.equation9_2_expect_sq {n : ℕ}
  (d e : FABL.SignCube n → ℝ)
  (f : FABL.SignCube (n + 1) → ℝ)
  (hf :
    ∀ (b : FABL.Sign)
      (x : Fin n → FABL.Sign),
      f (Fin.cons b x) =
        FABL.signValue b * d x + e x) :
  (Finset.univ.expect fun x => f x ^ 2) =
    (Finset.univ.expect fun x =>
        d x ^ 2) +
      Finset.univ.expect fun x => e x ^ 2

theorem FABL.reasonableProductPolynomial_isReasonable.{u_1}
  {n : ℕ} {Ω : Fin n → Type u_1}
  [(i : Fin n) → Fintype (Ω i)]
  (p : (i : Fin n) → PMF (Ω i))
  (X : (i : Fin n) → Ω i → ℝ) (B : ℝ)
  (a : Finset (Fin n) → ℝ) (k : ℕ)
  (hmean :
    ∀ (i : Fin n),
      FABL.pmfExpectation (p i) (X i) = 0)
  (hthird :
    ∀ (i : Fin n),
      (FABL.pmfExpectation (p i) fun z =>
          X i z ^ 3) =
        0)
  (hreasonable :
    ∀ (i : Fin n),
      FABL.IsReasonable (p i) B (X i))
  (hdegree :
    FABL.MultilinearDegreeAtMost a k) :
  FABL.IsReasonable
    (FABL.independentProductPMF p)
    (max B 9 ^ k)
    (FABL.productMultilinearRandomVariable
      a X)

theorem FABL.lowDegree_anticoncentration {n : ℕ}
  (f : FABL.SignCube n → ℝ) (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k)
  (hf :
    ¬∃ c,
        ∀ (x : FABL.SignCube n),
          f x = c) :
  9 / 16 / 9 ^ k ≤
    FABL.uniformProbability fun x =>
      1 / 2 * √(FABL.variance f) <
        |f x - FABL.mean f|

theorem FABL.expect_centeredSingletonSquare_sq_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  (δ : ℝ) (hδ₀ : 0 ≤ δ)
  (hδ : δ ≤ 1 / 1600)
  (hweight :
    FABL.fourierWeightAtLevel 1 f.toReal =
      1 - δ) :
  (Finset.univ.expect fun x =>
      FABL.centeredLinearSquare
          (fun i =>
            FABL.fourierCoeff f.toReal
              {i})
          x ^
        2) ≤
    6400 * δ

theorem FABL.fkn_small {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hn : 0 < n) (δ : ℝ) (hδ₀ : 0 ≤ δ)
  (hδ : δ ≤ 1 / 1600)
  (hweight :
    FABL.fourierWeightAtLevel 1 f.toReal =
      1 - δ) :
  ∃ i,
    FABL.relativeHammingDist f
          (FABL.dictator i) ≤
        1601 * δ ∨
      FABL.relativeHammingDist f
          (-FABL.dictator i) ≤
        1601 * δ