continuousOn_one_add_mul_inv — Mathlib

English

Represent log(1 + z) as an integral over the unit interval: log(1+z) = z ∫_0^1 (1 + t z)^{-1} dt, for z with 1+z in slitPlane.

Русский

Представление log(1+z) через интеграл по единичному отрезку: log(1+z) = z ∫_0^1 (1 + t z)^{-1} dt при 1+z ∈ slitPlane.

LaTeX

$$$$\\log(1 + z) = z \\int_{0}^{1} (1 + t z)^{-1}\\, dt, \\quad \\text{если } 1+z \\in \\mathrm{slitPlane}.$$$$

Lean4

theorem continuousOn_one_add_mul_inv {z : ℂ} (hz : 1 + z ∈ slitPlane) :
    ContinuousOn (fun t : ℝ ↦ (1 + t • z)⁻¹) (Set.Icc 0 1) :=
  ContinuousOn.inv₀ (by fun_prop)
    (fun _ ht ↦ slitPlane_ne_zero <| StarConvex.add_smul_mem starConvex_one_slitPlane hz ht.1 ht.2)

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