theorem FABL.fourierCoeff_eq_uniformInner {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff f S =
    FABL.uniformInner f (FABL.monomial S)

theorem FABL.parseval {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformInner f f =
    ∑ S, FABL.fourierCoeff f S ^ 2

theorem FABL.sum_sq_fourierCoeff_eq_one {n : ℕ}
  (f : FABL.BooleanFunction n) :
  ∑ S, FABL.fourierCoeff f.toReal S ^ 2 =
    1

theorem FABL.plancherel {n : ℕ}
  (f g : FABL.SignCube n → ℝ) :
  FABL.uniformInner f g =
    ∑ S,
      FABL.fourierCoeff f S *
        FABL.fourierCoeff g S

theorem FABL.uniformInner_eq_uniformProbability_eq_sub_ne
  {n : ℕ} (f g : FABL.BooleanFunction n) :
  FABL.uniformInner f.toReal g.toReal =
    (FABL.uniformProbability fun x =>
        f x = g x) -
      FABL.uniformProbability fun x =>
        f x ≠ g x

theorem FABL.uniformInner_eq_one_sub_two_mul_relativeHammingDist
  {n : ℕ} (f g : FABL.BooleanFunction n) :
  FABL.uniformInner f.toReal g.toReal =
    1 - 2 * FABL.relativeHammingDist f g

theorem FABL.mean_eq_probability_one_sub_probability_neg_one
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.mean f.toReal =
    (FABL.uniformProbability fun x =>
        f x = 1) -
      FABL.uniformProbability fun x =>
        f x = -1

theorem FABL.isBalanced_iff_uniformProbability_one_eq_half
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.IsBalanced f.toReal ↔
    (FABL.uniformProbability fun x =>
        f x = 1) =
      2⁻¹

theorem FABL.mean_eq_fourierCoeff_empty {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.mean f = FABL.fourierCoeff f ∅

theorem FABL.isBalanced_iff_fourierCoeff_empty_eq_zero
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.IsBalanced f ↔
    FABL.fourierCoeff f ∅ = 0

theorem FABL.variance_eq_uniformInner_centered
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f =
    FABL.uniformInner
      (fun x => f x - FABL.mean f)
      fun x => f x - FABL.mean f

theorem FABL.variance_eq_sum_sq_fourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f =
      (Finset.univ.expect fun x =>
          f x ^ 2) -
        FABL.mean f ^ 2 ∧
    FABL.variance f =
      ∑ S with S ≠ ∅,
        FABL.fourierCoeff f S ^ 2

theorem FABL.variance_eq_four_mul_probabilities
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.variance f.toReal =
      1 - FABL.mean f.toReal ^ 2 ∧
    (FABL.variance f.toReal =
        (4 *
            FABL.uniformProbability
              fun x => f x = 1) *
          FABL.uniformProbability fun x =>
            f x = -1) ∧
      FABL.variance f.toReal ∈ Set.Icc 0 1

theorem FABL.relativeHammingDist_one_eq_uniformProbability_neg_one
  {n : ℕ} (f : FABL.BooleanFunction n) :
  (FABL.relativeHammingDist f fun x =>
      1) =
    FABL.uniformProbability fun x =>
      f x = -1

theorem FABL.relativeHammingDist_neg_one_eq_uniformProbability_one
  {n : ℕ} (f : FABL.BooleanFunction n) :
  (FABL.relativeHammingDist f fun x =>
      -1) =
    FABL.uniformProbability fun x =>
      f x = 1

theorem FABL.variance_eq_four_mul_relativeHammingDist_one_mul_neg_one
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.variance f.toReal =
    (4 *
        FABL.relativeHammingDist f
          fun x => 1) *
      FABL.relativeHammingDist f fun x =>
        -1

theorem FABL.variance_bounds_distanceToNearestConstant
  {n : ℕ} (f : FABL.BooleanFunction n) :
  2 * FABL.distanceToNearestConstant f ≤
      FABL.variance f.toReal ∧
    FABL.variance f.toReal ≤
      4 * FABL.distanceToNearestConstant f

theorem FABL.covariance_eq_uniformInner_centered
  {n : ℕ} (f g : FABL.SignCube n → ℝ) :
  FABL.covariance f g =
    FABL.uniformInner
      (fun x => f x - FABL.mean f)
      fun x => g x - FABL.mean g

theorem FABL.covariance_eq_sum_fourierCoeff_mul
  {n : ℕ} (f g : FABL.SignCube n → ℝ) :
  FABL.covariance f g =
      (Finset.univ.expect fun x =>
          f x * g x) -
        FABL.mean f * FABL.mean g ∧
    FABL.covariance f g =
      ∑ S with S ≠ ∅,
        FABL.fourierCoeff f S *
          FABL.fourierCoeff g S

theorem FABL.spectralSample_apply_toReal {n : ℕ}
  (f : FABL.BooleanFunction n)
  (S : Finset (Fin n)) :
  ((FABL.spectralSample f) S).toReal =
    FABL.fourierWeight f.toReal S

theorem FABL.fourierWeightAtLevel_eq_uniformLpNorm_degreePart_sq
  {n : ℕ} (k : ℕ)
  (f : FABL.SignCube n → ℝ) :
  FABL.fourierWeightAtLevel k f =
    FABL.uniformLpNorm 2
        (FABL.degreePart k f) ^
      2

theorem FABL.spectralSample_card_eq {n : ℕ}
  (f : FABL.BooleanFunction n) (k : ℕ) :
  ∑ S with S.card = k,
      ((FABL.spectralSample f) S).toReal =
    FABL.fourierWeightAtLevel k f.toReal