# 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 ๐] [] [] [SMul ๐ E] [SMul ๐ ฮฒ] (s : Set E) (f : E โ ฮฒ) :

Convexity of functions

Equations
Instances For
def ConcaveOn (๐ : Type u_1) {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [SMul ๐ E] [SMul ๐ ฮฒ] (s : Set E) (f : E โ ฮฒ) :

Concavity of functions

Equations
Instances For
def StrictConvexOn (๐ : Type u_1) {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [SMul ๐ E] [SMul ๐ ฮฒ] (s : Set E) (f : E โ ฮฒ) :

Strict convexity of functions

Equations
Instances For
def StrictConcaveOn (๐ : Type u_1) {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [SMul ๐ E] [SMul ๐ ฮฒ] (s : Set E) (f : E โ ฮฒ) :

Strict concavity of functions

Equations
Instances For
theorem ConvexOn.dual {๐ : Type u_1} {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [SMul ๐ ฮฒ] {s : Set ฮฒ} (hs : Convex ๐ s) :
ConvexOn ๐ s id
theorem concaveOn_id {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [SMul ๐ ฮฒ] {s : Set ฮฒ} (hs : Convex ๐ s) :
ConcaveOn ๐ s id
theorem ConvexOn.subset {๐ : Type u_1} {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [] [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 ๐] [] [] [] [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 ๐] [] [] [] [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 ๐] [] [] [] [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 ๐] [] [] [] [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' : ) :
StrictConvexOn ๐ s (g โ f)
theorem StrictConcaveOn.comp {๐ : Type u_1} {E : Type u_2} {ฮฑ : Type u_4} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [] [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' : ) :
StrictConcaveOn ๐ s (g โ f)
theorem StrictConvexOn.comp_strictConcaveOn {๐ : Type u_1} {E : Type u_2} {ฮฑ : Type u_4} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [] [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' : ) :
StrictConvexOn ๐ s (g โ f)
theorem StrictConcaveOn.comp_strictConvexOn {๐ : Type u_1} {E : Type u_2} {ฮฑ : Type u_4} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [] [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' : ) :
StrictConcaveOn ๐ s (g โ f)
theorem ConvexOn.add {๐ : Type u_1} {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [SMul ๐ E] [Module ๐ ฮฒ] {s : Set E} (c : ฮฒ) (hs : Convex ๐ s) :
ConcaveOn ๐ s fun (x : E) => c
theorem convexOn_of_convex_epigraph {๐ : Type u_1} {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [Module ๐ E] [Module ๐ ฮฒ] [] {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 ๐] [] [] [Module ๐ E] [Module ๐ ฮฒ] [] {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 ๐] [] [] [Module ๐ E] [Module ๐ ฮฒ] [] {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 ๐] [] [] [Module ๐ E] [Module ๐ ฮฒ] [] {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 ๐] [] [] [] [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 ๐] [] [] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [SMul ๐ E] [DistribMulAction ๐ ฮฒ] {s : Set E} {f : E โ ฮฒ} {g : E โ ฮฒ} (hf : StrictConcaveOn ๐ s f) (hg : StrictConcaveOn ๐ s g) :
StrictConcaveOn ๐ s (f + g)
theorem ConvexOn.convex_lt {๐ : Type u_1} {E : Type u_2} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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} [] [] [] [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} [] [] [] [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} [] [] [] [] [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} [] [] [] [] [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} [] [] [] [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} [] [] [] [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} [] [] [] [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} [] [] [] [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 ๐] [] [SMul ๐ ฮฑ] [] [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 ๐] [] [SMul ๐ ฮฑ] [] [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 ๐] [] [SMul ๐ ฮฑ] [] [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 ๐] [] [SMul ๐ ฮฑ] [] [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} [] [] [] [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} [] [] [] [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} [] [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} [] [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} [] [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} [] [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