convolution_mul_swap — Mathlib

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 _

Похожие утверждения