add_distrib — Mathlib

English

Distributivity of convolution over addition in the second input: convolution (f) (g+g') = convolution (f) g + convolution (f) g'.

Русский

Распределение свёртки по сложению второй переменной: f ⋆ (g+g') = f ⋆ g + f ⋆ g'.

LaTeX

$$$\\mathrm{convolution}(f,g+g',L,μ)=\\mathrm{convolution}(f,g,L,μ)+\\mathrm{convolution}(f,g',L,μ)$$$

Lean4

theorem add_distrib {x : G} (hfg : ConvolutionExistsAt f g x L μ) (hfg' : ConvolutionExistsAt f' g x L μ) :
    ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g) x + (f' ⋆[L, μ] g) x := by
  simp only [convolution_def, L.map_add₂, Pi.add_apply, integral_add hfg hfg']

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