hasDerivAt_convolution_left — Mathlib

English

Analogous to the right-derivative case, the derivative of the left convolution with a differentiable left factor is the left derivative of f convolved with g.

Русский

Аналогично случаю с правой производной: производная левой конволюции с дифференцируемым левым множителем равна конволюте левой производной с g.

LaTeX

$$$$\\frac{d}{dx}(f \\star_{L,\\mu} g)(x_0) = (\\operatorname{deriv} f \\star_{L,\\mu} g)(x_0).$$$$

Lean4

theorem _root_.HasCompactSupport.hasDerivAt_convolution_left [IsNegInvariant μ] (hcf : HasCompactSupport f₀)
    (hf : ContDiff 𝕜 1 f₀) (hg : LocallyIntegrable g₀ μ) (x₀ : 𝕜) :
    HasDerivAt (f₀ ⋆[L, μ] g₀) ((deriv f₀ ⋆[L, μ] g₀) x₀) x₀ :=
  by
  simp +singlePass only [← convolution_flip]
  exact hcf.hasDerivAt_convolution_right L.flip hg hf x₀

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