cpow_eq_nhds — Mathlib

English

For a ≠ 0, the function x ↦ x^b is asymptotically exp(log x · b) near x = a; i.e., x^b equals exp((log x) b) in a neighborhood.

Русский

При a ≠ 0 функция x ↦ x^b близко к x → a эквивалентна exp((log x)·b).

LaTeX

$$$$\\text{If } a \\neq 0,\\quad x \\mapsto x^{b} \\sim \\exp(\\log x \\cdot b) \\quad \\text{as } x \\to a.$$$$

Lean4

theorem cpow_eq_nhds {a b : ℂ} (ha : a ≠ 0) : (fun x => x ^ b) =ᶠ[𝓝 a] fun x => exp (log x * b) :=
  by
  suffices ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [cpow_def_of_ne_zero hx]
  exact IsOpen.eventually_mem isOpen_ne ha

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