support_convolution_subset — Mathlib

English

The convolution with scalar multiplication is given by (f ⋆ [lsmul 𝕜 𝕜, μ] g)(x) = ∫ f(x−t) (g t) dμ.

Русский

Свёртка, где билинейный оператор равен скалярному умножению, задаётся выражением (f ⋆ [lsmul 𝕜 𝕜, μ] g)(x) = ∫ f(x−t) (g(t)) dμ.

LaTeX

$$$(f ⋆[lsmul 𝕜 𝕜, μ] g)(x) = \int_G f(x-t) \cdot g(t) \, d\mu(t).$$$

Lean4

theorem support_convolution_subset : support (f ⋆[L, μ] g) ⊆ support f + support g :=
  (support_convolution_subset_swap L).trans (add_comm _ _).subset

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