convex_lt — Mathlib

English

If f is convex on s, then the epigraph of f over s is convex.

Русский

Если f выпукла на s, то эпиграф f над s выпукл.

LaTeX

$$$\text{If } f \text{ is convex on } s,\; \{(x,t)\mid x\in s,\; t\ge f(x)\} \text{ is convex}$$$

Lean4

theorem convex_lt (hf : ConvexOn 𝕜 s f) (r : β) : Convex 𝕜 ({x ∈ s | f x < r}) :=
  convex_iff_forall_pos.2 fun x hx y hy a b ha hb hab =>
    ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
      calc
        f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha.le hb.le hab
        _ < a • r + b • r :=
          (add_lt_add_of_lt_of_le (smul_lt_smul_of_pos_left hx.2 ha) (smul_le_smul_of_nonneg_left hy.2.le hb.le))
        _ = r := Convex.combo_self hab _⟩

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