rpow_eq_nhds_of_neg — Mathlib

English

For p = (x,y) with x < 0, the expression x^y has expansion exp(log x · y) cos(yπ) in a neighborhood sense.

Русский

При x < 0 выражение x^y имеет в окрестности вид exp(log x · y) cos(yπ).

LaTeX

$$$$\\text{If } x<0,\\quad x^{y}= \\exp(\\log x \\cdot y) \\cos(y\\pi) \\text{ in a neighborhood sense}. $$$$

Lean4

theorem rpow_eq_nhds_of_neg {p : ℝ × ℝ} (hp_fst : p.fst < 0) :
    (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) * cos (x.2 * π) :=
  by
  suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, x.1 < 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [rpow_def_of_neg hx]
  exact IsOpen.eventually_mem (isOpen_lt continuous_fst continuous_const) hp_fst

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