theorem FABL.pmfInner_symm.{u_1} {Ω : Type u_1}
  [Fintype Ω] (π : PMF Ω) (f g : Ω → ℝ) :
  FABL.pmfInner π f g =
    FABL.pmfInner π g f

theorem FABL.pmfInner_add_left.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  (f g h : Ω → ℝ) :
  FABL.pmfInner π (f + g) h =
    FABL.pmfInner π f h +
      FABL.pmfInner π g h

theorem FABL.pmfInner_smul_left.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  (c : ℝ) (f g : Ω → ℝ) :
  FABL.pmfInner π (c • f) g =
    c * FABL.pmfInner π f g

theorem FABL.pmfInner_self_nonneg.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  (f : Ω → ℝ) : 0 ≤ FABL.pmfInner π f f

theorem FABL.pmfInner_self_eq_zero_iff.{u_1}
  {Ω : Type u_1} [Fintype Ω] {π : PMF Ω}
  (hπ : FABL.PMFHasFullSupport π)
  (f : Ω → ℝ) :
  FABL.pmfInner π f f = 0 ↔ f = 0

theorem FABL.FiniteFourierBasis.fourierCoeff_eq_pmfInner.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff f a =
    FABL.pmfInner
      (FABL.productProbabilityPMF π n) f
      (B.productFunction a)

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

theorem FABL.threePointFourierFunction_orthonormal
  (a b : Fin 3) :
  (FABL.pmfExpectation
      (FABL.uniformPMF FABL.ThreePoint)
      fun x =>
      FABL.threePointFourierFunction a x *
        FABL.threePointFourierFunction b
          x) =
    if a = b then 1 else 0

theorem FABL.threePointCIndicator_coefficient
  (j : Fin 3) :
  (FABL.pmfExpectation
      (FABL.uniformPMF FABL.ThreePoint)
      fun x =>
      FABL.threePointCIndicator x *
        FABL.threePointBasis j x) =
    FABL.threePointCIndicatorCoeff j

theorem FABL.threePointBothCIndicator_fourierCoeff
  (a : FABL.MultiIndex 2 (Fin 3)) :
  FABL.threePointFourierBasis.fourierCoeff
      FABL.threePointBothCIndicator a =
    ∏ i,
      FABL.threePointCIndicatorCoeff (a i)

theorem FABL.threePointBothCIndicator_fourierCoeff_table :
  FABL.threePointFourierBasis.fourierCoeff
      FABL.threePointBothCIndicator =
    fun a =>
    FABL.threePointCIndicatorCoeff (a 0) *
      FABL.threePointCIndicatorCoeff (a 1)

theorem FABL.FiniteFourierBasis.fourierCoeff_centered.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff
      (fun x =>
        f x - FABL.productMean π f)
      a =
    if a = B.zeroMultiIndex n then 0
    else B.fourierCoeff f a

theorem FABL.FiniteFourierBasis.fourierCoeff_const.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (c : ℝ)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff (fun x => c) a =
    if a = B.zeroMultiIndex n then c
    else 0

theorem FABL.FiniteFourierBasis.fourierCoeff_injective.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} :
  Function.Injective B.fourierCoeff

theorem FABL.projectOnCoordinates_add.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (J : Finset (Fin n))
  (f g : FABL.ProductL2 Ω n) :
  FABL.projectOnCoordinates π J (f + g) =
    FABL.projectOnCoordinates π J f +
      FABL.projectOnCoordinates π J g

theorem FABL.projectOnCoordinates_smul.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (J : Finset (Fin n)) (c : ℝ)
  (f : FABL.ProductL2 Ω n) :
  FABL.projectOnCoordinates π J (c • f) =
    c • FABL.projectOnCoordinates π J f

theorem FABL.projectOnCoordinates_sum.{u_1, u_2}
  {Ω : Type u_1} {κ : Type u_2}
  [Fintype Ω] [Fintype κ] (π : PMF Ω)
  {n : ℕ} (J : Finset (Fin n))
  (f : κ → FABL.ProductL2 Ω n) :
  FABL.projectOnCoordinates π J
      (∑ k, f k) =
    ∑ k,
      FABL.projectOnCoordinates π J (f k)

theorem FABL.productNoiseOperator_add.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.ProductL2 Ω n) :
  FABL.productNoiseOperator π ρ hρ
      (f + g) =
    FABL.productNoiseOperator π ρ hρ f +
      FABL.productNoiseOperator π ρ hρ g

theorem FABL.productNoiseOperator_smul.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (c : ℝ) (f : FABL.ProductL2 Ω n) :
  FABL.productNoiseOperator π ρ hρ
      (c • f) =
    c • FABL.productNoiseOperator π ρ hρ f

theorem FABL.productNoiseOperator_selfAdjoint.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.ProductL2 Ω n) :
  FABL.productInner π n f
      (FABL.productNoiseOperator π ρ hρ
        g) =
    FABL.productInner π n
      (FABL.productNoiseOperator π ρ hρ f)
      g

theorem FABL.coordinateProjection_add_laplacian.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n) :
  FABL.coordinateProjection π i f +
      FABL.productCoordinateLaplacian π i
        f =
    f

theorem FABL.FiniteFourierBasis.productInner_eq_projection_add_laplacian.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (i : Fin n)
  (f g : FABL.ProductL2 Ω n) :
  FABL.productInner π n f g =
    FABL.productInner π n
        (FABL.coordinateProjection π i f)
        (FABL.coordinateProjection π i
          g) +
      FABL.productInner π n
        (FABL.productCoordinateLaplacian π
          i f)
        (FABL.productCoordinateLaplacian π
          i g)

theorem FABL.coordinateProjection_apply.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n)
  (x : Fin n → Ω) :
  FABL.coordinateProjection π i f x =
    FABL.pmfExpectation π fun ω =>
      f (FABL.replaceCoordinate x i ω)

theorem FABL.coordinateProjection_replaceCoordinate.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n) (x : Fin n → Ω)
  (ω : Ω) :
  FABL.coordinateProjection π i f
      (FABL.replaceCoordinate x i ω) =
    FABL.coordinateProjection π i f x

theorem FABL.coordinateConditionalVariance_eq_coordinateProjection_sq_laplacian.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) (x : Fin n → Ω) :
  FABL.coordinateConditionalVariance π f i
      x =
    FABL.coordinateProjection π i
      (fun z =>
        FABL.productCoordinateLaplacian π
            i f z ^
          2)
      x

theorem FABL.coordinateProjection_abs_laplacian_eq_coordinateConditionalVariance.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hf : FABL.HasSignRange f) (i : Fin n) :
  (FABL.coordinateProjection π i fun x =>
      |FABL.productCoordinateLaplacian π i
          f x|) =
    FABL.coordinateConditionalVariance π f
      i

theorem FABL.coordinateProjection_resamplingDisagreement_eq_half_variance.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hf : FABL.HasSignRange f) (i : Fin n) :
  (FABL.coordinateProjection π i fun x =>
      FABL.pmfExpectation π fun ω =>
        if
            f x ≠
              f
                (FABL.replaceCoordinate x
                  i ω) then
          1
        else 0) =
    fun x =>
    1 / 2 *
      FABL.coordinateConditionalVariance π
        f i x

theorem FABL.FiniteFourierBasis.productMean_abs_laplacian_rpow_eq_conditional.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (p : ℝ) (f : FABL.ProductL2 Ω n)
  (i : Fin n) :
  (FABL.productMean π fun x =>
      |FABL.productCoordinateLaplacian π i
            f x| ^
        p) =
    FABL.productMean π
      (FABL.coordinateConditionalAbsMoment
        π p f i)

theorem FABL.FiniteFourierBasis.productMean_abs_laplacian_rpow_le_two_rpow_influence.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} {f : FABL.ProductL2 Ω n}
  (hf : FABL.HasSignRange f) (i : Fin n)
  (p : ℝ) (hp : 1 ≤ p) :
  (FABL.productMean π fun x =>
      |FABL.productCoordinateLaplacian π i
            f x| ^
        p) ≤
    2 ^ p * FABL.productInfluence π f i

theorem FABL.FiniteFourierBasis.productMean_abs_laplacian_rpow_le_influence.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} {f : FABL.ProductL2 Ω n}
  (hf : FABL.HasSignRange f) (i : Fin n)
  (p : ℝ) (hp1 : 1 ≤ p) (hp2 : p ≤ 2) :
  (FABL.productMean π fun x =>
      |FABL.productCoordinateLaplacian π i
            f x| ^
        p) ≤
    FABL.productInfluence π f i