English
In the left-parameter setting, the differentiability of g⋆f with parameter s is ensured by reducing to the right-parametric case via universe alignment.
Русский
В левой постановке параметра гладкость g⋆f достигается за счёт редукции к правому параметрическому случаю путём согласования вселенных.
LaTeX
$$$$\\text{contDiffOn}_𝕜 n (p,x) \\mapsto (g_p⋆[L, μ] f)(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`),
given in terms of composition with additional `C^n` functions. -/
theorem contDiffOn_convolution_left_with_param_comp [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E' →L[𝕜] E →L[𝕜] F)
{s : Set P} {n : ℕ∞} {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 => (g x ⋆[L, μ] f) (v x)) s :=
by
apply (contDiffOn_convolution_left_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]
