convolution_mul — Mathlib

English

Convolution is linear in the right input: convolution f g+g' equals convolution f g plus convolution f g'.

Русский

Свёртка линейна по правой части: f⋆(g+g') = f⋆g + f⋆g'.

LaTeX

$$$(f⋆[L,μ](g+g'))(x)=(f⋆[L,μ]g)(x)+(f⋆[L,μ]g')(x)$$$

Lean4

/-- The definition of convolution where the bilinear operator is multiplication. -/
theorem convolution_mul [Sub G] [NormedSpace ℝ 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
    (f ⋆[mul 𝕜 𝕜, μ] g) x = ∫ t, f t * g (x - t) ∂μ :=
  rfl

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