contDiff_convolution_left — Mathlib

English

Analogous to the right-parameter case, differentiability with respect to the left parameter holds, with derivative given by the left-parameter derivative convolved with f.

Русский

Аналогично правому случаю, дифференцируемость по левому параметру сохраняется, производная выражается через лево-параметрическую производную, свёрткующую f.

LaTeX

$$$$D_{p}((g_p⋆[L, μ] f)(x)) = (D_p g(p, \\cdot) ⋆[L, μ] f)(x).$$$$

Lean4

theorem _root_.HasCompactSupport.contDiff_convolution_left [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {n : ℕ∞}
    (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 n f) (hg : LocallyIntegrable g μ) : ContDiff 𝕜 n (f ⋆[L, μ] g) :=
  by
  rw [← convolution_flip]
  exact hcf.contDiff_convolution_right L.flip hg hf

Похожие утверждения