term_⋆[_,_]_ — Mathlib

English

If f =ae f' and g =ae g' with respect to μ, then convolution f g = convolution f' g' with the same L and μ.

Русский

Если f равно f' и g равно g' по мере a.e., то свёртки совпадают: f ⋆ g = f' ⋆ g' при той же μ и L.

LaTeX

$$$\\mathrm{convolution}(f,g,L,μ)=\\mathrm{convolution}(f',g',L,μ)$ при $f=f'\\text{ a.e.}$ и $g=g'\\text{ a.e.}$$$

Lean4

/-- The convolution of two functions with respect to a bilinear operation `L` and a measure `μ`. -/
@[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.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⋆[") (ParserDescr.cat✝ `term 67))
            (ParserDescr.symbol✝ ", "))
          (ParserDescr.cat✝ `term 67))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 66))

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