log_eq_integral — Mathlib

English

Represent log(1 - z)^{-1} as an integral: log(1 - z)^{-1} = z ∫_0^1 (1 - t z)^{-1} dt, when 1 - z ∈ slitPlane.

Русский

Представление log(1 - z)^{-1} через интеграл: 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,$$ при $1 - z \\in \\mathrm{slitPlane}$.$$

Lean4

/-- Represent `log (1 + z)` as an integral over the unit interval -/
theorem log_eq_integral {z : ℂ} (hz : 1 + z ∈ slitPlane) : log (1 + z) = z * ∫ (t : ℝ) in (0 : ℝ)..1, (1 + t • z)⁻¹ :=
  by
  convert
    (integral_unitInterval_deriv_eq_sub (continuousOn_one_add_mul_inv hz)
        (fun _ ht ↦ hasDerivAt_log <| StarConvex.add_smul_mem starConvex_one_slitPlane hz ht.1 ht.2)).symm using
    1
  simp only [log_one, sub_zero]

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