strictConcaveOn_iff_div — Mathlib

English

A function is concave on s iff it satisfies the convexity-duality condition under division (convexity of the dual on the opposite order).

Русский

Функция конкавна на s тогда, когда выполняется двойственность выпуклости через деление (выпуклость в противоположном порядке).

LaTeX

$$$ConcaveOn\ 𝕜\ s\ f \iff Convex 𝕜\ s ∧ ∀ x\in s, ∀ y\in s, ∀ a,b, 0≤a,0≤b,0

Lean4

theorem strictConcaveOn_iff_div {f : E → β} :
    StrictConcaveOn 𝕜 s f ↔
      Convex 𝕜 s ∧
        ∀ ⦃x⦄,
          x ∈ s →
            ∀ ⦃y⦄,
              y ∈ s →
                x ≠ y →
                  ∀ ⦃a b : 𝕜⦄,
                    0 < a →
                      0 < b → (a / (a + b)) • f x + (b / (a + b)) • f y < f ((a / (a + b)) • x + (b / (a + b)) • y) :=
  strictConvexOn_iff_div (β := βᵒᵈ)

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