log_inv_eq_ite — Mathlib

English

log(conj x) = conj(log x) whenever Arg x ≠ π.

Русский

log(conj x) = conj(log x), если Arg x ≠ π.

LaTeX

$$$\log(\overline{x}) = \overline{\log x}, \quad \arg x \neq \pi.$$$

Lean4

theorem log_inv_eq_ite (x : ℂ) : log x⁻¹ = if x.arg = π then -conj (log x) else -log x :=
  by
  by_cases hx : x = 0
  · simp [hx]
  rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
  · simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_norm_sq, Real.log_pow, Nat.cast_two, ofReal_mul,
      neg_add, mul_neg, neg_neg]
    norm_num
    grind
  · rwa [inv_pos, Complex.normSq_pos]
  · rwa [map_ne_zero]

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