posLog_eq_log_max_one

Mathlib.Analysis.SpecialFunctions.Log.PosLog

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

← MathLib Explorer

English

If x ≥ 0, then log⁺ x = log(max(1, x)).

Русский

Если x ≥ 0, то log⁺ x = log(max(1, x)).

LaTeX

$$log^{+} x = \log(\max\{1, x\}) \quad (x \ge 0)$$

Lean4

/-- The function `log⁺` equals `log (max 1 _)` for non-negative real numbers. -/
theorem posLog_eq_log_max_one {x : ℝ} (hx : 0 ≤ x) : log⁺ x = log (max 1 x) := by
  grind [le_abs, posLog_eq_log, log_one, max_eq_left, log_nonpos, posLog_def]

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

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

Разделы

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

Аффилиация

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