log_sub_self_isBigO

Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

URI: https://scilib.ai/kg/mathlib#Complex.log_sub_self_isBigO

← MathLib Explorer

English

Same Big-O bound as above for log(1+z) − logTaylor(n+1) z as z→0.

Русский

Та же граница Big-O для log(1+z) − logTaylor(n+1) z при z→0.

LaTeX

$$$\\log(1+z) - \\mathrm{logTaylor}(n+1)\\,z =O(z^{n+1})\\quad \\text{при } z \\to 0$$$

Lean4

theorem log_sub_self_isBigO : (fun z ↦ log (1 + z) - z) =O[𝓝 0] fun z ↦ z ^ 2 :=
  by
  convert log_sub_logTaylor_isBigO 1
  simp [logTaylor_succ, logTaylor_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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