zero_convolution — Mathlib

English

The convolution with flipped arguments is naturally related to the original convolution via flipping L.

Русский

Свёртка со свернутыми аргументами естественно связана с исходной через разворот L.

LaTeX

$$$\\mathrm{convolution\\_flip}(g,f,x,L,μ)\\;\\iff\\; \\mathrm{convolution}(f,g,x,L,μ)$$$

Lean4

@[simp]
theorem zero_convolution : 0 ⋆[L, μ] g = 0 := by
  ext
  simp_rw [convolution_def, Pi.zero_apply, L.map_zero₂, integral_zero]

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