theorem FABL.isPivotal_iff_setCoordinate_ne.{u_1}
  {n : ℕ} {β : Type u_1}
  (f : FABL.SignCube n → β) (i : Fin n)
  (x : FABL.SignCube n) :
  FABL.IsPivotal f i x ↔
    f (FABL.setCoordinate x i 1) ≠
      f (FABL.setCoordinate x i (-1))

theorem FABL.booleanInfluence_eq_dimensionEdgeBoundaryFraction
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  FABL.booleanInfluence f i =
    FABL.dimensionEdgeBoundaryFraction f i

theorem FABL.booleanInfluence_dictator_self
  {n : ℕ} (i : Fin n) :
  FABL.booleanInfluence (FABL.dictator i)
      i =
    1

theorem FABL.booleanInfluence_dictator_of_ne
  {n : ℕ} (i j : Fin n) (hji : j ≠ i) :
  FABL.booleanInfluence (FABL.dictator i)
      j =
    0

theorem FABL.booleanInfluence_neg_dictator {n : ℕ}
  (i j : Fin n) :
  FABL.booleanInfluence
      (fun x => -FABL.dictator i x) j =
    if j = i then 1 else 0

theorem FABL.booleanInfluence_const {n : ℕ}
  (c : FABL.Sign) (i : Fin n) :
  FABL.booleanInfluence (fun x => c) i = 0

theorem FABL.booleanInfluence_orFunction {n : ℕ}
  (i : Fin n) :
  FABL.booleanInfluence
      (FABL.orFunction n) i =
    1 / 2 ^ (n - 1)

theorem FABL.booleanInfluence_andFunction {n : ℕ}
  (i : Fin n) :
  FABL.booleanInfluence
      (FABL.andFunction n) i =
    1 / 2 ^ (n - 1)

theorem FABL.booleanInfluence_majority_three
  (i : Fin 3) :
  FABL.booleanInfluence (FABL.majority 3)
      i =
    1 / 2

theorem FABL.booleanInfluence_majority_odd (m : ℕ)
  (i : Fin (2 * m + 1)) :
  FABL.booleanInfluence
      (FABL.majority (2 * m + 1)) i =
    ↑((2 * m).choose m) / 2 ^ (2 * m)

theorem FABL.discreteDerivative_apply {n : ℕ}
  (i : Fin n) (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  (FABL.discreteDerivative i) f x =
    (f (FABL.setCoordinate x i 1) -
        f (FABL.setCoordinate x i (-1))) /
      2

theorem FABL.discreteDerivative_add {n : ℕ}
  (i : Fin n)
  (f g : FABL.SignCube n → ℝ) :
  (FABL.discreteDerivative i) (f + g) =
    (FABL.discreteDerivative i) f +
      (FABL.discreteDerivative i) g

theorem FABL.discreteDerivative_setCoordinate
  {n : ℕ} (i : Fin n)
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) (b : FABL.Sign) :
  (FABL.discreteDerivative i) f
      (FABL.setCoordinate x i b) =
    (FABL.discreteDerivative i) f x

theorem FABL.sq_discreteDerivative_toReal_eq_pivotalIndicator
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) (x : FABL.SignCube n) :
  (FABL.discreteDerivative i) f.toReal x ^
      2 =
    FABL.pivotalIndicator f i x

theorem FABL.booleanInfluence_eq_influence_toReal
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  FABL.booleanInfluence f i =
    FABL.influence f.toReal i

theorem FABL.isRelevant_iff_exists_setCoordinate_ne
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) :
  FABL.IsRelevant f i ↔
    ∃ x,
      f (FABL.setCoordinate x i 1) ≠
        f (FABL.setCoordinate x i (-1))

theorem FABL.discreteDerivative_eq_fourier_sum
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) (x : FABL.SignCube n) :
  (FABL.discreteDerivative i) f x =
    ∑ S with i ∈ S,
      FABL.fourierCoeff f S *
        FABL.monomial (S.erase i) x

theorem FABL.influence_eq_sum_sq_fourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) :
  FABL.influence f i =
    ∑ S with i ∈ S,
      FABL.fourierCoeff f S ^ 2

theorem FABL.influence_eq_fourierCoeff_singleton_of_monotone
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) (i : Fin n) :
  FABL.influence f.toReal i =
    FABL.fourierCoeff f.toReal {i}

theorem FABL.influence_le_one_div_sqrt_of_transitiveSymmetric_monotone
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hsymm : FABL.IsTransitiveSymmetric f)
  (hf : Monotone f) (i : Fin n) :
  FABL.influence f.toReal i ≤ 1 / √↑n

theorem FABL.coordinateExpectation_apply {n : ℕ}
  (i : Fin n) (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  (FABL.coordinateExpectation i) f x =
    (f (FABL.setCoordinate x i 1) +
        f (FABL.setCoordinate x i (-1))) /
      2

theorem FABL.coordinateExpectation_eq_fourier_sum
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) (x : FABL.SignCube n) :
  (FABL.coordinateExpectation i) f x =
    ∑ S with i ∉ S,
      FABL.fourierCoeff f S *
        FABL.monomial S x

theorem FABL.eq_signValue_mul_discreteDerivative_add_coordinateExpectation
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) (x : FABL.SignCube n) :
  f x =
    FABL.signValue (x i) *
        (FABL.discreteDerivative i) f x +
      (FABL.coordinateExpectation i) f x

theorem FABL.coordinateExpectation_setCoordinate
  {n : ℕ} (i : Fin n)
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) (b : FABL.Sign) :
  (FABL.coordinateExpectation i) f
      (FABL.setCoordinate x i b) =
    (FABL.coordinateExpectation i) f x

theorem FABL.coordinateLaplacian_eq_sub_flip_div_two
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) (x : FABL.SignCube n) :
  (FABL.coordinateLaplacian i) f x =
    (f x - f (FABL.flipCoordinate x i)) /
      2

theorem FABL.coordinateLaplacian_eq_signValue_mul_discreteDerivative
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) (x : FABL.SignCube n) :
  (FABL.coordinateLaplacian i) f x =
    FABL.signValue (x i) *
      (FABL.discreteDerivative i) f x

theorem FABL.coordinateLaplacian_eq_fourier_sum
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) (x : FABL.SignCube n) :
  (FABL.coordinateLaplacian i) f x =
    ∑ S with i ∈ S,
      FABL.fourierCoeff f S *
        FABL.monomial S x

theorem FABL.uniformInner_coordinateLaplacian_eq_influence
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) :
  FABL.uniformInner f
      ((FABL.coordinateLaplacian i) f) =
    FABL.influence f i

theorem FABL.uniformInner_coordinateLaplacian_self_eq_influence
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) :
  FABL.uniformInner
      ((FABL.coordinateLaplacian i) f)
      ((FABL.coordinateLaplacian i) f) =
    FABL.influence f i