English
Parametric convolution differentiability reduces to the standard case by universe-sharing, preserving the derivative structure.
Русский
Дифференцируемость параметрической свёртки приводится к стандартному случаю через универсуальное объединение, сохраняющее структуру производной.
LaTeX
$$$$\\text{contDiffOn}_𝕜 n (f⋆[L, μ] g) = \\text{...}$$$$
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`). -/
theorem contDiffOn_convolution_right_with_param {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {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 => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) := by
/- The result is known when all the universes are the same, from
`contDiffOn_convolution_right_with_param_aux`. We reduce to this situation by pushing
everything through `ULift` continuous linear equivalences. -/
let eG : Type max uG uE' uF uP := ULift.{max uE' uF uP} G
borelize eG
let eE' : Type max uE' uG uF uP := ULift.{max uG uF uP} E'
let eF : Type max uF uG uE' uP := ULift.{max uG uE' uP} F
let eP : Type max uP uG uE' uF := ULift.{max uG uE' uF} P
let isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
let isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
let isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
let isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
let ef := f ∘ isoG
let eμ : Measure eG := Measure.map isoG.symm μ
let eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))
let eL :=
ContinuousLinearMap.comp ((ContinuousLinearEquiv.arrowCongr isoE' isoF).symm : (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF) L
let R := fun q : eP × eG => (ef ⋆[eL, eμ] eg q.1) q.2
have R_contdiff : ContDiffOn 𝕜 n R ((isoP ⁻¹' s) ×ˢ univ) :=
by
have hek : IsCompact (isoG ⁻¹' k) := isoG.toHomeomorph.isClosedEmbedding.isCompact_preimage hk
have hes : IsOpen (isoP ⁻¹' s) := isoP.continuous.isOpen_preimage _ hs
refine contDiffOn_convolution_right_with_param_aux eL hes hek ?_ ?_ ?_
· intro p x hp hx
simp only [eg, ContinuousLinearEquiv.map_eq_zero_iff]
exact hgs _ _ hp hx
· exact (locallyIntegrable_map_homeomorph isoG.symm.toHomeomorph).2 hf
· apply isoE'.symm.contDiff.comp_contDiffOn
apply hg.comp (isoP.prodCongr isoG).contDiff.contDiffOn
rintro ⟨p, x⟩ ⟨hp, -⟩
simpa only [mem_preimage, ContinuousLinearEquiv.prodCongr_apply, prodMk_mem_set_prod_eq, mem_univ, and_true] using
hp
have A : ContDiffOn 𝕜 n (isoF ∘ R ∘ (isoP.prodCongr isoG).symm) (s ×ˢ univ) :=
by
apply isoF.contDiff.comp_contDiffOn
apply R_contdiff.comp (ContinuousLinearEquiv.contDiff _).contDiffOn
rintro ⟨p, x⟩ ⟨hp, -⟩
simpa only [mem_preimage, mem_prod, mem_univ, and_true, ContinuousLinearEquiv.prodCongr_symm,
ContinuousLinearEquiv.prodCongr_apply, ContinuousLinearEquiv.apply_symm_apply] using hp
have : isoF ∘ R ∘ (isoP.prodCongr isoG).symm = fun q : P × G => (f ⋆[L, μ] g q.1) q.2 :=
by
apply funext
rintro ⟨p, x⟩
simp only [(· ∘ ·), ContinuousLinearEquiv.prodCongr_symm, ContinuousLinearEquiv.prodCongr_apply]
simp only [R, convolution]
rw [IsClosedEmbedding.integral_map, ← isoF.integral_comp_comm]
· rfl
· exact isoG.symm.toHomeomorph.isClosedEmbedding
simp_rw [this] at A
exact A
