half_mul_log_add_log_abs

Mathlib.Analysis.SpecialFunctions.Log.PosLog

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

← MathLib Explorer

English

1/2 (log r + |log r|) = log⁺ r.

Русский

1/2 (лог r + |лог r|) = log⁺ r.

LaTeX

$$\frac{1}{2}\bigl(\log r + |\log r|\bigr) = \log^{+} r$$

Lean4

/-- Presentation of `log⁺` in terms of `log`. -/
theorem half_mul_log_add_log_abs {r : ℝ} : 2⁻¹ * (log r + |log r|) = log⁺ r :=
  by
  by_cases hr : 0 ≤ log r
  · simp [posLog, hr, abs_of_nonneg]
    ring
  · simp [posLog, le_of_not_ge hr, abs_of_nonpos]

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

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

Разделы

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

Аффилиация

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