convolution_eq_swap — Mathlib

English

The convolution is symmetric under swapping the two factors, up to appropriate flips of the bilinear map: convolution with g and f equals convolution with f and g under the flipped map.

Русский

Свёртка симметрична при перестановке множителей (с учетом переворота билинейного отображения).

LaTeX

$$$\operatorname{convolution}(g,f,L.flip,\mu) = \operatorname{convolution}(f,g,L,\mu).$$$

Lean4

/-- The symmetric definition of convolution. -/
theorem convolution_eq_swap : (f ⋆[L, μ] g) x = ∫ t, L (f (x - t)) (g t) ∂μ := by rw [← convolution_flip]; rfl

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