concaveOn_of_lt — Mathlib

English

If a function is strictly convex on s, then the set {x ∈ s | f(x) < r} is convex for any r.

Русский

Если функция строго выпуклая на s, то множество {x ∈ s | f(x) < r} выпукло для любого r.

LaTeX

$$$\forall r:\; {x\in s \mid f(x)

Lean4

/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
structures aren't necessarily compatible), in order to prove that it is concave it suffices to
verify the inequality `a • f x + b • f y ≤ f (a • x + b • y)` for `x < y` and positive `a`, `b`. The
main use case is `E = ℝ` however one can apply it, e.g., to `ℝ^n` with lexicographic order. -/
theorem concaveOn_of_lt (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃x⦄,
        x ∈ s → ∀ ⦃y⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)) :
    ConcaveOn 𝕜 s f :=
  LinearOrder.convexOn_of_lt (β := βᵒᵈ) hs hf

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