English
For a fixed z with Re(z) > 0, the map x ↦ x^z is continuous as a function from ℝ to ℂ.
Русский
Для фиксированного z с Re(z) > 0 отображение x ↦ x^z непрерывно с ℝ в ℂ.
LaTeX
$$$$\forall z\in\mathbb{C},\ \Re(z)>0 \Rightarrow \text{Continuous}(x\mapsto x^z)\text{ (as } x\in\mathbb{R}).$$$$
Lean4
/-- See also `continuousAt_cpow` and `Complex.continuousAt_cpow_of_re_pos`. -/
theorem continuousAt_cpow_zero_of_re_pos {z : ℂ} (hz : 0 < z.re) : ContinuousAt (fun x : ℂ × ℂ => x.1 ^ x.2) (0, z) :=
by
have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'
rw [ContinuousAt, zero_cpow hz₀, tendsto_zero_iff_norm_tendsto_zero]
refine squeeze_zero (fun _ => norm_nonneg _) (fun _ => norm_cpow_le _ _) ?_
simp only [div_eq_mul_inv, ← Real.exp_neg]
refine Tendsto.zero_mul_isBoundedUnder_le ?_ ?_
·
convert (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _) _ <;>
simp [hz, Real.zero_rpow hz.ne']
· simp only [Function.comp_def, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
rcases exists_gt |im z| with ⟨C, hC⟩
refine ⟨Real.exp (π * C), eventually_map.2 ?_⟩
refine
(((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono fun z hz =>
Real.exp_le_exp.2 <| (neg_le_abs _).trans ?_
rw [_root_.abs_mul]
exact mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _) Real.pi_pos.le
