English
For x ∈ ℝ≥0∞ and y ∈ ℝ, log(x^y) = y log x.
Русский
Для x ∈ ℝ≥0∞ и y ∈ ℝ верно log(x^y) = y log x.
LaTeX
$$$\\log(x^y) = y \\cdot \\log x$$$
Lean4
theorem log_rpow {x : ℝ≥0∞} {y : ℝ} : log (x ^ y) = y * log x :=
by
rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)
· rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
·
simp only [ENNReal.zero_rpow_def y, not_lt_of_gt y_neg, y_neg.ne, if_false, log_top, log_zero,
EReal.coe_mul_bot_of_neg y_neg]
· rw [ENNReal.top_rpow_of_neg y_neg, log_zero, log_top, EReal.coe_mul_top_of_neg y_neg]
· have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte, rpow_eq_top_iff]
norm_cast
exact ENNReal.toReal_rpow x y ▸ Real.log_rpow x_real y
· simp
· rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
· rw [ENNReal.zero_rpow_of_pos y_pos, log_zero, EReal.mul_bot_of_pos]; norm_cast
· rw [ENNReal.top_rpow_of_pos y_pos, log_top, EReal.mul_top_of_pos]; norm_cast
· have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte, rpow_eq_top_iff]
norm_cast
exact ENNReal.toReal_rpow x y ▸ Real.log_rpow x_real y
