English
Let F(x,y)=x^y. For p=(a,b) with a<0, the derivative is the linear map (h1,h2) ↦ b a^{b-1} h1 + (a^b log a − exp(log a · b) sin(bπ) π) h2.
Русский
Пусть F(x,y)=x^y. При p=(a,b) с a<0 производная имеет вид (h1,h2) ↦ b a^{b-1} h1 + (a^b log a − e^{log a · b} sin(bπ) π) h2.
LaTeX
$$$\\text{Let } p=(a,b)\\text{ with } a<0.\\\\ D F_p(h_1,h_2)= b\,a^{b-1}h_1 + \\Bigl(a^{b}\\log a - e^{(\\log a) b}\\sin(b\\pi)\\,\\pi\\Bigr) h_2.$$$
Lean4
theorem hasStrictDerivAt_rpow_const_of_ne {x : ℝ} (hx : x ≠ 0) (p : ℝ) :
HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x :=
by
rcases hx.lt_or_gt with hx | hx
· have :=
(hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
((hasStrictDerivAt_id x).prodMk (hasStrictDerivAt_const x p))
convert this using 1; simp
· simpa using (hasStrictDerivAt_id x).rpow (hasStrictDerivAt_const x p) hx
