HepLean Documentation

Mathlib.Analysis.Convex.Function

Convex and concave functions #

This file defines convex and concave functions in vector spaces and proves the finite Jensen inequality. The integral version can be found in Analysis.Convex.Integral.

A function f : E → β is ConvexOn a set s if s is itself a convex set, and for any two points x y ∈ s, the segment joining (x, f x) to (y, f y) is above the graph of f. Equivalently, ConvexOn 𝕜 f s means that the epigraph {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} is a convex set.

Main declarations #

ConvexOn 𝕜 s f: The function f is convex on s with scalars 𝕜.
ConcaveOn 𝕜 s f: The function f is concave on s with scalars 𝕜.
StrictConvexOn 𝕜 s f: The function f is strictly convex on s with scalars 𝕜.
StrictConcaveOn 𝕜 s f: The function f is strictly concave on s with scalars 𝕜.

def ConvexOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] (s : Set E) (f : E → β) :

Convexity of functions

Equations

ConvexOn 𝕜 s f = (Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y)

Instances For

def ConcaveOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] (s : Set E) (f : E → β) :

Concavity of functions

Equations

ConcaveOn 𝕜 s f = (Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y))

Instances For

def StrictConvexOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] (s : Set E) (f : E → β) :

Strict convexity of functions

Equations

StrictConvexOn 𝕜 s f = (Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y)

Instances For

def StrictConcaveOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] (s : Set E) (f : E → β) :

Strict concavity of functions

Equations

StrictConcaveOn 𝕜 s f = (Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y))

Instances For

theorem ConvexOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) :

ConcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)

theorem ConcaveOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) :

ConvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)

theorem StrictConvexOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) :

StrictConcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)

theorem StrictConcaveOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) :

StrictConvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)

theorem convexOn_id {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [OrderedAddCommMonoid β] [SMul 𝕜 β] {s : Set β} (hs : Convex 𝕜 s) :

ConvexOn 𝕜 s id

theorem concaveOn_id {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [OrderedAddCommMonoid β] [SMul 𝕜 β] {s : Set β} (hs : Convex 𝕜 s) :

ConcaveOn 𝕜 s id

theorem ConvexOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConvexOn 𝕜 s f) (hfg : Set.EqOn f g s) :

ConvexOn 𝕜 s g

theorem ConcaveOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConcaveOn 𝕜 s f) (hfg : Set.EqOn f g s) :

ConcaveOn 𝕜 s g

theorem StrictConvexOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConvexOn 𝕜 s f) (hfg : Set.EqOn f g s) :

StrictConvexOn 𝕜 s g

theorem StrictConcaveOn.congr {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConcaveOn 𝕜 s f) (hfg : Set.EqOn f g s) :

StrictConcaveOn 𝕜 s g

theorem ConvexOn.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {t : Set E} (hf : ConvexOn 𝕜 t f) (hst : s ⊆ t) (hs : Convex 𝕜 s) :

ConvexOn 𝕜 s f

theorem ConcaveOn.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {t : Set E} (hf : ConcaveOn 𝕜 t f) (hst : s ⊆ t) (hs : Convex 𝕜 s) :

ConcaveOn 𝕜 s f

theorem StrictConvexOn.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {t : Set E} (hf : StrictConvexOn 𝕜 t f) (hst : s ⊆ t) (hs : Convex 𝕜 s) :

StrictConvexOn 𝕜 s f

theorem StrictConcaveOn.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} {t : Set E} (hf : StrictConcaveOn 𝕜 t f) (hst : s ⊆ t) (hs : Convex 𝕜 s) :

StrictConcaveOn 𝕜 s f

theorem ConvexOn.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : ConvexOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) :

ConvexOn 𝕜 s (g ∘ f)

theorem ConcaveOn.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : ConcaveOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) :

ConcaveOn 𝕜 s (g ∘ f)

theorem ConvexOn.comp_concaveOn {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : ConvexOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) :

ConvexOn 𝕜 s (g ∘ f)

theorem ConcaveOn.comp_convexOn {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : ConcaveOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) :

ConcaveOn 𝕜 s (g ∘ f)

theorem StrictConvexOn.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : StrictConvexOn 𝕜 (f '' s) g) (hf : StrictConvexOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s)) (hf' : Set.InjOn f s) :

StrictConvexOn 𝕜 s (g ∘ f)

theorem StrictConcaveOn.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : StrictConcaveOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s)) (hf' : Set.InjOn f s) :

StrictConcaveOn 𝕜 s (g ∘ f)

theorem StrictConvexOn.comp_strictConcaveOn {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : StrictConvexOn 𝕜 (f '' s) g) (hf : StrictConcaveOn 𝕜 s f) (hg' : StrictAntiOn g (f '' s)) (hf' : Set.InjOn f s) :

StrictConvexOn 𝕜 s (g ∘ f)

theorem StrictConcaveOn.comp_strictConvexOn {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : StrictConvexOn 𝕜 s f) (hg' : StrictAntiOn g (f '' s)) (hf' : Set.InjOn f s) :

StrictConcaveOn 𝕜 s (g ∘ f)

theorem ConvexOn.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) :

ConvexOn 𝕜 s (f + g)

theorem ConcaveOn.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) :

ConcaveOn 𝕜 s (f + g)

theorem convexOn_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} (c : β) (hs : Convex 𝕜 s) :

ConvexOn 𝕜 s fun (x : E) => c

theorem concaveOn_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} (c : β) (hs : Convex 𝕜 s) :

ConcaveOn 𝕜 s fun (x : E) => c

theorem ConvexOn.add_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) (b : β) :

ConvexOn 𝕜 s (f + fun (x : E) => b)

theorem ConcaveOn.add_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) (b : β) :

ConcaveOn 𝕜 s (f + fun (x : E) => b)

theorem convexOn_of_convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} (h : Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}) :

ConvexOn 𝕜 s f

theorem concaveOn_of_convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} (h : Convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}) :

ConcaveOn 𝕜 s f

theorem ConvexOn.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}

theorem ConcaveOn.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}

theorem ConvexOn.convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) :

Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}

theorem ConcaveOn.convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) :

Convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}

theorem convexOn_iff_convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} :

ConvexOn 𝕜 s f ↔ Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}

theorem concaveOn_iff_convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} :

ConcaveOn 𝕜 s f ↔ Convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1}

theorem ConvexOn.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) (c : E) :

ConvexOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => c + z)

Right translation preserves convexity.

theorem ConcaveOn.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) (c : E) :

ConcaveOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => c + z)

Right translation preserves concavity.

theorem ConvexOn.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) (c : E) :

ConvexOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => z + c)

Left translation preserves convexity.

theorem ConcaveOn.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) (c : E) :

ConcaveOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => z + c)

Left translation preserves concavity.

theorem convexOn_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

theorem concaveOn_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

theorem convexOn_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ s.Pairwise fun (x y : E) => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

theorem concaveOn_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ s.Pairwise fun (x y : E) => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

theorem LinearMap.convexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] (f : E →ₗ[𝕜] β) {s : Set E} (hs : Convex 𝕜 s) :

ConvexOn 𝕜 s ⇑f

A linear map is convex.

theorem LinearMap.concaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] (f : E →ₗ[𝕜] β) {s : Set E} (hs : Convex 𝕜 s) :

ConcaveOn 𝕜 s ⇑f

A linear map is concave.

theorem StrictConvexOn.convexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) :

ConvexOn 𝕜 s f

theorem StrictConcaveOn.concaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) :

ConcaveOn 𝕜 s f

theorem StrictConvexOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ f x < r}

theorem StrictConcaveOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ r < f x}

theorem LinearOrder.convexOn_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) :

ConvexOn 𝕜 s f

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 convex, it suffices to verify the inequality f (a • x + b • y) ≤ a • f x + b • f y only 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 LinearOrder.concaveOn_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, 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

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 LinearOrder.strictConvexOn_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y) :

StrictConvexOn 𝕜 s f

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 strictly convex, it suffices to verify the inequality f (a • x + b • y) < a • f x + b • f 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 LinearOrder.strictConcaveOn_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)) :

StrictConcaveOn 𝕜 s f

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 strictly 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 ConvexOn.comp_linearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} {s : Set F} (hf : ConvexOn 𝕜 s f) (g : E →ₗ[𝕜] F) :

ConvexOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If g is convex on s, so is (f ∘ g) on f ⁻¹' s for a linear f.

theorem ConcaveOn.comp_linearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} {s : Set F} (hf : ConcaveOn 𝕜 s f) (g : E →ₗ[𝕜] F) :

ConcaveOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If g is concave on s, so is (g ∘ f) on f ⁻¹' s for a linear f.

theorem StrictConvexOn.add_convexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) :

StrictConvexOn 𝕜 s (f + g)

theorem ConvexOn.add_strictConvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConvexOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) :

StrictConvexOn 𝕜 s (f + g)

theorem StrictConvexOn.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConvexOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) :

StrictConvexOn 𝕜 s (f + g)

theorem StrictConcaveOn.add_concaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) :

StrictConcaveOn 𝕜 s (f + g)

theorem ConcaveOn.add_strictConcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConcaveOn 𝕜 s f) (hg : StrictConcaveOn 𝕜 s g) :

StrictConcaveOn 𝕜 s (f + g)

theorem StrictConcaveOn.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [SMul 𝕜 E] [DistribMulAction 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConcaveOn 𝕜 s f) (hg : StrictConcaveOn 𝕜 s g) :

StrictConcaveOn 𝕜 s (f + g)

theorem StrictConvexOn.add_const {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {γ : Type u_7} {f : E → γ} [OrderedCancelAddCommMonoid γ] [Module 𝕜 γ] (hf : StrictConvexOn 𝕜 s f) (b : γ) :

StrictConvexOn 𝕜 s (f + fun (x : E) => b)

theorem StrictConcaveOn.add_const {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {γ : Type u_7} {f : E → γ} [OrderedCancelAddCommMonoid γ] [Module 𝕜 γ] (hf : StrictConcaveOn 𝕜 s f) (b : γ) :

StrictConcaveOn 𝕜 s (f + fun (x : E) => b)

theorem ConvexOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ f x < r}

theorem ConcaveOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ r < f x}

theorem ConvexOn.openSegment_subset_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) (p : E × β) (q : E × β) (hp : p.1 ∈ s ∧ f p.1 < p.2) (hq : q.1 ∈ s ∧ f q.1 ≤ q.2) :

openSegment 𝕜 p q ⊆ {p : E × β | p.1 ∈ s ∧ f p.1 < p.2}

theorem ConcaveOn.openSegment_subset_strict_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) (p : E × β) (q : E × β) (hp : p.1 ∈ s ∧ p.2 < f p.1) (hq : q.1 ∈ s ∧ q.2 ≤ f q.1) :

openSegment 𝕜 p q ⊆ {p : E × β | p.1 ∈ s ∧ p.2 < f p.1}

theorem ConvexOn.convex_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) :

Convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 < p.2}

theorem ConcaveOn.convex_strict_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) :

Convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 < f p.1}

theorem ConvexOn.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) :

ConvexOn 𝕜 s (f ⊔ g)

The pointwise maximum of convex functions is convex.

theorem ConcaveOn.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) :

ConcaveOn 𝕜 s (f ⊓ g)

The pointwise minimum of concave functions is concave.

theorem StrictConvexOn.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConvexOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) :

StrictConvexOn 𝕜 s (f ⊔ g)

The pointwise maximum of strictly convex functions is strictly convex.

theorem StrictConcaveOn.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConcaveOn 𝕜 s f) (hg : StrictConcaveOn 𝕜 s g) :

StrictConcaveOn 𝕜 s (f ⊓ g)

The pointwise minimum of strictly concave functions is strictly concave.

theorem ConvexOn.le_on_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {a : 𝕜} {b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

f (a • x + b • y) ≤ max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

theorem ConcaveOn.ge_on_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {a : 𝕜} {b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

min (f x) (f y) ≤ f (a • x + b • y)

A concave function on a segment is lower-bounded by the min of its endpoints.

theorem ConvexOn.le_on_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ segment 𝕜 x y) :

f z ≤ max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

theorem ConcaveOn.ge_on_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ segment 𝕜 x y) :

min (f x) (f y) ≤ f z

A concave function on a segment is lower-bounded by the min of its endpoints.

theorem StrictConvexOn.lt_on_open_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

f (a • x + b • y) < max (f x) (f y)

A strictly convex function on an open segment is strictly upper-bounded by the max of its endpoints.

theorem StrictConcaveOn.lt_on_open_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

min (f x) (f y) < f (a • x + b • y)

A strictly concave function on an open segment is strictly lower-bounded by the min of its endpoints.

theorem StrictConvexOn.lt_on_openSegment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) (hz : z ∈ openSegment 𝕜 x y) :

f z < max (f x) (f y)

A strictly convex function on an open segment is strictly upper-bounded by the max of its endpoints.

theorem StrictConcaveOn.lt_on_openSegment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) (hz : z ∈ openSegment 𝕜 x y) :

min (f x) (f y) < f z

A strictly concave function on an open segment is strictly lower-bounded by the min of its endpoints.

theorem ConvexOn.le_left_of_right_le' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hfy : f y ≤ f (a • x + b • y)) :

f (a • x + b • y) ≤ f x

theorem ConcaveOn.left_le_of_le_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hfy : f (a • x + b • y) ≤ f y) :

f x ≤ f (a • x + b • y)

theorem ConvexOn.le_right_of_left_le' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} {a : 𝕜} {b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x ≤ f (a • x + b • y)) :

f (a • x + b • y) ≤ f y

theorem ConcaveOn.right_le_of_le_left' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} {a : 𝕜} {b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hfx : f (a • x + b • y) ≤ f x) :

f y ≤ f (a • x + b • y)

theorem ConvexOn.le_left_of_right_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hyz : f y ≤ f z) :

f z ≤ f x

theorem ConcaveOn.left_le_of_le_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hyz : f z ≤ f y) :

f x ≤ f z

theorem ConvexOn.le_right_of_left_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hxz : f x ≤ f z) :

f z ≤ f y

theorem ConcaveOn.right_le_of_le_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hxz : f z ≤ f x) :

f y ≤ f z

theorem ConvexOn.lt_left_of_right_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfy : f y < f (a • x + b • y)) :

f (a • x + b • y) < f x

theorem ConcaveOn.left_lt_of_lt_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfy : f (a • x + b • y) < f y) :

f x < f (a • x + b • y)

theorem ConvexOn.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} {a : 𝕜} {b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x < f (a • x + b • y)) :

f (a • x + b • y) < f y

theorem ConcaveOn.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} {a : 𝕜} {b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfx : f (a • x + b • y) < f x) :

f y < f (a • x + b • y)

theorem ConvexOn.lt_left_of_right_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hyz : f y < f z) :

f z < f x

theorem ConcaveOn.left_lt_of_lt_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hyz : f z < f y) :

f x < f z

theorem ConvexOn.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hxz : f x < f z) :

f z < f y

theorem ConcaveOn.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) {x : E} {y : E} {z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y) (hxz : f z < f x) :

f y < f z

@[simp]

theorem neg_convexOn_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f

A function -f is convex iff f is concave.

@[simp]

theorem neg_concaveOn_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f

A function -f is concave iff f is convex.

@[simp]

theorem neg_strictConvexOn_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f

A function -f is strictly convex iff f is strictly concave.

@[simp]

theorem neg_strictConcaveOn_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f

A function -f is strictly concave iff f is strictly convex.

theorem ConcaveOn.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (-f)

Alias of the reverse direction of neg_convexOn_iff.

A function -f is convex iff f is concave.

theorem ConvexOn.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

ConvexOn 𝕜 s f → ConcaveOn 𝕜 s (-f)

Alias of the reverse direction of neg_concaveOn_iff.

A function -f is concave iff f is convex.

theorem StrictConcaveOn.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

StrictConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s (-f)

Alias of the reverse direction of neg_strictConvexOn_iff.

A function -f is strictly convex iff f is strictly concave.

theorem StrictConvexOn.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} :

StrictConvexOn 𝕜 s f → StrictConcaveOn 𝕜 s (-f)

Alias of the reverse direction of neg_strictConcaveOn_iff.

A function -f is strictly concave iff f is strictly convex.

theorem ConvexOn.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) :

ConvexOn 𝕜 s (f - g)

theorem ConcaveOn.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) :

ConcaveOn 𝕜 s (f - g)

theorem StrictConvexOn.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConvexOn 𝕜 s f) (hg : StrictConcaveOn 𝕜 s g) :

StrictConvexOn 𝕜 s (f - g)

theorem StrictConcaveOn.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConcaveOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) :

StrictConcaveOn 𝕜 s (f - g)

theorem ConvexOn.sub_strictConcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConvexOn 𝕜 s f) (hg : StrictConcaveOn 𝕜 s g) :

StrictConvexOn 𝕜 s (f - g)

theorem ConcaveOn.sub_strictConvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : ConcaveOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) :

StrictConcaveOn 𝕜 s (f - g)

theorem StrictConvexOn.sub_concaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) :

StrictConvexOn 𝕜 s (f - g)

theorem StrictConcaveOn.sub_convexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommGroup β] [SMul 𝕜 E] [Module 𝕜 β] {s : Set E} {f : E → β} {g : E → β} (hf : StrictConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) :

StrictConcaveOn 𝕜 s (f - g)

theorem StrictConvexOn.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCancelCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) (c : E) :

StrictConvexOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => c + z)

Right translation preserves strict convexity.

theorem StrictConcaveOn.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCancelCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) (c : E) :

StrictConcaveOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => c + z)

Right translation preserves strict concavity.

theorem StrictConvexOn.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCancelCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConvexOn 𝕜 s f) (c : E) :

StrictConvexOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => z + c)

Left translation preserves strict convexity.

theorem StrictConcaveOn.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedSemiring 𝕜] [AddCancelCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) (c : E) :

StrictConcaveOn 𝕜 ((fun (z : E) => c + z) ⁻¹' s) (f ∘ fun (z : E) => z + c)

Left translation preserves strict concavity.

theorem ConvexOn.smul {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {c : 𝕜} (hc : 0 ≤ c) (hf : ConvexOn 𝕜 s f) :

ConvexOn 𝕜 s fun (x : E) => c • f x

theorem ConcaveOn.smul {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {c : 𝕜} (hc : 0 ≤ c) (hf : ConcaveOn 𝕜 s f) :

ConcaveOn 𝕜 s fun (x : E) => c • f x

theorem ConvexOn.comp_affineMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [AddCommGroup F] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : Set F} (hf : ConvexOn 𝕜 s f) :

ConvexOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If a function is convex on s, it remains convex when precomposed by an affine map.

theorem ConcaveOn.comp_affineMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [AddCommGroup F] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : Set F} (hf : ConcaveOn 𝕜 s f) :

ConcaveOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If a function is concave on s, it remains concave when precomposed by an affine map.

theorem convexOn_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [LinearOrderedField 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} :

ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y

theorem concaveOn_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [LinearOrderedField 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} :

ConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y)

theorem strictConvexOn_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [LinearOrderedField 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} :

StrictConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y

theorem strictConcaveOn_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [LinearOrderedField 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [SMul 𝕜 E] [SMul 𝕜 β] {s : Set E} {f : E → β} :

StrictConcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • f x + (b / (a + b)) • f y < f ((a / (a + b)) • x + (b / (a + b)) • y)

theorem OrderIso.strictConvexOn_symm {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [OrderedAddCommMonoid α] [SMul 𝕜 α] [OrderedAddCommMonoid β] [SMul 𝕜 β] (f : α ≃o β) (hf : StrictConcaveOn 𝕜 Set.univ ⇑f) :

StrictConvexOn 𝕜 Set.univ ⇑f.symm

theorem OrderIso.convexOn_symm {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [OrderedAddCommMonoid α] [SMul 𝕜 α] [OrderedAddCommMonoid β] [SMul 𝕜 β] (f : α ≃o β) (hf : ConcaveOn 𝕜 Set.univ ⇑f) :

ConvexOn 𝕜 Set.univ ⇑f.symm

theorem OrderIso.strictConcaveOn_symm {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [OrderedAddCommMonoid α] [SMul 𝕜 α] [OrderedAddCommMonoid β] [SMul 𝕜 β] (f : α ≃o β) (hf : StrictConvexOn 𝕜 Set.univ ⇑f) :

StrictConcaveOn 𝕜 Set.univ ⇑f.symm

theorem OrderIso.concaveOn_symm {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [OrderedSemiring 𝕜] [OrderedAddCommMonoid α] [SMul 𝕜 α] [OrderedAddCommMonoid β] [SMul 𝕜 β] (f : α ≃o β) (hf : ConvexOn 𝕜 Set.univ ⇑f) :

ConcaveOn 𝕜 Set.univ ⇑f.symm

theorem StrictConvexOn.eq_of_isMinOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [LinearOrderedField 𝕜] [OrderedAddCommMonoid β] [AddCommMonoid E] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} {s : Set E} {x : E} {y : E} (hf : StrictConvexOn 𝕜 s f) (hfx : IsMinOn f s x) (hfy : IsMinOn f s y) (hx : x ∈ s) (hy : y ∈ s) :

x = y

A strictly convex function admits at most one global minimum.

theorem StrictConcaveOn.eq_of_isMaxOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [LinearOrderedField 𝕜] [OrderedAddCommMonoid β] [AddCommMonoid E] [SMul 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} {s : Set E} {x : E} {y : E} (hf : StrictConcaveOn 𝕜 s f) (hfx : IsMaxOn f s x) (hfy : IsMaxOn f s y) (hx : x ∈ s) (hy : y ∈ s) :

x = y

A strictly concave function admits at most one global maximum.

theorem ConvexOn.le_right_of_left_le'' {𝕜 : Type u_1} {β : Type u_5} [LinearOrderedField 𝕜] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {x : 𝕜} {y : 𝕜} {z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β} (hf : ConvexOn 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y ≤ z) (h : f x ≤ f y) :

f y ≤ f z

theorem ConvexOn.le_left_of_right_le'' {𝕜 : Type u_1} {β : Type u_5} [LinearOrderedField 𝕜] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {x : 𝕜} {y : 𝕜} {z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β} (hf : ConvexOn 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x ≤ y) (hyz : y < z) (h : f z ≤ f y) :

f y ≤ f x

theorem ConcaveOn.right_le_of_le_left'' {𝕜 : Type u_1} {β : Type u_5} [LinearOrderedField 𝕜] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {x : 𝕜} {y : 𝕜} {z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β} (hf : ConcaveOn 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y ≤ z) (h : f y ≤ f x) :

f z ≤ f y

theorem ConcaveOn.left_le_of_le_right'' {𝕜 : Type u_1} {β : Type u_5} [LinearOrderedField 𝕜] [LinearOrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {x : 𝕜} {y : 𝕜} {z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β} (hf : ConcaveOn 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x ≤ y) (hyz : y < z) (h : f y ≤ f z) :

f x ≤ f y