concaveOn — Mathlib

English

If a function is uniformly concave on a set with a nonnegative modulus, then it is concave on that set.

Русский

Если функция униформно вогнута на некотором множестве с неотрицательным модулем, то она вогнута на этом множестве.

LaTeX

$$$$ \text{UniformConcaveOn}(s,\phi,f) \land 0 \le \phi \Rightarrow \text{ConcaveOn}(\mathbb{R},s,f). $$$$

Lean4

theorem concaveOn (hf : UniformConcaveOn s φ f) (hφ : 0 ≤ φ) : ConcaveOn ℝ s f := by simpa using hf.mono hφ

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