English
A function -f is strictly convex on s iff f is strictly concave on s.
Русский
Функция -f строго выпукла на s тогда и только тогда, когда f строго выпукла по конкавности на s.
LaTeX
$$$StrictConvexOn\ 𝕜\ s\ (-f) \iff StrictConcaveOn\ 𝕜\ s\ f$$$
Lean4
/-- A function `-f` is strictly convex iff `f` is strictly concave. -/
@[simp]
theorem neg_strictConvexOn_iff : StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f :=
by
constructor
· rintro ⟨hconv, h⟩
refine ⟨hconv, fun x hx y hy hxy a b ha hb hab => ?_⟩
simp only [ne_eq, Pi.neg_apply, smul_neg, lt_add_neg_iff_add_lt, add_comm, add_neg_lt_iff_lt_add] at h
exact h hx hy hxy ha hb hab
· rintro ⟨hconv, h⟩
refine ⟨hconv, fun x hx y hy hxy a b ha hb hab => ?_⟩
rw [← neg_lt_neg_iff]
simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
exact h hx hy hxy ha hb hab
