English
The map (x,y) ↦ x^y is continuous at (x,y) provided 0 < Im(y) or x ≠ 0, in the real-to-complex setting.
Русский
Отображение (x,y) ↦ x^y непрерывно в точке (x,y) при условии 0 < Im(y) или x ≠ 0, в связке ℝ→ℂ.
LaTeX
$$$$\forall x\in\mathbb{R},\forall y\in\mathbb{C},\ (0<\operatorname{Im} y) \lor (x \neq 0) \Rightarrow \text{ContinuousAt}((x,y)\mapsto x^y)\,(x,y).$$$$
Lean4
/-- Continuity of `(x, y) ↦ x ^ y` as a function on `ℝ × ℂ`. -/
theorem continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
ContinuousAt (fun p => (p.1 : ℂ) ^ p.2 : ℝ × ℂ → ℂ) (x, y) :=
by
rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
· -- x > 0 : easy case
have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
refine (continuousAt_cpow (Or.inl ?_)).comp this
rwa [ofReal_re]
· -- x = 0 : reduce to continuousAt_cpow_zero_of_re_pos
have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ :=
by
rw [ofReal_zero]
apply continuousAt_cpow_zero_of_re_pos
tauto
have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := by fun_prop
exact A.comp_of_eq B rfl
· -- x < 0 : difficult case
suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y)
by
refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
apply ContinuousAt.mul
· refine (continuousAt_cpow (Or.inl ?_)).comp A
rwa [neg_re, ofReal_re, neg_pos]
· exact (continuous_exp.comp (continuous_const.mul continuous_snd)).continuousAt
