tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero

English

If Re(z) < 0 and Im(z) = 0, then log z has a limit as one approaches z from the lower half-plane, namely log|z| − π i.

Русский

Если Re(z) < 0 и Im(z) = 0, то логарифм z имеет предел при подходе снизу к z: log|z| − π i.

LaTeX

$$$\text{If } \mathrm{Re}(z) < 0 \text{ and } \mathrm{Im}(z) = 0,\quad \mathrm{Tendsto}\log(\mathcal{N}_{z}^{\{w: w.im<0\}}) \to \log \lVert z \rVert - \pi i$$$

Lean4

theorem tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
    Tendsto log (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 <| Real.log ‖z‖ - π * I) :=
  by
  convert
    (continuous_ofReal.continuousAt.comp_continuousWithinAt (continuous_norm.continuousWithinAt.log _)).tendsto.add
      (((continuous_ofReal.tendsto _).comp <| tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using
    1
  · simp [sub_eq_add_neg]
  · lift z to ℝ using him
    simpa using hre.ne

Похожие утверждения