English
When the scalar multiplication is used as the bilinear operator, the convolution equals the integral of f(t) g(x − t) with the scalar multiplication.
Русский
При использовании скалярного умножения как билинейного оператора свёртка равна интегралу f(t) g(x − t) с умножением на скаляр.
LaTeX
$$$\\mathrm{convolution}(f,g,L,μ)=\\int f(t)\\, g(x-t)\\, dμ(t)$$$
Lean4
theorem convolution_smul [SMulCommClass ℝ 𝕜 F] {y : 𝕜} : f ⋆[L, μ] y • g = y • (f ⋆[L, μ] g) := by ext;
simp only [Pi.smul_apply, convolution_def, ← integral_smul, (L _).map_smul]