theorem FABL.noiseOperator_degreePart {n : ℕ}
  (rho : ℝ) (k : ℕ)
  (f : FABL.SignCube n → ℝ) :
  (FABL.noiseOperator rho)
      (FABL.degreePart k f) =
    fun x =>
    rho ^ k * FABL.degreePart k f x

theorem FABL.homogeneous_twoFour_estimate {n : ℕ}
  (k : ℕ) (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm 4
        ((FABL.noiseOperator
            FABL.twoFourNoiseRoot)
          (FABL.degreePart k f)) =
      FABL.twoFourNoiseRoot ^ k *
        FABL.uniformLpNorm 4
          (FABL.degreePart k f) ∧
    FABL.twoFourNoiseRoot ^ k *
        FABL.uniformLpNorm 4
          (FABL.degreePart k f) ≤
      FABL.uniformLpNorm 2
        (FABL.degreePart k f)

theorem FABL.twoFourHypercontractive_fourthMoment
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  (Finset.univ.expect fun x =>
      (FABL.noiseOperator
            FABL.twoFourNoiseRoot)
          f x ^
        4) ≤
    (Finset.univ.expect fun x =>
        f x ^ 2) ^
      2

theorem FABL.uniformLpNorm_four_pow_eq_expect_fourth.{u_1}
  {Ω : Type u_1} [Fintype Ω] (f : Ω → ℝ) :
  FABL.uniformLpNorm 4 f ^ 4 =
    Finset.univ.expect fun x => f x ^ 4

theorem FABL.twoFourHypercontractivity {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm 4
      ((FABL.noiseOperator
          FABL.twoFourNoiseRoot)
        f) ≤
    FABL.uniformLpNorm 2 f

theorem FABL.uniformInner_le_uniformLpNorm_fourThird_mul_four.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  (f g : Ω → ℝ) :
  FABL.uniformInner f g ≤
    FABL.uniformLpNorm (4 / 3) f *
      FABL.uniformLpNorm 4 g

theorem FABL.fourThirdTwoHypercontractivity
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm 2
      ((FABL.noiseOperator
          FABL.twoFourNoiseRoot)
        f) ≤
    FABL.uniformLpNorm (4 / 3) f

theorem FABL.noiseStability_oneThird_le_uniformLpNorm_fourThird_sq
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.noiseStability (1 / 3)
      FABL.noiseStability_oneThird_le_uniformLpNorm_fourThird_sq._proof_1
      f ≤
    FABL.uniformLpNorm (4 / 3) f ^ 2

theorem FABL.uniformLpNorm_fourThird_sq_of_zeroOne
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (α : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) :
  FABL.uniformLpNorm (4 / 3) f ^ 2 =
    α ^ (3 / 2)

theorem FABL.smallSetExpansion_oneThird {n : ℕ}
  (f : FABL.SignCube n → ℝ) (α : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) :
  FABL.noiseStability (1 / 3)
      FABL.noiseStability_oneThird_le_uniformLpNorm_fourThird_sq._proof_1
      f ≤
    α ^ (3 / 2)

theorem FABL.smallSetExpansion_oneThird_event
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (α : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) :
  (FABL.pmfEventProbability
      (FABL.correlatedPairPMF (1 / 3)
        FABL.noiseStability_oneThird_le_uniformLpNorm_fourThird_sq._proof_1)
      fun xy => f xy.1 = 1 ∧ f xy.2 = 1) ≤
    α ^ (3 / 2)

theorem FABL.smallSetExpansion_oneThird_conditional
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (α : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) (hα : 0 < α) :
  (FABL.pmfEventProbability
        (FABL.correlatedPairPMF (1 / 3)
          FABL.noiseStability_oneThird_le_uniformLpNorm_fourThird_sq._proof_1)
        fun xy =>
        f xy.1 = 1 ∧ f xy.2 = 1) /
      α ≤
    √α

theorem FABL.mean_pointSubcubeIndicator (k : ℕ) :
  FABL.mean
      (FABL.pointSubcubeIndicator k) =
    (2 ^ k)⁻¹

theorem FABL.pointSubcube_oneThird_stayProbability
  (k : ℕ) :
  have x₀ := fun x => 1;
  FABL.pmfExpectation
      (FABL.noiseKernel (1 / 3)
        FABL.noiseStability_oneThird_le_uniformLpNorm_fourThird_sq._proof_1
        x₀)
      (FABL.pointSubcubeIndicator k) =
    (2 / 3) ^ k

theorem FABL.stableHypercubeEdgeWeight_nonneg
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (x y : FABL.SignCube n) :
  0 ≤
    FABL.stableHypercubeEdgeWeight ρ hρ x
      y

theorem FABL.stableHypercubeEdgeWeight_eq_uniform_mul_transition
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (x y : FABL.SignCube n) :
  FABL.stableHypercubeEdgeWeight ρ hρ x
      y =
    ((FABL.uniformPMF (FABL.SignCube n))
          x).toReal *
      ((FABL.noiseKernel ρ hρ x) y).toReal

theorem FABL.sum_stableHypercubeEdgeWeight {n : ℕ}
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  ∑ xy,
      FABL.stableHypercubeEdgeWeight ρ hρ
        xy.1 xy.2 =
    1

theorem FABL.stableHypercubeEdgeWeight_comm
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (x y : FABL.SignCube n) :
  FABL.stableHypercubeEdgeWeight ρ hρ x
      y =
    FABL.stableHypercubeEdgeWeight ρ hρ y
      x

theorem FABL.stableHypercubeUndirectedEdgeWeight_eq_two_mul
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (x y : FABL.SignCube n) :
  FABL.stableHypercubeUndirectedEdgeWeight
      ρ hρ x y =
    2 *
      FABL.stableHypercubeEdgeWeight ρ hρ
        x y

theorem FABL.sum_stableHypercubeEdgeWeight_outgoing
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (x : FABL.SignCube n) :
  ∑ y,
      FABL.stableHypercubeEdgeWeight ρ hρ
        x y =
    (2 ^ n)⁻¹

theorem FABL.sum_stableHypercubeEdgeWeight_incoming
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (y : FABL.SignCube n) :
  ∑ x,
      FABL.stableHypercubeEdgeWeight ρ hρ
        x y =
    (2 ^ n)⁻¹

theorem FABL.coordinateNoisePMF_noisy_apply_toReal
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (x y : FABL.Sign) :
  ((FABL.coordinateNoisePMF (1 - 2 * δ) ⋯
          x)
        y).toReal =
    if x = y then 1 - δ else δ

theorem FABL.noiseKernel_noisy_apply_toReal
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (x y : FABL.SignCube n) :
  ((FABL.noiseKernel (1 - 2 * δ) ⋯ x)
        y).toReal =
    δ ^ hammingDist x y *
      (1 - δ) ^ (n - hammingDist x y)

theorem FABL.noisyHypercubeUndirectedEdgeWeight_eq_hamming
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (x y : FABL.SignCube n) :
  FABL.stableHypercubeUndirectedEdgeWeight
      (1 - 2 * δ) ⋯ x y =
    2 ^ (1 - ↑n) * δ ^ hammingDist x y *
      (1 - δ) ^ (n - hammingDist x y)

theorem FABL.exp_neg_stableHypercubeContinuousTime
  (rho : ℝ) (hrho : 0 < rho) :
  Real.exp
      (-FABL.stableHypercubeContinuousTime
          rho) =
    rho

theorem FABL.stableInfluence_oneThird_le_booleanInfluence_mul_sqrt
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  FABL.stableInfluence (1 / 3) f.toReal
      i ≤
    FABL.booleanInfluence f i *
      √(FABL.booleanInfluence f i)

theorem FABL.stableInfluence_oneThird_le_booleanInfluence_rpow
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  FABL.stableInfluence (1 / 3) f.toReal
      i ≤
    FABL.booleanInfluence f i ^ (3 / 2)

theorem FABL.oneThird_pow_mul_fourierWeightAtMost_le_noiseStability
  {n : ℕ} (k : ℕ)
  (f : FABL.SignCube n → ℝ) :
  (1 / 3) ^ k *
      FABL.fourierWeightAtMost k f ≤
    FABL.noiseStability (1 / 3)
      FABL.noiseStability_oneThird_le_uniformLpNorm_fourThird_sq._proof_1
      f

theorem FABL.fourierWeightAtMost_le_three_pow_mul_rpow
  {n : ℕ} (k : ℕ)
  (f : FABL.SignCube n → ℝ) (α : ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = α) :
  FABL.fourierWeightAtMost k f ≤
    3 ^ k * α ^ (3 / 2)