English
Suppose f is locally integrable and g is parameterized by p ∈ P with a compact parameter domain k and compatibility hypotheses as in the previous lemma. If g is continuous on s × univ, then the function x ↦ (f ⋆ g)(x) depends continuously on p for p ∈ s, i.e., the map (p, x) ↦ (f ⋆ g_p)(x) is continuous on s × univ.
Русский
Пусть f локально интегрируема, а g зависит от параметра p ∈ P и удовлетворяет условиям предыдущего леммы; если g непрерывна на s × univ, то отображение (p, x) ↦ (f ⋆ g_p)(x) непрерывно на s × univ.
LaTeX
$$$\text{ContinuousOn}( (p,x) \mapsto (f ⋆[L, μ] g p) x )\; (s \times univ).$$$
Lean4
/-- The convolution `f * g` is continuous if `f` is locally integrable and `g` is continuous and
compactly supported. Version where `g` depends on an additional parameter in an open subset `s` of
a parameter space `P` (and the compact support `k` is independent of the parameter in `s`),
given in terms of compositions with an additional continuous map. -/
theorem continuousOn_convolution_right_with_param_comp {s : Set P} {v : P → G} (hv : ContinuousOn v s) {g : P → G → E'}
{k : Set G} (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0) (hf : LocallyIntegrable f μ)
(hg : ContinuousOn ↿g (s ×ˢ univ)) : ContinuousOn (fun x => (f ⋆[L, μ] g x) (v x)) s :=
by
apply (continuousOn_convolution_right_with_param L hk hgs hf hg).comp (continuousOn_id.prodMk hv)
intro x hx
simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]
