theorem FABL.noiseOperator_one {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  (FABL.noiseOperator 1) f = f

theorem FABL.uniformLpNorm_two_noiseOperator_le_pow_of_degree
  {n : ℕ} (rho : ℝ) (hrho : 1 ≤ rho)
  (f : FABL.SignCube n → ℝ) (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k) :
  FABL.uniformLpNorm 2
      ((FABL.noiseOperator rho) f) ≤
    rho ^ k * FABL.uniformLpNorm 2 f

theorem FABL.lowDegree_uniformLpNorm_le {n : ℕ}
  (q : ℝ) (hq : 2 ≤ q)
  (f : FABL.SignCube n → ℝ) (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k) :
  FABL.uniformLpNorm q f ≤
    √(q - 1) ^ k * FABL.uniformLpNorm 2 f

theorem FABL.lowDegree_two_le_expFactor_mul
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k)
  (p : ℝ) (hp1 : 1 ≤ p) (hp2 : p ≤ 2) :
  FABL.uniformLpNorm 2 f ≤
    (Real.exp 1 ^ (2 / p - 1)) ^ k *
      FABL.uniformLpNorm p f

theorem FABL.lowDegree_two_le_exp_pow_mul_one
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k) :
  FABL.uniformLpNorm 2 f ≤
    Real.exp 1 ^ k *
      FABL.uniformLpNorm 1 f

theorem FABL.fourierDegree_linearForm_le_one
  {n : ℕ} (a : Fin n → ℝ) :
  FABL.fourierDegree (FABL.linearForm a) ≤
    1

theorem FABL.khintchine_of_le_two {n : ℕ}
  (a : Fin n → ℝ) (p : ℝ) (hp1 : 1 ≤ p)
  (hp2 : p ≤ 2) :
  Real.exp (-(2 / p - 1)) *
        FABL.uniformLpNorm 2
          (FABL.linearForm a) ≤
      FABL.uniformLpNorm p
        (FABL.linearForm a) ∧
    FABL.uniformLpNorm p
        (FABL.linearForm a) ≤
      FABL.uniformLpNorm 2
        (FABL.linearForm a)

theorem FABL.khintchine_of_two_le {n : ℕ}
  (a : Fin n → ℝ) (p : ℝ) (hp : 2 ≤ p) :
  FABL.uniformLpNorm 2
        (FABL.linearForm a) ≤
      FABL.uniformLpNorm p
        (FABL.linearForm a) ∧
    FABL.uniformLpNorm p
        (FABL.linearForm a) ≤
      √(p - 1) *
        FABL.uniformLpNorm 2
          (FABL.linearForm a)

theorem FABL.khintchineInequality {n : ℕ}
  (a : Fin n → ℝ) (p : ℝ) (hp : 1 ≤ p) :
  ∃ c C,
    0 < c ∧
      c < C ∧
        c *
              FABL.uniformLpNorm 2
                (FABL.linearForm a) ≤
            FABL.uniformLpNorm p
              (FABL.linearForm a) ∧
          FABL.uniformLpNorm p
              (FABL.linearForm a) ≤
            C *
              FABL.uniformLpNorm 2
                (FABL.linearForm a)

theorem FABL.lowDegree_tail_bound_parameter
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k)
  (q t : ℝ) (hq : 2 ≤ q) (ht : 0 < t)
  (hnorm : 0 < FABL.uniformLpNorm 2 f) :
  (FABL.uniformProbability fun x =>
      t * FABL.uniformLpNorm 2 f ≤
        |f x|) ≤
    (q ^ (↑k / 2) / t) ^ q

theorem FABL.lowDegree_tail_bound {n : ℕ}
  (f : FABL.SignCube n → ℝ) (k : ℕ)
  (hk : 0 < k)
  (hdegree : FABL.fourierDegree f ≤ k)
  (t : ℝ)
  (ht : (2 * Real.exp 1) ^ (↑k / 2) ≤ t)
  (hnorm : 0 < FABL.uniformLpNorm 2 f) :
  (FABL.uniformProbability fun x =>
      t * FABL.uniformLpNorm 2 f ≤
        |f x|) ≤
    Real.exp
      (-↑k / (2 * Real.exp 1) *
        t ^ (2 / ↑k))

theorem FABL.lowDegree_aboveMean_probability
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (k : ℕ)
  (hdegree : FABL.fourierDegree f ≤ k)
  (hnonconstant :
    ¬∃ c,
        ∀ (x : FABL.SignCube n),
          f x = c) :
  1 / 4 * Real.exp (-2 * ↑k) ≤
    FABL.uniformProbability fun x =>
      FABL.mean f < f x

theorem FABL.uniformLpNorm_zeroOne {n : ℕ}
  (f : FABL.SignCube n → ℝ) (α p : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) (hp : 0 < p) :
  FABL.uniformLpNorm p f = α ^ p⁻¹

theorem FABL.noiseStability_le_uniformLpNorm_oneAdd_sq
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.SignCube n → ℝ) :
  FABL.noiseStability ρ ⋯ f ≤
    FABL.uniformLpNorm (1 + ρ) f ^ 2

theorem FABL.smallSetExpansion {n : ℕ}
  (f : FABL.SignCube n → ℝ) (α ρ : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α)
  (hρ : ρ ∈ Set.Icc 0 1) :
  FABL.noiseStability ρ ⋯ f ≤
    α ^ (2 / (1 + ρ))

theorem FABL.smallSetExpansion_event {n : ℕ}
  (f : FABL.SignCube n → ℝ) (α ρ : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α)
  (hρ : ρ ∈ Set.Icc 0 1) :
  (FABL.pmfEventProbability
      (FABL.correlatedPairPMF ρ ⋯)
      fun xy => f xy.1 = 1 ∧ f xy.2 = 1) ≤
    α ^ (2 / (1 + ρ))

theorem FABL.smallSetExpansion_conditional {n : ℕ}
  (f : FABL.SignCube n → ℝ) (α ρ : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) (hα : 0 < α)
  (hρ : ρ ∈ Set.Icc 0 1) :
  (FABL.pmfEventProbability
        (FABL.correlatedPairPMF ρ ⋯)
        fun xy =>
        f xy.1 = 1 ∧ f xy.2 = 1) /
      α ≤
    α ^ ((1 - ρ) / (1 + ρ))

theorem FABL.stableInfluence_le_booleanInfluence_rpow
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) :
  FABL.stableInfluence ρ f.toReal i ≤
    FABL.booleanInfluence f i ^
      (2 / (1 + ρ))

theorem FABL.rho_pow_mul_fourierWeightAtMost_le_noiseStability
  {n : ℕ} (k : ℕ)
  (f : FABL.SignCube n → ℝ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Ioc 0 1) :
  ρ ^ k * FABL.fourierWeightAtMost k f ≤
    FABL.noiseStability ρ ⋯ f

theorem FABL.fourierWeightAtMost_le_invPow_mul_rpow
  {n : ℕ} (k : ℕ)
  (f : FABL.SignCube n → ℝ) (α ρ : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α)
  (hρ : ρ ∈ Set.Ioc 0 1) :
  FABL.fourierWeightAtMost k f ≤
    ρ⁻¹ ^ k * α ^ (2 / (1 + ρ))

theorem FABL.levelKInequality {n : ℕ}
  (f : FABL.SignCube n → ℝ) (α : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) (k : ℕ)
  (hkpos : 0 < k)
  (hk : ↑k ≤ 2 * Real.log (1 / α)) :
  FABL.fourierWeightAtMost k f ≤
    (2 * Real.exp 1 / ↑k *
          Real.log (1 / α)) ^
        k *
      α ^ 2

theorem FABL.levelOneInequality_sharp {n : ℕ}
  (f : FABL.SignCube n → ℝ) (α : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) :
  FABL.fourierWeightAtLevel 1 f ≤
    2 * α ^ 2 * Real.log (1 / α)