English
If either base is nonzero or exponent is nonzero, the map y ↦ x^y has a strict derivative equal to x^y log x.
Русский
Если основание не равно нулю или показатель степени не равен нулю, отображение y ↦ x^y имеет строгую производную x^y log x.
LaTeX
$$$\\\\forall x,y \\in \\mathbb{C}, (x \\neq 0 \\lor y \\neq 0) \\\\Rightarrow HasStrictDerivAt (\\\\lambda t, x^t) (x^y \\log x) \\\\text{ at } y$$$
Lean4
theorem hasStrictDerivAt_const_cpow {x y : ℂ} (h : x ≠ 0 ∨ y ≠ 0) :
HasStrictDerivAt (fun y => x ^ y) (x ^ y * log x) y :=
by
rcases em (x = 0) with (rfl | hx)
· replace h := h.neg_resolve_left rfl
rw [log_zero, mul_zero]
refine (hasStrictDerivAt_const y 0).congr_of_eventuallyEq ?_
exact (isOpen_ne.eventually_mem h).mono fun y hy => (zero_cpow hy).symm
· simpa only [cpow_def_of_ne_zero hx, mul_one] using ((hasStrictDerivAt_id y).const_mul (log x)).cexp
