comp_add_const — Mathlib

English

Let f: 𝕜 → F be differentiable at x + a with derivative f'. Then the shifted function h(t) = f(t + a) is differentiable at t = x with derivative f'.

Русский

Пусть f: 𝕜 → F дифференцируема в точке x + a с производной f'. Тогда функция h(t) = f(t + a) дифференцируема в t = x и её производная равна f'.

LaTeX

$$$ Df(x+a) = f' \Rightarrow D\bigl(x \mapsto f(x+a)\bigr)(x) = f' $$$

Lean4

/-- Translation in the domain does not change the derivative. -/
theorem comp_add_const (x a : 𝕜) (hf : HasDerivAt f f' (x + a)) : HasDerivAt (fun x ↦ f (x + a)) f' x := by
  simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.add_const a

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