theorem FABL.productProbabilityPMF_apply.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  (n : ℕ) (x : Fin n → Ω) :
  (FABL.productProbabilityPMF π n) x =
    ∏ i, π (x i)

theorem FABL.productProbabilityPMF_hasFullSupport.{u_1}
  {Ω : Type u_1} [Fintype Ω] {π : PMF Ω}
  (hπ : FABL.PMFHasFullSupport π)
  (n : ℕ) :
  FABL.PMFHasFullSupport
    (FABL.productProbabilityPMF π n)

theorem FABL.indicatorBasis_apply.{u_1}
  {Ω : Type u_1} [Finite Ω]
  [DecidableEq Ω] (x y : Ω) :
  (FABL.indicatorBasis Ω) x y =
    if y = x then 1 else 0

theorem FABL.finrank_real_fun_eq_card.{u_1}
  (Ω : Type u_1) [Fintype Ω] :
  Module.finrank ℝ (Ω → ℝ) =
    Fintype.card Ω

theorem FABL.FiniteFourierBasis.pmfInner_basis.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  (a b : ι) :
  FABL.pmfInner π (B.basis a)
      (B.basis b) =
    if a = b then 1 else 0

theorem FABL.signSiteFourierBasis_productFunction_eq_monomial
  {n : ℕ} (a : FABL.MultiIndex n (Fin 2))
  (x : FABL.SignCube n) :
  FABL.signSiteFourierBasis.productFunction
      a x =
    FABL.monomial
      (FABL.signMultiIndexSupport a) x

theorem FABL.signSiteFourierBasis_productBasis_eq_monomial
  {n : ℕ}
  (a : FABL.MultiIndex n (Fin 2)) :
  (FABL.signSiteFourierBasis.productBasis
        n)
      a =
    FABL.monomial
      (FABL.signMultiIndexSupport a)

theorem FABL.signSiteFourierBasis_fourierCoeff_eq_fourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (a : FABL.MultiIndex n (Fin 2)) :
  FABL.signSiteFourierBasis.fourierCoeff f
      a =
    FABL.fourierCoeff f
      (FABL.signMultiIndexSupport a)

theorem FABL.inner_pmfSqrtScaleLinearEquiv.{u_1}
  {Ω : Type u_1} [Fintype Ω] {π : PMF Ω}
  (hπ : FABL.PMFHasFullSupport π)
  (f g : Ω → ℝ) :
  inner ℝ
      ((FABL.pmfSqrtScaleLinearEquiv hπ)
        f)
      ((FABL.pmfSqrtScaleLinearEquiv hπ)
        g) =
    FABL.pmfInner π f g

theorem FABL.exists_finiteFourierBasis.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  [DecidableEq Ω] {π : PMF Ω}
  (hπ : FABL.PMFHasFullSupport π) :
  Nonempty (FABL.FiniteFourierBasis Ω π Ω)

theorem FABL.FiniteFourierBasis.productFunction_orthonormal.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (a b : FABL.MultiIndex n ι) :
  (FABL.pmfExpectation
      (FABL.productProbabilityPMF π n)
      fun x =>
      B.productFunction a x *
        B.productFunction b x) =
    if a = b then 1 else 0

theorem FABL.FiniteFourierBasis.productFunction_linearIndependent.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  (n : ℕ) :
  LinearIndependent ℝ B.productFunction

theorem FABL.FiniteFourierBasis.productBasis_apply.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  (n : ℕ) (a : FABL.MultiIndex n ι) :
  (B.productBasis n) a =
    B.productFunction a

theorem FABL.FiniteFourierBasis.fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (x : Fin n → Ω) :
  f x =
    ∑ a,
      B.fourierCoeff f a *
        B.productFunction a x

theorem FABL.FiniteFourierBasis.fourier_expansion_unique.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (c : FABL.MultiIndex n ι → ℝ)
  (hc :
    ∀ (x : Fin n → Ω),
      f x =
        ∑ a,
          c a * B.productFunction a x) :
  c = B.fourierCoeff f

theorem FABL.threePointBothCIndicator_fourier_expansion
  (x : Fin 2 → FABL.ThreePoint) :
  FABL.threePointBothCIndicator x =
    ∑ a,
      FABL.threePointCIndicatorCoeff
            (a 0) *
          FABL.threePointCIndicatorCoeff
            (a 1) *
        FABL.threePointFourierBasis.productFunction
          a x