English
The map (x,y) ↦ x^y from C×C to C is differentiable in the sense of Frechet derivative, with derivative given by a standard combination of x^y, log x, and y-derivatives.
Русский
Отображение (x, y) ↦ x^y с C×C в C дифференцируемо в смысле Фреше, производная выражается через x^y, log x и производные по y.
LaTeX
$$$\\forall p \\in \\mathbb{C}^2, \\; \\text{HasStrictFDerivAt } (p \\mapsto p_1^{p_2}) = (p_2 p_1^{p_2-1}) \\cdot \\mathrm{fst} + (p_1^{p_2} \\log p_1) \\cdot \\mathrm snd$$$
Lean4
theorem hasStrictFDerivAt_cpow {p : ℂ × ℂ} (hp : p.1 ∈ slitPlane) :
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 A : p.1 ≠ 0 := slitPlane_ne_zero hp
have : (fun x : ℂ × ℂ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
((isOpen_ne.preimage continuous_fst).eventually_mem A).mono fun p hp => cpow_def_of_ne_zero hp _
rw [cpow_sub _ _ A, cpow_one, mul_div_left_comm, mul_smul, mul_smul]
refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm
simpa only [cpow_def_of_ne_zero A, div_eq_mul_inv, mul_smul, add_comm, smul_add] using
((hasStrictFDerivAt_fst.clog hp).mul hasStrictFDerivAt_snd).cexp
