English
If two functions f and g on a topological group G have compact support, then their convolution f ⋆ g also has compact support. Moreover, the support of f ⋆ g is contained in the sum of the supports of f and g: Supp(f ⋆ g) ⊆ Supp(f) + Supp(g).
Русский
Если две функции f и g на топологической группе G имеют компактную опору, то их свёртка f ⋆ g тоже имеет компактную опору. Кроме того, опора f ⋆ g вложена в сумму опор f и g: Supp(f ⋆ g) ⊆ Supp(f) + Supp(g).
LaTeX
$$$\operatorname{Supp}(f) \text{ и } \operatorname{Supp}(g) \text{ компактны} \;\Rightarrow\; \operatorname{Supp}(f \star g) \text{ компактно и } \operatorname{Supp}(f \star g) \subseteq \operatorname{Supp}(f) + \operatorname{Supp}(g).$$$
Lean4
protected theorem _root_.HasCompactSupport.convolution [T2Space G] (hcf : HasCompactSupport f)
(hcg : HasCompactSupport g) : HasCompactSupport (f ⋆[L, μ] g) :=
(hcg.isCompact.add hcf).of_isClosed_subset isClosed_closure <|
closure_minimal ((support_convolution_subset_swap L).trans <| add_subset_add subset_closure subset_closure)
(hcg.isCompact.add hcf).isClosed
