noncomputable def BooleanFourier.booleanExpectation {n : ℕ} (f : (Fin n → Bool) → ℝ) (g : ℝ → ℝ) : ℝ

noncomputable def BooleanFourier.gaussianExpectation {n : ℕ} (f : (Fin n → Bool) → ℝ) (g : ℝ → ℝ) : ℝ

structure BooleanFourier.IsC3Bounded (Ψ : ℝ → ℝ) : Type

• differentiable : ContDiff ℝ 3 Ψ
• thirdDerivBound : ℝ
• thirdDerivBound_nonneg : 0 ≤ self.thirdDerivBound
• bound (x : ℝ) : |iteratedDeriv 3 Ψ x| ≤ self.thirdDerivBound