English
If f is locally integrable and g depends smoothly on a parameter, then the parametric convolution f ⋆ g is C^n in the parameter and space variable, with derivative given by the parameter-derivative convolution.
Русский
Если f локально интегрируема, а g гладко зависит от параметра, то параметрическая свёртка f⋆g гладкая (C^n) по параметру и по переменной, с производной, заданной через свёртку по производной по параметру.
LaTeX
$$$$\\text{contDiffOn}_𝕜 n (p,x) \\mapsto (f⋆[L, μ] g_p)(x)$$ имеет производную, равную $$(f⋆[L.precompR (P \\times G), μ] (D_p g(p, \\cdot)))(x)$$ при соответствующих условиях.$$
Lean4
/-- The convolution `g * f` 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`). -/
theorem contDiffOn_convolution_left_with_param [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E' →L[𝕜] E →L[𝕜] F)
{f : G → E} {n : ℕ∞} {g : P → G → E'} {s : Set P} {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 q : P × G => (g q.1 ⋆[L, μ] f) q.2) (s ×ˢ univ) := by
simpa only [convolution_flip] using contDiffOn_convolution_right_with_param L.flip hs hk hgs hf hg
