log_mul_eq_add_log_iff — Mathlib

English

For x,y ≠ 0, log(x y) = log x + log y if and only if Arg x + Arg y ∈ (-π, π].

Русский

Для x, y ≠ 0 выполняется log(x y) = log x + log y тогда и только тогда, когда Arg x + Arg y ∈ (-π, π].

LaTeX

$$$\log(xy) = \log x + \log y \iff \operatorname{arg} x + \operatorname{arg} y \in (-\pi, \pi].$$$

Lean4

theorem log_mul_eq_add_log_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    log (x * y) = log x + log y ↔ arg x + arg y ∈ Set.Ioc (-π) π :=
  by
  refine Complex.ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀
  simp_rw [add_re, add_im, log_re, log_im, norm_mul, Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀),
    true_and]

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