English
If the first coordinate is nonzero, the map (x,y) ↦ x^y is smooth; more precisely, it is ContDiffOfAllOrders at every point p with p.fst ≠ 0.
Русский
Если первая координата не равна нулю, функция (x,y) ↦ x^y гладкая; более точно, она бесконечно дифференцируема в каждой точке p с p.fst ≠ 0.
LaTeX
$$$\\forall p=(a,b)\\in\\mathbb{R}^2\\; (a\\neq 0) \\Rightarrow \\forall n\\in\\mathbb{N},\\ ContDiffAt\\mathbb{R}\\ n (\\lambda p:\\mathbb{R}\\times\\mathbb{R}.\\, p_1^{p_2})\\ p.$$$
Lean4
/-- The function `fun (x, y) => x ^ y` is infinitely smooth at `(x, y)` unless `x = 0`. -/
theorem contDiffAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) {n : WithTop ℕ∞} :
ContDiffAt ℝ n (fun p : ℝ × ℝ => p.1 ^ p.2) p :=
by
rcases hp.lt_or_gt with hneg | hpos
exacts
[(((contDiffAt_fst.log hneg.ne).mul contDiffAt_snd).exp.mul
(contDiffAt_snd.mul contDiffAt_const).cos).congr_of_eventuallyEq
((continuousAt_fst.eventually (gt_mem_nhds hneg)).mono fun p hp => rpow_def_of_neg hp _),
((contDiffAt_fst.log hpos.ne').mul contDiffAt_snd).exp.congr_of_eventuallyEq
((continuousAt_fst.eventually (lt_mem_nhds hpos)).mono fun p hp => rpow_def_of_pos hp _)]
