concaveOn_iff_forall_pos — Mathlib

English

ConcaveOn is equivalent to convexity of the domain and the reverse inequality for all positive coefficients.

Русский

ConcaveOn эквивалентна выпуклости области и обратному неравенству для всех положительных коэффициентов.

LaTeX

$$$ConcaveOn\ 𝕜\ s\ f \iff (Convex\ 𝕜\ s \land \forall x\in s\forall y\in s\forall a,b>0, a+b=1 \Rightarrow a f(x) + b f(y) \le f(a x + b y))$$$

Lean4

theorem concaveOn_iff_forall_pos {s : Set E} {f : E → β} :
    ConcaveOn 𝕜 s f ↔
      Convex 𝕜 s ∧
        ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y) :=
  convexOn_iff_forall_pos (β := βᵒᵈ)

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