Properties of convex functions

Main definitions

• FooBar

Main statements

• fooBar_unique

Notation

Implementation details

theorem ConvexOn.affine_le_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} (hf : ConvexOn ℝ s f) {x : ℝ} {y : ℝ} (hx : x ∈ interior s) (hy : y ∈ s) : rightDeriv f x * y + (f x - rightDeriv f x * x) ≤ f y

theorem Convex.subsingleton_of_interior_eq_empty {s : Set ℝ} (hs : Convex ℝ s) (h : interior s = ∅) : s.Subsingleton

theorem ConvexOn.exists_affine_le {f : ℝ → ℝ} {s : Set ℝ} (hf : ConvexOn ℝ s f) (hs : Convex ℝ s) : ∃ (c : ℝ) (c' : ℝ), ∀ x ∈ s, c * x + c' ≤ f x