English
Let p=(a,b) with a<0. Then the map F(x,y)=x^y is strictly differentiable at p; its derivative is the linear map (h1,h2) ↦ b a^{b-1} h1 + (a^b log a − exp(log a · b) sin(bπ) π) h2.
Русский
Пусть p=(a,b) и a<0. Тогда F(x,y)=x^y строго дифференцируема в p; производная: (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.\\ \\\\ DF_p(h_1,h_2)= b\,a^{b-1}h_1 + \\left(a^{b}\\log a - \\exp(\\log a\\,b) \\sin(b\\pi)\\,\\pi\\right) h_2.$$$
Lean4
/-- `(x, y) ↦ x ^ y` is strictly differentiable at `p : ℝ × ℝ` such that `p.fst < 0`. -/
theorem hasStrictFDerivAt_rpow_of_neg (p : ℝ × ℝ) (hp : p.1 < 0) :
HasStrictFDerivAt (fun x : ℝ × ℝ => x.1 ^ x.2)
((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
(p.1 ^ p.2 * log p.1 - exp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ)
p :=
by
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) * cos (x.2 * π) :=
(continuousAt_fst.eventually (gt_mem_nhds hp)).mono fun p hp => rpow_def_of_neg hp _
refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm
convert
((hasStrictFDerivAt_fst.log hp.ne).fun_mul hasStrictFDerivAt_snd).exp.fun_mul
(hasStrictFDerivAt_snd.mul_const π).cos using
1
simp_rw [rpow_sub_one hp.ne, smul_add, ← add_assoc, smul_smul, ← add_smul, ← mul_assoc, mul_comm (cos _), ←
rpow_def_of_neg hp]
rw [div_eq_mul_inv, add_comm]; congr 2 <;> ring
