English
If g has compact support and f is locally integrable, and g is continuous, then the convolution f ⋆ g is a continuous function on G.
Русский
Если g имеет компактную опору и непрерывна, а f локально интегрируема, то свёртка f ⋆ g является непрерывной функцией на G.
LaTeX
$$$\operatorname{Continuous}(f ⋆ g).$$$
Lean4
/-- The convolution is continuous if one function is locally integrable and the other has compact
support and is continuous. -/
theorem _root_.HasCompactSupport.continuous_convolution_right (hcg : HasCompactSupport g) (hf : LocallyIntegrable f μ)
(hg : Continuous g) : Continuous (f ⋆[L, μ] g) :=
by
rw [← continuousOn_univ]
let g' : G → G → E' := fun _ q => g q
have : ContinuousOn ↿g' (univ ×ˢ univ) := (hg.comp continuous_snd).continuousOn
exact
continuousOn_convolution_right_with_param_comp L (continuousOn_univ.2 continuous_id) hcg
(fun p x _ hx => image_eq_zero_of_notMem_tsupport hx) hf this
