quasiconcaveOn_iff_min_le — Mathlib

English

QuasiconcaveOn 𝕜 s f is equivalent to convexity of s together with the condition that for all x,y ∈ s and a,b ≥ 0 with a+b=1, min(f(x), f(y)) ≤ f(ax+by).

Русский

QuasiconcaveOn 𝕜 s f эквивалентна выпуклости s и условию min(f(x), f(y)) ≤ f(ax+by) для всех x,y ∈ s и a,b ≥ 0, a+b=1.

LaTeX

$$$QuasiconcaveOn\ 𝕜\ s\ f \iff Convex\ 𝕜\ s \land \forall\{x\}, x\in s \to \forall\{y\}, y\in s \to \forall\{a,b\}: 𝕜, 0\le a\to 0\le b\to a+b=1\to \min(f(x),f(y)) \le f(a\cdot x+b\cdot y)$$$

Lean4

theorem quasiconcaveOn_iff_min_le :
    QuasiconcaveOn 𝕜 s f ↔
      Convex 𝕜 s ∧
        ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y) :=
  quasiconvexOn_iff_le_max (β := βᵒᵈ)

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