posLog_eq_log

Mathlib.Analysis.SpecialFunctions.Log.PosLog

URI: https://scilib.ai/kg/mathlib#Real.posLog_eq_log

← MathLib Explorer

English

If 1 ≤ |x|, then log⁺ x = log x.

Русский

Если 1 ≤ |x|, то log⁺ x = log x.

LaTeX

$$log^{+} x = \log x \quad \text{если } 1 \le |x|$$

Lean4

/-- The function `log⁺` equals `log` outside of the interval (-1,1). -/
theorem posLog_eq_log {x : ℝ} (hx : 1 ≤ |x|) : log⁺ x = log x :=
  by
  simp only [posLog, sup_eq_right]
  rw [← log_abs]
  apply log_nonneg hx

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

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

Разделы

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

Аффилиация

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