posLog_sub_posLog_inv

Mathlib.Analysis.SpecialFunctions.Log.PosLog

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

← MathLib Explorer

English

log⁺ r − log⁺ r^{−1} = log r.

Русский

log⁺ r − log⁺ r^{−1} = log r.

LaTeX

$$\log^{+} r - \log^{+} r^{-1} = \log r$$

Lean4

/-- Presentation of `log` in terms of its positive part. -/
theorem posLog_sub_posLog_inv {r : ℝ} : log⁺ r - log⁺ r⁻¹ = log r :=
  by
  rw [posLog_def, posLog_def, log_inv]
  by_cases h : 0 ≤ log r
  · simp [h]
  · rw [not_le] at h
    simp [neg_nonneg.1 (Left.nonneg_neg_iff.2 h.le)]

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

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

Разделы

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

Аффилиация

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