theorem FABL.coordinateResamplingNoisePMF_eq_coordinateNoisePMF
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (x : FABL.Sign) :
  FABL.coordinateResamplingNoisePMF ρ hρ
      x =
    FABL.coordinateNoisePMF ρ ⋯ x

theorem FABL.resamplingNoiseKernel_eq_noiseKernel
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (x : FABL.SignCube n) :
  FABL.resamplingNoiseKernel ρ hρ x =
    FABL.noiseKernel ρ ⋯ x

theorem FABL.correlatedPairPMF_map_swap {n : ℕ}
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  PMF.map Prod.swap
      (FABL.correlatedPairPMF ρ hρ) =
    FABL.correlatedPairPMF ρ hρ

theorem FABL.correlatedPairPMF_expect_signValue_fst
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) (i : Fin n) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ hρ)
      fun xy => FABL.signValue (xy.1 i)) =
    0

theorem FABL.correlatedPairPMF_expect_signValue_snd
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) (i : Fin n) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ hρ)
      fun xy => FABL.signValue (xy.2 i)) =
    0

theorem FABL.correlatedPairPMF_expect_signValue_mul
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) (i : Fin n) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ hρ)
      fun xy =>
      FABL.signValue (xy.1 i) *
        FABL.signValue (xy.2 i)) =
    ρ

theorem FABL.noiseStability_toReal_eq_agreement_sub_disagreement
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f : FABL.BooleanFunction n) :
  FABL.noiseStability ρ hρ f.toReal =
    FABL.correlatedAgreementProbability ρ
        hρ f -
      FABL.correlatedDisagreementProbability
        ρ hρ f

theorem FABL.noiseStability_toReal_eq_two_mul_agreement_sub_one
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f : FABL.BooleanFunction n) :
  FABL.noiseStability ρ hρ f.toReal =
    2 *
        FABL.correlatedAgreementProbability
          ρ hρ f -
      1

theorem FABL.noiseSensitivity_eq_half_sub_half_noiseStability
  {n : ℕ} (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BooleanFunction n) :
  FABL.noiseSensitivity δ hδ f =
    (1 -
        FABL.noiseStability (1 - 2 * δ) ⋯
          f.toReal) /
      2

theorem FABL.noiseStability_const_one {n : ℕ}
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  (FABL.noiseStability ρ hρ fun x => 1) =
    1

theorem FABL.noiseStability_const_neg_one {n : ℕ}
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  (FABL.noiseStability ρ hρ fun x => -1) =
    1

theorem FABL.noiseStability_dictator {n : ℕ}
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1)
  (i : Fin n) :
  FABL.noiseStability ρ hρ
      (FABL.dictator i).toReal =
    ρ

theorem FABL.noiseSensitivity_dictator {n : ℕ}
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (i : Fin n) :
  FABL.noiseSensitivity δ hδ
      (FABL.dictator i) =
    δ

theorem FABL.noiseStability_parityFunction {n : ℕ}
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1)
  (S : Finset (Fin n)) :
  FABL.noiseStability ρ hρ
      (FABL.parityFunction S).toReal =
    ρ ^ S.card

theorem FABL.tendsto_noiseStability_majority_odd
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  Filter.Tendsto
    (fun k =>
      FABL.noiseStability ρ hρ
        (FABL.majority
            (2 * k + 1)).toReal)
    Filter.atTop
    (nhds (2 / Real.pi * Real.arcsin ρ))

theorem FABL.two_div_pi_mul_arcsin_eq_one_sub_two_div_pi_mul_arccos
  (ρ : ℝ) :
  2 / Real.pi * Real.arcsin ρ =
    1 - 2 / Real.pi * Real.arccos ρ

theorem FABL.tendsto_noiseStability_majority_odd_arccos
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  Filter.Tendsto
    (fun k =>
      FABL.noiseStability ρ hρ
        (FABL.majority
            (2 * k + 1)).toReal)
    Filter.atTop
    (nhds
      (1 - 2 / Real.pi * Real.arccos ρ))

theorem FABL.tendsto_noiseSensitivity_majority_odd
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1) :
  Filter.Tendsto
    (fun k =>
      FABL.noiseSensitivity δ hδ
        (FABL.majority (2 * k + 1)))
    Filter.atTop
    (nhds
      (Real.arccos (1 - 2 * δ) / Real.pi))

theorem FABL.arccos_one_sub_two_mul_eq_two_mul_arcsin_sqrt
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1) :
  Real.arccos (1 - 2 * δ) =
    2 * Real.arcsin √δ

theorem FABL.arccos_one_sub_two_mul_sub_two_mul_sqrt_isBigO :
  (fun δ =>
      Real.arccos (1 - 2 * δ) -
        2 *
          √δ) =O[nhdsWithin 0 (Set.Ici 0)]
    fun δ => δ ^ (3 / 2)

theorem FABL.majorityNoiseSensitivityLimit_sub_two_div_pi_mul_sqrt_isBigO :
  (fun δ =>
      Real.arccos (1 - 2 * δ) / Real.pi -
        2 / Real.pi *
          √δ) =O[nhdsWithin 0 (Set.Ici 0)]
    fun δ => δ ^ (3 / 2)

theorem FABL.noiseOperator_apply_eq_pmfExpectation
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  (FABL.noiseOperator ρ) f x =
    FABL.pmfExpectation
      (FABL.noiseKernel ρ hρ x) f

theorem FABL.noiseOperator_monomial_apply {n : ℕ}
  (ρ : ℝ) (S : Finset (Fin n))
  (x : FABL.SignCube n) :
  (FABL.noiseOperator ρ) (FABL.monomial S)
      x =
    ρ ^ S.card * FABL.monomial S x

theorem FABL.noiseOperator_fourier_expansion
  {n : ℕ} (ρ : ℝ)
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  (FABL.noiseOperator ρ) f x =
    ∑ S,
      ρ ^ S.card * FABL.fourierCoeff f S *
        FABL.monomial S x

theorem FABL.noiseOperator_eq_sum_degreePart
  {n : ℕ} (ρ : ℝ)
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  (FABL.noiseOperator ρ) f x =
    ∑ k ∈ Finset.range (n + 1),
      ρ ^ k * FABL.degreePart k f x

theorem FABL.noiseStability_eq_uniformInner_noiseOperator
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f : FABL.SignCube n → ℝ) :
  FABL.noiseStability ρ hρ f =
    FABL.uniformInner f
      ((FABL.noiseOperator ρ) f)

theorem FABL.noiseStability_eq_sum_rho_pow_mul_sq_fourierCoeff
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f : FABL.SignCube n → ℝ) :
  FABL.noiseStability ρ hρ f =
    ∑ S,
      ρ ^ S.card *
        FABL.fourierCoeff f S ^ 2

theorem FABL.noiseStability_eq_sum_level_rho_pow_mul_fourierWeight
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f : FABL.SignCube n → ℝ) :
  FABL.noiseStability ρ hρ f =
    ∑ k ∈ Finset.range (n + 1),
      ρ ^ k *
        FABL.fourierWeightAtLevel k f

theorem FABL.noiseStability_toReal_eq_spectralSample_moment
  {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f : FABL.BooleanFunction n) :
  FABL.noiseStability ρ hρ f.toReal =
    FABL.pmfExpectation
      (FABL.spectralSample f) fun S =>
      ρ ^ S.card

theorem FABL.noiseSensitivity_eq_sum_level {n : ℕ}
  (δ : ℝ) (hδ : δ ∈ Set.Icc 0 1)
  (f : FABL.BooleanFunction n) :
  FABL.noiseSensitivity δ hδ f =
    1 / 2 *
      ∑ k ∈ Finset.range (n + 1),
        (1 - (1 - 2 * δ) ^ k) *
          FABL.fourierWeightAtLevel k
            f.toReal

theorem FABL.noiseStability_le_rho_of_balanced
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioo 0 1)
  (f : FABL.BooleanFunction n)
  (hf : FABL.IsBalanced f.toReal) :
  FABL.noiseStability ρ ⋯ f.toReal ≤ ρ

theorem FABL.noiseStability_eq_rho_iff_signed_dictator
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioo 0 1)
  (f : FABL.BooleanFunction n)
  (hf : FABL.IsBalanced f.toReal) :
  FABL.noiseStability ρ ⋯ f.toReal = ρ ↔
    ∃ i,
      f = FABL.dictator i ∨
        f = -FABL.dictator i

theorem FABL.deriv_stabilityCurve_zero {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  deriv (FABL.stabilityCurve f) 0 =
    FABL.fourierWeightAtLevel 1 f