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 #

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
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
    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
      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
        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.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_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 โˆง Set.Pairwise s 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 โˆง Set.Pairwise s 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 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 โ‡‘(OrderIso.symm f)
          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 โ‡‘(OrderIso.symm f)
          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 โ‡‘(OrderIso.symm f)
          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 โ‡‘(OrderIso.symm f)
          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