English
For x,y ∈ ℝ≥0∞, log(xy) = log x + log y.
Русский
Для x,y ∈ ℝ≥0∞ верно log(xy) = log x + log y.
LaTeX
$$$\\log(xy) = \\log x + \\log y$$$
Lean4
theorem log_mul_add {x y : ℝ≥0∞} : log (x * y) = log x + log y :=
by
rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
· simp
· rw [log_top]
rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
· rw [mul_zero, log_zero, EReal.add_bot]
· simp
· rw [log_pos_real' y_real, ENNReal.top_mul', EReal.top_add_coe, log_eq_top_iff]
simp only [ite_eq_right_iff, zero_ne_top, imp_false]
exact (ENNReal.toReal_pos_iff.1 y_real).1.ne'
· rw [log_pos_real' x_real]
rcases ENNReal.trichotomy y with (rfl | rfl | y_real)
· simp
· simp [(ENNReal.toReal_pos_iff.1 x_real).1.ne']
· rw_mod_cast [log_pos_real', log_pos_real' y_real, ENNReal.toReal_mul]
· exact Real.log_mul x_real.ne' y_real.ne'
rw [toReal_mul]
positivity
