convolution_lsmul_swap — Mathlib

English

A formula expressing how the convolution with a bilinear operator interacts with a precomposition: (f ⋆[L, μ] g) at (x0, x) equals (f ⋆[L, μ] g_x) at x0, where g_x is the function a ↦ g(a)(x).

Русский

Формула взаимодействия свёртки с пред/composition: (f ⋆[L, μ] g) при аргументах (x0, x) равна (f ⋆[L, μ] (a ↦ g(a)(x))) при x0.

LaTeX

$$$(f ⋆[L, μ] g)_{x_0}(x) = (f ⋆[L, μ] (a \mapsto g(a)(x))) (x_0).$$$

Lean4

/-- The symmetric definition of convolution where the bilinear operator is scalar multiplication. -/
theorem convolution_lsmul_swap {f : G → 𝕜} {g : G → F} : (f ⋆[lsmul 𝕜 𝕜, μ] g : G → F) x = ∫ t, f (x - t) • g t ∂μ :=
  convolution_eq_swap _

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