English
The symmetric definition of convolution with the bilinear operator being scalar multiplication yields the standard formula (f ⋆ g)(x) = ∫ f(x−t) g(t) dt.
Русский
Симметричное определение свёртки с билинейным отображением в виде умножения даёт обычную формулу (f ⋆ g)(x) = ∫ f(x−t) g(t) dt.
LaTeX
$$$ (f ⋆ g)(x) = \int_G f(x-t) g(t) \, d\mu(t). $$$
Lean4
/-- The symmetric definition of convolution where the bilinear operator is multiplication. -/
theorem convolution_mul_swap [NormedSpace ℝ 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
(f ⋆[mul 𝕜 𝕜, μ] g) x = ∫ t, f (x - t) * g t ∂μ :=
convolution_eq_swap _