log_inv_eq_integral — Mathlib

English

The formula log(1 - z)^{-1} = z ∫_0^1 (1 - t z)^{-1} dt holds when 1 - z ∈ slitPlane.

Русский

Формула log(1 - z)^{-1} = z ∫_0^1 (1 - t z)^{-1} dt верна при 1 - z ∈ slitPlane.

LaTeX

$$$$\\log(1 - z)^{-1} = z \\int_{0}^{1} (1 - t z)^{-1}\\, dt, \\quad 1 - z \\in \\mathrm{slitPlane}.$$$$

Lean4

/-- Represent `log (1 - z)⁻¹` as an integral over the unit interval -/
theorem log_inv_eq_integral {z : ℂ} (hz : 1 - z ∈ slitPlane) :
    log (1 - z)⁻¹ = z * ∫ (t : ℝ) in (0 : ℝ)..1, (1 - t • z)⁻¹ :=
  by
  rw [sub_eq_add_neg 1 z] at hz ⊢
  rw [log_inv _ <| slitPlane_arg_ne_pi hz, neg_eq_iff_eq_neg, ← neg_mul]
  convert log_eq_integral hz using 5
  rw [sub_eq_add_neg, smul_neg]

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