noncomputable def HeatFundamental.convolution {n : ℕ} (f g : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

The convolution of two functions $f, g : \mathbb{R}^n \to \mathbb{R}$ (Definition 1.1.1): $(f * g)(x) = \int_{\mathbb{R}^n} f(y)\, g(x - y)\, d^n y$.