add_strictConcaveOn — Mathlib

English

If f is concave on s and g is strictly concave on s, then f + g is strictly concave on s.

Русский

Если f вогнута на s и g строго вогнута на s, то f+g строго вогнута на s.

LaTeX

$$$\text{If } f\text{ is concave on } s\text{ and } g\text{ is strictly concave on } s,\; f+g\text{ is strictly concave on } s$$$

Lean4

theorem add_strictConcaveOn (hf : ConcaveOn 𝕜 s f) (hg : StrictConcaveOn 𝕜 s g) : StrictConcaveOn 𝕜 s (f + g) :=
  hf.dual.add_strictConvexOn hg.dual

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