convolution_smul — Mathlib

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]

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