concaveOn — Mathlib

English

ConcaveOn is equivalent to the convexity of the hypograph.

Русский

ConcaveOn эквивалентна выпуклости гипогипографа.

LaTeX

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

Lean4

/-- A linear map is concave. -/
theorem concaveOn (f : E →ₗ[𝕜] β) {s : Set E} (hs : Convex 𝕜 s) : ConcaveOn 𝕜 s f :=
  ⟨hs, fun _ _ _ _ _ _ _ _ _ => by rw [f.map_add, f.map_smul, f.map_smul]⟩

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