ofReal_cpow_const — Mathlib

English

Let f: ℝ → ℝ be differentiable at x. If f(x) ≠ 0 and c ≠ 0, then the complex-valued function y ↦ (f(y):ℂ)^{c} is differentiable at x.

Русский

Пусть f: ℝ → ℝ дифференцируема в x. Если f(x) ≠ 0 и c ≠ 0, то функция y ↦ (f(y):ℂ)^{c} дифференцируема в x.

LaTeX

$$$\\text{Let }f:\\mathbb{R}\\to\\mathbb{R}\\text{ be differentiable at }x.\\quad f(x)\\neq 0,\\ c\\neq 0:\\ \\text{then } y\\mapsto (f(y)\\!:\\!\\mathbb{C})^{c}\\text{ is differentiable at }x.$$$

Lean4

/-- A version of `DifferentiableAt.cpow_const` for a real function. -/
theorem ofReal_cpow_const {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (h0 : f x ≠ 0) (h1 : c ≠ 0) :
    DifferentiableAt ℝ (fun (y : ℝ) => (f y : ℂ) ^ c) x :=
  (hasDerivAt_ofReal_cpow_const h0 h1).differentiableAt.comp x hf

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