English
Let p = (a,b) ∈ ℝ × ℝ with a > 0. Then the map F: ℝ × ℝ → ℝ given by F(x,y) = x^y is strictly differentiable at p, and its derivative is the linear map sending (h1,h2) to b a^{b-1} h1 + a^b log a · h2.
Русский
Пусть p = (a,b) ∈ ℝ × ℝ и a > 0. Тогда функция F(x,y) = x^y из ℝ^2 в ℝ строго дифференцируема в точке p, производная задана линейным отображением, которое отправляет (h1,h2) в b a^{b-1} h1 + a^b log a · h2.
LaTeX
$$$\\text{Let } p=(a,b)\\in\\mathbb{R}\\times\\mathbb{R} \\text{ with } a>0. \\\\ \\\\ F: \\mathbb{R}^2\\to\\mathbb{R},\\ F(x,y)=x^y. \\\\ \\\\ \n\\text{Then } F \\text{ is strictly differentiable at } p, \\text{ and } DF_p(h_1,h_2)= b\,a^{b-1}h_1 + a^{b}\\log a\\, h_2.$$$
Lean4
/-- `(x, y) ↦ x ^ y` is strictly differentiable at `p : ℝ × ℝ` such that `0 < p.fst`. -/
theorem hasStrictFDerivAt_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.1) :
HasStrictFDerivAt (fun x : ℝ × ℝ => x.1 ^ x.2)
((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ)
p :=
by
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
(continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _
refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm
convert ((hasStrictFDerivAt_fst.log hp.ne').fun_mul hasStrictFDerivAt_snd).exp using 1
rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm, div_eq_mul_inv, smul_smul,
smul_smul, mul_assoc, add_comm]
