strictConcaveOn_log_Iio — Mathlib

English

The function x ↦ log(-x) is strictly concave on (-∞, 0).

Русский

Функция x ↦ log(-x) строго выпуклая на (-∞, 0).

LaTeX

$$(∀ x < 0)\, StrictConvex? no; $log(-x)$ строго вогнута на $(-\infty,0)$.$$

Lean4

theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log :=
  by
  refine ⟨convex_Iio _, ?_⟩
  intro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab
  have hx' : 0 < -x := by linarith
  have hy' : 0 < -y := by linarith
  have hxy' : -x ≠ -y := by contrapose! hxy; linarith
  calc
    a • log x + b • log y = a • log (-x) + b • log (-y) := by simp_rw [log_neg_eq_log]
    _ < log (a • -x + b • -y) := (strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab)
    _ = log (-(a • x + b • y)) := by congr 1; simp only [Algebra.id.smul_eq_mul]; ring
    _ = _ := by rw [log_neg_eq_log]

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