neg_convexOn_iff — Mathlib

English

A function -f is convex on s if and only if f is concave on s.

Русский

Функция -f выпукла на s тогда и только тогда, когда f выпуклая по отношению к углу конкавности на s.

LaTeX

$$$ConvexOn\ 𝕜\ s\ (-f) \iff ConcaveOn\ 𝕜\ s\ f$$$

Lean4

/-- A function `-f` is convex iff `f` is concave. -/
@[simp]
theorem neg_convexOn_iff : ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f :=
  by
  constructor
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩
    simpa [add_comm] using h hx hy ha hb hab
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩
    rw [← neg_le_neg_iff]
    simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
    exact h hx hy ha hb hab

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