English
The right-parametric convolution is differentiable with respect to the parameter; the derivative is given by convolving f with the derivative of g in the parameter variable.
Русский
Правая параметрическая свёртка дифференцируема по параметру; производная выражается свёрткой f с производной g по параметру.
LaTeX
$$$$D_p\\big((f⋆[L, μ] g_p)(x)\\big) = (f⋆[L.precompR (P \\times G), μ] (D_p g(p, ·)))(x).$$$$
Lean4
/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` 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 composition with an additional `C^n` function. -/
theorem contDiffOn_convolution_right_with_param_comp {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {s : Set P} {v : P → G}
(hv : ContDiffOn 𝕜 n v s) {f : G → E} {g : P → G → E'} {k : Set G} (hs : IsOpen s) (hk : IsCompact k)
(hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0) (hf : LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n ↿g (s ×ˢ univ)) :
ContDiffOn 𝕜 n (fun x => (f ⋆[L, μ] g x) (v x)) s :=
by
apply (contDiffOn_convolution_right_with_param L hs hk hgs hf hg).comp (contDiffOn_id.prodMk hv)
intro x hx
simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]
