convex_epigraph — Mathlib

English

ConvexOn 𝕜 s f is equivalent to the convexity of its epigraph over s.

Русский

Выпуклость на s эквивалентна выпуклости эпиграфа функции над s.

LaTeX

$$$ConvexOn\ 𝕜\ s\ f \iff Convex\ 𝕜\ {p : E \times β | p.1 \in s \wedge f(p.1) \le p.2}$$$

Lean4

theorem convex_epigraph (hf : ConvexOn 𝕜 s f) : Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
  by
  rintro ⟨x, r⟩ ⟨hx, hr⟩ ⟨y, t⟩ ⟨hy, ht⟩ a b ha hb hab
  refine ⟨hf.1 hx hy ha hb hab, ?_⟩
  calc
    f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
    _ ≤ a • r + b • t := by gcongr

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