negMulLog_mul — Mathlib

English

For x > 0 and y > 0, negMulLog(xy) = y negMulLog x + x negMulLog y.

Русский

Для x > 0 и y > 0 выполнено: negMulLog(xy) = y negMulLog x + x negMulLog y.

LaTeX

$$(x > 0) \land (y > 0) \Rightarrow \operatorname{negMulLog}(xy) = y\operatorname{negMulLog} x + x\operatorname{negMulLog} y$$

Lean4

theorem negMulLog_mul (x y : ℝ) : negMulLog (x * y) = y * negMulLog x + x * negMulLog y :=
  by
  simp only [negMulLog, neg_mul]
  by_cases hx : x = 0
  · simp [hx]
  by_cases hy : y = 0
  · simp [hy]
  rw [log_mul hx hy]
  ring

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