add_const — Mathlib

English

If f is strictly concave on s, then f + constant is strictly concave on s.

Русский

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

LaTeX

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

Lean4

theorem add_const {γ : Type*} {f : E → γ} [AddCommMonoid γ] [PartialOrder γ] [IsOrderedCancelAddMonoid γ] [Module 𝕜 γ]
    (hf : StrictConcaveOn 𝕜 s f) (b : γ) : StrictConcaveOn 𝕜 s (f + fun _ => b) :=
  hf.add_concaveOn (concaveOn_const _ hf.1)

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