hasDerivAt_convolution_right — Mathlib

English

If f is locally integrable and g has compact support and is C^1, then the derivative of f ⋆ g at x0 equals f ⋆ (deriv g) at x0.

Русский

Если f локально интегрируем, а g имеет компактную опору и является C^1, то производная f ⋆ g в точке x0 равна f ⋆ (deriv g) в x0.

LaTeX

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

Lean4

theorem _root_.HasCompactSupport.hasDerivAt_convolution_right (hf : LocallyIntegrable f₀ μ) (hcg : HasCompactSupport g₀)
    (hg : ContDiff 𝕜 1 g₀) (x₀ : 𝕜) : HasDerivAt (f₀ ⋆[L, μ] g₀) ((f₀ ⋆[L, μ] deriv g₀) x₀) x₀ :=
  by
  convert (hcg.hasFDerivAt_convolution_right L hf hg x₀).hasDerivAt using 1
  rw [convolution_precompR_apply L hf (hcg.fderiv 𝕜) (hg.continuous_fderiv le_rfl)]
  rfl

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