analyticAt_log — Mathlib

English

For real x > 0, the real logarithm is analytic at x.

Русский

Для действительного x > 0 функция Real.log является аналитической в точке x.

LaTeX

$$$\\text{analyticAt}_\\mathbb{R}(\\log)(x) \\text{ holds for } x>0.$$$

Lean4

@[fun_prop]
theorem analyticAt_log (hx : 0 < x) : AnalyticAt ℝ Real.log x :=
  by
  have : Real.log = fun x : ℝ ↦ (Complex.log x).re := by ext x; exact (Complex.log_ofReal_re x).symm
  rw [this]
  refine AnalyticAt.re_ofReal <| analyticAt_clog ?_
  simp [hx]

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