integrable_convolution — Mathlib

English

If the convolution exists for f and g and for f and g', then the encoded integrability conditions imply the same convolution result with g' in place of g.

Русский

Если существует свёртка для (f,g) и (f,g'), то условия интегрируемости приводят к тем же результатам свёртки с g' вместо g.

LaTeX

$$$\\mathrm{ConvolutionExists}(f,g,L,μ)\\Rightarrow \\mathrm{ConvolutionExists}(f,g',L,μ)\\Rightarrow \\mathrm{convolution}(f,g,L,μ)=\\mathrm{convolution}(f,g',L,μ)$$$

Lean4

theorem integrable_convolution (hf : Integrable f μ) (hg : Integrable g μ) : Integrable (f ⋆[L, μ] g) μ :=
  (hf.convolution_integrand L hg).integral_prod_left

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