English
Convolution is linear in its left input: convolution (f+f') with g equals convolution f with g plus convolution f' with g.
Русский
Свёртка линейна по левой входной функции: (f+f')⋆g = f⋆g + f'⋆g.
LaTeX
$$$(f+f')⋆[L,μ]g = (f⋆[L,μ]g) + (f'⋆[L,μ]g)$$$
Lean4
/-- The convolution of two functions with respect to a bilinear operation `L` and the volume. -/
@[scoped term_parser 1000]
public meta def «term_⋆[_]_» : Lean.TrailingParserDescr✝ :=
ParserDescr.trailingNode✝ `Convolution.«term_⋆[_]_» 67 0
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⋆[") (ParserDescr.cat✝ `term 67))
(ParserDescr.symbol✝ "]"))
(ParserDescr.cat✝ `term 66))
