theorem FABL.ProbabilityDensity.toPMF_apply
  {n : ℕ} (φ : FABL.ProbabilityDensity n)
  (x : FABL.F₂Cube n) :
  φ.toPMF x =
    ENNReal.ofReal
      (φ.toFun x /
        ↑(Fintype.card (FABL.F₂Cube n)))

theorem FABL.ProbabilityDensity.integral_toPMF_eq_expectation
  {n : ℕ} (φ : FABL.ProbabilityDensity n)
  (g : FABL.F₂Cube n → ℝ) :
  ∫ (x : FABL.F₂Cube n),
      g x ∂φ.toPMF.toMeasure =
    φ.expectation g

theorem FABL.densityExpectation_eq_uniformInner
  {n : ℕ} (φ : FABL.ProbabilityDensity n)
  (g : FABL.F₂Cube n → ℝ) :
  φ.expectation g =
    FABL.uniformInner φ.toFun g

theorem FABL.binaryFourierCoeff_subsetDensity_singleton_zero
  {n : ℕ} (S : Finset (Fin n)) :
  FABL.binaryFourierCoeff
      (FABL.subsetDensity {0} ⋯).toFun S =
    1

theorem FABL.subsetDensity_singleton_zero_eq_sum_χ
  {n : ℕ} (x : FABL.F₂Cube n) :
  (FABL.subsetDensity {0} ⋯).toFun x =
    ∑ S, (FABL.χ S) x

theorem FABL.convolution_apply {n : ℕ}
  (f g : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  FABL.convolution f g x =
    Finset.univ.expect fun y =>
      f y * g (x - y)

theorem FABL.convolution_apply_add {n : ℕ}
  (f g : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  FABL.convolution f g x =
    Finset.univ.expect fun y =>
      f y * g (x + y)

theorem FABL.convolution_apply_swap {n : ℕ}
  (f g : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  FABL.convolution f g x =
    Finset.univ.expect fun y =>
      f (x - y) * g y

theorem FABL.convolution_apply_swap_add {n : ℕ}
  (f g : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  FABL.convolution f g x =
    Finset.univ.expect fun y =>
      f (x + y) * g y

theorem FABL.convolution_comm {n : ℕ}
  (f g : FABL.F₂Cube n → ℝ) :
  FABL.convolution f g =
    FABL.convolution g f

theorem FABL.convolution_assoc {n : ℕ}
  (f g h : FABL.F₂Cube n → ℝ) :
  FABL.convolution (FABL.convolution f g)
      h =
    FABL.convolution f
      (FABL.convolution g h)

theorem FABL.density_convolution_apply {n : ℕ}
  (φ : FABL.ProbabilityDensity n)
  (g : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  (FABL.convolution φ.toFun g x =
      φ.expectation fun y => g (x - y)) ∧
    FABL.convolution φ.toFun g x =
      φ.expectation fun y => g (x + y)

theorem FABL.densityExpectation_eq_convolution_apply_zero
  {n : ℕ} (φ : FABL.ProbabilityDensity n)
  (g : FABL.F₂Cube n → ℝ) :
  φ.expectation g =
    FABL.convolution φ.toFun g 0

theorem FABL.ProbabilityDensity.toPMF_convolution
  {n : ℕ}
  (φ ψ : FABL.ProbabilityDensity n) :
  (φ.toPMF.bind fun y =>
      PMF.map (fun z => y + z) ψ.toPMF) =
    (φ.convolution ψ).toPMF

theorem FABL.convolution_probability_eq_add
  {n : ℕ}
  (φ ψ : FABL.ProbabilityDensity n)
  (A : Set (FABL.F₂Cube n)) :
  (φ.convolution ψ).probability A =
    Finset.univ.expect fun y =>
      Finset.univ.expect fun z =>
        φ.toFun y * ψ.toFun z *
          FABL.setIndicator A (y + z)

theorem FABL.binaryFourierCoeff_convolution
  {n : ℕ} (f g : FABL.F₂Cube n → ℝ)
  (S : Finset (Fin n)) :
  FABL.binaryFourierCoeff
      (FABL.convolution f g) S =
    FABL.binaryFourierCoeff f S *
      FABL.binaryFourierCoeff g S