concaveOn_iff_pairwise_pos — Mathlib

English

ConcaveOn is equivalent to convexity of the domain along with a pairwise inequality for all x,y with positive coefficients, reversed.

Русский

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

LaTeX

$$$ConcaveOn\ 𝕜\ s\ f \iff Convex 𝕜\ s ∧ s.\text{Pairwise} (\lambda x y, ∀ a,b>0, a+b=1 \Rightarrow a f(x) + b f(y) \le f(a x + b y))$$$

Lean4

theorem concaveOn_iff_pairwise_pos {s : Set E} {f : E → β} :
    ConcaveOn 𝕜 s f ↔
      Convex 𝕜 s ∧
        s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y) :=
  convexOn_iff_pairwise_pos (β := βᵒᵈ)

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