English
Let f and g be integrable with respect to measures ν and μ, respectively, and L be a bilinear continuous linear map. Then the integral of their convolution equals applying L to the pair of integrals of f and g.
Русский
Пусть f и g интегрируемы по соответствующим мерам ν и μ, соответственно, и дано билинейное непрерывное отображение L. Тогда интеграл от их свёртки равен применению L к паре интегралов ∫ f и ∫ g.
LaTeX
$$$$\\int x\\,(f \\star_{L,\\nu} g)(x)\\,d\\mu(x) = L\\Big(\\int x\\,f(x)\\,d\\nu(x),\\ \\int x\\,g(x)\\,d\\mu(x)\\Big).$$$$
Lean4
theorem integral_convolution [MeasurableAdd₂ G] [MeasurableNeg G] [NormedSpace ℝ E] [NormedSpace ℝ E'] [CompleteSpace E]
[CompleteSpace E'] (hf : Integrable f ν) (hg : Integrable g μ) :
∫ x, (f ⋆[L, ν] g) x ∂μ = L (∫ x, f x ∂ν) (∫ x, g x ∂μ) :=
by
refine (integral_integral_swap (by apply hf.convolution_integrand L hg)).trans ?_
simp_rw [integral_comp_comm _ (hg.comp_sub_right _), integral_sub_right_eq_self]
exact (L.flip (∫ x, g x ∂μ)).integral_comp_comm hf
