theorem FABL.biasMean_mem_Icc (p : ℝ)
  (hp : p ∈ Set.Icc 0 1) :
  FABL.biasMean p ∈ Set.Icc (-1) 1

theorem FABL.biasSigma_sq (p : ℝ)
  (hp : p ∈ Set.Icc 0 1) :
  FABL.biasSigma p ^ 2 =
    FABL.biasVarianceScale p

theorem FABL.biasSigma_pos (p : ℝ)
  (hp : p ∈ Set.Ioo 0 1) :
  0 < FABL.biasSigma p

theorem FABL.biasedStandardizedSign_one_eq_sqrt
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1) :
  FABL.biasedStandardizedSign p 1 =
    √(p / (1 - p))

theorem FABL.biasedStandardizedSign_neg_one_eq_neg_sqrt
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1) :
  FABL.biasedStandardizedSign p (-1) =
    -√((1 - p) / p)

theorem FABL.pmfExpectation_biasedStandardizedSign
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1) :
  FABL.pmfExpectation
      (FABL.biasedSignPMF p ⋯)
      (FABL.biasedStandardizedSign p) =
    0

theorem FABL.pmfExpectation_biasedStandardizedSign_sq
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1) :
  (FABL.pmfExpectation
      (FABL.biasedSignPMF p ⋯) fun x =>
      FABL.biasedStandardizedSign p x ^
        2) =
    1

theorem FABL.biasedSignPMF_apply_toReal (p : ℝ)
  (hp : p ∈ Set.Icc 0 1) (x : FABL.Sign) :
  ((FABL.biasedSignPMF p hp) x).toReal =
    if x = 1 then 1 - p else p

theorem FABL.biasedSignPMF_hasFullSupport (p : ℝ)
  (hp : p ∈ Set.Ioo 0 1) :
  FABL.PMFHasFullSupport
    (FABL.biasedSignPMF p ⋯)

theorem FABL.pmfExpectation_biasedSignPMF_signValue
  (p : ℝ) (hp : p ∈ Set.Icc 0 1) :
  FABL.pmfExpectation
      (FABL.biasedSignPMF p hp)
      FABL.signValue =
    FABL.biasMean p

theorem FABL.biasedSiteFourierFunction_orthonormal
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (a b : Fin 2) :
  (FABL.pmfExpectation
      (FABL.biasedSignPMF p ⋯) fun x =>
      FABL.biasedSiteFourierFunction p a
          x *
        FABL.biasedSiteFourierFunction p b
          x) =
    if a = b then 1 else 0

theorem FABL.biasedMonomial_apply {n : ℕ} (p : ℝ)
  (hp : p ∈ Set.Ioo 0 1)
  (S : Finset (Fin n))
  (x : FABL.SignCube n) :
  FABL.biasedMonomial p hp S x =
    ∏ i ∈ S,
      FABL.biasedStandardizedSign p (x i)

theorem FABL.biasedFourierCoeff_eq_expect {n : ℕ}
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  FABL.biasedFourierCoeff p hp f S =
    FABL.pmfExpectation
      (FABL.productProbabilityPMF
        (FABL.biasedSignPMF p ⋯) n)
      fun x =>
      f x * FABL.biasedMonomial p hp S x

theorem FABL.biased_fourier_expansion {n : ℕ}
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  f x =
    ∑ S,
      FABL.biasedFourierCoeff p hp f S *
        FABL.biasedMonomial p hp S x

theorem FABL.signValue_eq_biasMean_add_sigma_mul_biasedMonomial_singleton
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (i : Fin n) (x : FABL.SignCube n) :
  FABL.signValue (x i) =
    FABL.biasMean p +
      FABL.biasSigma p *
        FABL.biasedMonomial p hp {i} x

theorem FABL.biasedFourierCoeff_dictator {n : ℕ}
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (i : Fin n) (S : Finset (Fin n)) :
  FABL.biasedFourierCoeff p hp
      (fun x => FABL.signValue (x i)) S =
    if S = ∅ then FABL.biasMean p
    else
      if S = {i} then FABL.biasSigma p
      else 0

theorem FABL.biasedFourierCoeff_dictator_empty
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (i : Fin n) :
  FABL.biasedFourierCoeff p hp
      (fun x => FABL.signValue (x i)) ∅ =
    FABL.biasMean p

theorem FABL.biasedFourierCoeff_dictator_singleton
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (i : Fin n) :
  FABL.biasedFourierCoeff p hp
      (fun x => FABL.signValue (x i))
      {i} =
    FABL.biasSigma p

theorem FABL.biasedFourierCoeff_dictator_other
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (i : Fin n) (S : Finset (Fin n))
  (hS0 : S ≠ ∅) (hSi : S ≠ {i}) :
  FABL.biasedFourierCoeff p hp
      (fun x => FABL.signValue (x i)) S =
    0

theorem FABL.selectionFunction_biased_expansion
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (x : FABL.SignCube 3) :
  FABL.signValue
      (FABL.selectionFunction x) =
    FABL.biasMean p +
            (1 / 2 -
                  FABL.biasMean p / 2) *
                FABL.biasSigma p *
              FABL.biasedMonomial p hp {1}
                x +
          (1 / 2 + FABL.biasMean p / 2) *
              FABL.biasSigma p *
            FABL.biasedMonomial p hp {2}
              x -
        1 / 2 * FABL.biasSigma p ^ 2 *
          FABL.biasedMonomial p hp {0, 1}
            x +
      1 / 2 * FABL.biasSigma p ^ 2 *
        FABL.biasedMonomial p hp {0, 2} x

theorem FABL.biasedFourierCoeff_biasedView {n : ℕ}
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  FABL.biasedFourierCoeff p hp
      (FABL.biasedView p hp f) S =
    FABL.biasedFourierCoeff p hp f S

theorem FABL.biasedDiscreteDerivative_eq_sigma_mul
  {n : ℕ} (p : ℝ) (i : Fin n)
  (f : FABL.SignCube n → ℝ) :
  FABL.biasedDiscreteDerivative p i f =
    fun x =>
    FABL.biasSigma p *
      (FABL.discreteDerivative i) f x

theorem FABL.biasSigma_mul_standardizedSign_difference_div_two
  (p : ℝ) (hp : p ∈ Set.Ioo 0 1) :
  FABL.biasSigma p *
        (FABL.biasedStandardizedSign p 1 -
          FABL.biasedStandardizedSign p
            (-1)) /
      2 =
    1

theorem FABL.biasedDiscreteDerivative_biasedMonomial
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (i : Fin n) (S : Finset (Fin n))
  (x : FABL.SignCube n) :
  FABL.biasedDiscreteDerivative p i
      (FABL.biasedMonomial p hp S) x =
    if i ∈ S then
      FABL.biasedMonomial p hp (S.erase i)
        x
    else 0

theorem FABL.biasedDiscreteDerivative_eq_fourier_sum
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.SignCube n → ℝ) (i : Fin n)
  (x : FABL.SignCube n) :
  FABL.biasedDiscreteDerivative p i f x =
    ∑ S with i ∈ S,
      FABL.biasedFourierCoeff p hp f S *
        FABL.biasedMonomial p hp
          (S.erase i) x

theorem FABL.coordinateConditionalVariance_biasedSignPMF_toReal
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.BooleanFunction n) (i : Fin n)
  (x : FABL.SignCube n) :
  FABL.coordinateConditionalVariance
      (FABL.biasedSignPMF p ⋯) f.toReal i
      x =
    FABL.biasSigma p ^ 2 *
      if
          f x ≠
            f
              (FABL.flipCoordinate x
                i) then
        1
      else 0

theorem FABL.productInfluence_biased_eq_sigma_sq_mul_flipProbability
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.BooleanFunction n)
  (i : Fin n) :
  FABL.productInfluence
      (FABL.biasedSignPMF p ⋯) f.toReal
      i =
    FABL.biasSigma p ^ 2 *
      FABL.biasedFlipProbability p hp f i

theorem FABL.productTotalInfluence_biased_eq_sigma_sq_mul_expect_sensitivity
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.BooleanFunction n) :
  FABL.productTotalInfluence
      (FABL.biasedSignPMF p ⋯) f.toReal =
    FABL.biasSigma p ^ 2 *
      FABL.productMean
        (FABL.biasedSignPMF p ⋯) fun x =>
        ↑(FABL.biasedSensitivity f x)

theorem FABL.biasedFourierCoeff_singleton_eq_sigma_mul_expect_discreteDerivative
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.SignCube n → ℝ) (i : Fin n) :
  FABL.biasedFourierCoeff p hp f {i} =
    FABL.biasSigma p *
      FABL.productMean
        (FABL.biasedSignPMF p ⋯)
        ((FABL.discreteDerivative i) f)

theorem FABL.productInfluence_biased_eq_sigma_mul_singletonCoeff_of_monotone
  {n : ℕ} (p : ℝ) (hp : p ∈ Set.Ioo 0 1)
  (f : FABL.BooleanFunction n)
  (hf : Monotone f) (i : Fin n) :
  FABL.productInfluence
      (FABL.biasedSignPMF p ⋯) f.toReal
      i =
    FABL.biasSigma p *
      FABL.biasedFourierCoeff p hp
        f.toReal {i}