rpow_def_of_nonpos — Mathlib

English

If x ≤ 0, then x^y equals 1 if x = 0 and y = 0, equals 0 if x = 0 and y ≠ 0, otherwise equals exp(y log x) cos(π y).

Русский

Если x ≤ 0, то x^y = 1 при x = 0 и y = 0; x^y = 0 при x = 0 и y ≠ 0; иначе x^y = e^{(log x) y} cos(π y).

LaTeX

$$$\\forall x \\in \\mathbb{R}, x \\le 0 \\Rightarrow x^y = \\begin{cases}1 & x = 0 \\land y = 0 \\[2pt] 0 & x = 0 \\land y \\neq 0 \\[2pt] e^{(\\log x) y} \\cos(\\pi y) & x < 0 \\end{cases}$$$

Lean4

theorem rpow_def_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℝ) :
    x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y) * cos (y * π) := by
  split_ifs with h <;> simp [rpow_def, *]; exact rpow_def_of_neg (lt_of_le_of_ne hx h) _

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