log_ofReal_of_pos

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

URI: https://scilib.ai/kg/mathlib#ENNReal.log_ofReal_of_pos

English

For |x| < 1, log(1+x) - log(1-x) equals sum over k≥0 of 2/(2k+1) x^{2k+1}.

Русский

Для |x| < 1 log(1+x) - log(1-x) равняется сумме по k≥0: 2/(2k+1) x^{2k+1}.

LaTeX

$$$\sum_{k=0}^{\infty} \dfrac{2}{2k+1} x^{2k+1} = \log(1+x) - \log(1-x), \quad |x|<1$$$

Lean4

theorem log_ofReal_of_pos {x : ℝ} (hx : 0 < x) : log (ENNReal.ofReal x) = Real.log x := by
  rw [log_ofReal, if_neg hx.not_ge]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru