add_distrib — Mathlib

English

The lsmul construction defines the convolution when the bilinear operator is scalar multiplication; the formula is (f ⋆[lsmul L] g)(x) = ∫ f(t) (L⋅g)(x−t) dt.

Русский

Определение свёртки через lsmul: (f ⋆[lsmul] g)(x) = ∫ f(t) (L⋅g)(x−t) dt.

LaTeX

$$$\\mathrm{convolution}_{lsmul}(f,g,L,μ)(x)=\\int t\\, f(t)\\, (g(x-t))\\, dt$$$

Lean4

theorem add_distrib (hfg : ConvolutionExists f g L μ) (hfg' : ConvolutionExists f' g L μ) :
    (f + f') ⋆[L, μ] g = f ⋆[L, μ] g + f' ⋆[L, μ] g := by
  ext x
  exact (hfg x).add_distrib (hfg' x)

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