doc-next-gen

Mathlib.Analysis.Convex.Function

Module docstring

{"# 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 π•œ. "}
ConvexOn definition
: Prop
Full source 
/-- Convexity of functions -/
def ConvexOn : Prop :=
  ConvexConvex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ βˆ€ ⦃a b : π•œβ¦„, 0 ≀ a β†’ 0 ≀ b β†’ a + b = 1 β†’
    f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y
Convex function on a convex set
Informal description
A function $f : E \to \beta$ is called convex on a set $s$ with respect to scalars $\mathbb{K}$ if $s$ is a convex set and for any two points $x, y \in s$ and any non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the following inequality holds: \[ f(a \cdot x + b \cdot y) \leq a \cdot f(x) + b \cdot f(y). \] This means that the segment joining $(x, f(x))$ to $(y, f(y))$ lies above the graph of $f$ over $s$.
ConcaveOn definition
: Prop
Full source 
/-- Concavity of functions -/
def ConcaveOn : Prop :=
  ConvexConvex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ βˆ€ ⦃a b : π•œβ¦„, 0 ≀ a β†’ 0 ≀ b β†’ a + b = 1 β†’
    a β€’ f x + b β€’ f y ≀ f (a β€’ x + b β€’ y)
Concave function on a convex set
Informal description
A function $f : E \to \beta$ is called concave on a set $s$ with respect to scalars $\mathbb{K}$ if $s$ is a convex set and for any two points $x, y \in s$ and any non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the following inequality holds: \[ a \cdot f(x) + b \cdot f(y) \leq f(a \cdot x + b \cdot y). \] This means that the segment joining $(x, f(x))$ to $(y, f(y))$ lies below the graph of $f$ over $s$.
StrictConvexOn definition
: Prop
Full source 
/-- Strict convexity of functions -/
def StrictConvexOn : Prop :=
  ConvexConvex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ x β‰  y β†’ βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’
    f (a β€’ x + b β€’ y) < a β€’ f x + b β€’ f y
Strictly convex function on a convex set
Informal description
A function \( f : E \to \beta \) is called strictly convex on a convex set \( s \) with respect to scalars \( \mathbb{K} \) if \( s \) is a convex set and for any two distinct points \( x, y \in s \) and any positive scalars \( a, b \in \mathbb{K} \) with \( a + b = 1 \), the following strict inequality holds: \[ f(a \cdot x + b \cdot y) < a \cdot f(x) + b \cdot f(y). \] This means that the segment joining \((x, f(x))\) to \((y, f(y))\) lies strictly above the graph of \( f \) over \( s \).
StrictConcaveOn definition
: Prop
Full source 
/-- Strict concavity of functions -/
def StrictConcaveOn : Prop :=
  ConvexConvex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ x β‰  y β†’ βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’
    a β€’ f x + b β€’ f y < f (a β€’ x + b β€’ y)
Strictly concave function on a convex set
Informal description
A function \( f : E \to \beta \) is called strictly concave on a convex set \( s \) with respect to scalars \( \mathbb{K} \) if for any two distinct points \( x, y \in s \) and any positive scalars \( a, b \in \mathbb{K} \) with \( a + b = 1 \), the following strict inequality holds: \[ a \cdot f(x) + b \cdot f(y) < f(a \cdot x + b \cdot y). \] This means that the segment joining \((x, f(x))\) to \((y, f(y))\) lies strictly below the graph of \( f \) over \( s \).
ConvexOn.dual theorem
(hf : ConvexOn π•œ s f) : ConcaveOn π•œ s (toDual ∘ f)
Full source 
theorem ConvexOn.dual (hf : ConvexOn π•œ s f) : ConcaveOn π•œ s (toDualtoDual ∘ f) := hf
Dual of Convex Function is Concave
Informal description
If a function $f : E \to \beta$ is convex on a convex set $s$ with respect to scalars $\mathbb{K}$, then the composition of $f$ with the order dual map $\text{toDual} : \beta \to \beta^{\text{op}}$ is concave on $s$ with respect to $\mathbb{K}$.
ConcaveOn.dual theorem
(hf : ConcaveOn π•œ s f) : ConvexOn π•œ s (toDual ∘ f)
Full source 
theorem ConcaveOn.dual (hf : ConcaveOn π•œ s f) : ConvexOn π•œ s (toDualtoDual ∘ f) := hf
Convexity of Dual Composition of Concave Function
Informal description
If a function $f : E \to \beta$ is concave on a convex set $s$ with respect to scalars $\mathbb{K}$, then the composition of $f$ with the order dual map $\text{toDual} : \beta \to \beta^{\text{op}}$ is convex on $s$ with respect to $\mathbb{K}$.
StrictConvexOn.dual theorem
(hf : StrictConvexOn π•œ s f) : StrictConcaveOn π•œ s (toDual ∘ f)
Full source 
theorem StrictConvexOn.dual (hf : StrictConvexOn π•œ s f) : StrictConcaveOn π•œ s (toDualtoDual ∘ f) := hf
Dual of Strictly Convex Function is Strictly Concave
Informal description
If a function $f : E \to \beta$ is strictly convex on a convex set $s$ with respect to scalars $\mathbb{K}$, then the composition $(\text{toDual} \circ f) : E \to \beta^{\text{op}}$ is strictly concave on $s$ with respect to $\mathbb{K}$.
StrictConcaveOn.dual theorem
(hf : StrictConcaveOn π•œ s f) : StrictConvexOn π•œ s (toDual ∘ f)
Full source 
theorem StrictConcaveOn.dual (hf : StrictConcaveOn π•œ s f) : StrictConvexOn π•œ s (toDualtoDual ∘ f) := hf
Dual of Strictly Concave Function is Strictly Convex
Informal description
If a function \( f \) is strictly concave on a convex set \( s \) with respect to scalars \( \mathbb{K} \), then the composition of \( f \) with the order dual map \( \text{toDual} \) is strictly convex on \( s \) with respect to \( \mathbb{K} \).
convexOn_id theorem
{s : Set Ξ²} (hs : Convex π•œ s) : ConvexOn π•œ s _root_.id
Full source 
theorem convexOn_id {s : Set Ξ²} (hs : Convex π•œ s) : ConvexOn π•œ s _root_.id :=
  ⟨hs, by
    intros
    rfl⟩
Convexity of the Identity Function on a Convex Set
Informal description
For any convex set $s$ in a vector space $\beta$ over a scalar field $\mathbb{K}$, the identity function $\mathrm{id} : \beta \to \beta$ is convex on $s$.
concaveOn_id theorem
{s : Set Ξ²} (hs : Convex π•œ s) : ConcaveOn π•œ s _root_.id
Full source 
theorem concaveOn_id {s : Set Ξ²} (hs : Convex π•œ s) : ConcaveOn π•œ s _root_.id :=
  ⟨hs, by
    intros
    rfl⟩
Concavity of the Identity Function on a Convex Set
Informal description
For any convex set $s$ in a vector space $\beta$ over a scalar field $\mathbb{K}$, the identity function $\mathrm{id} : \beta \to \beta$ is concave on $s$. This means that for any two points $x, y \in s$ and any non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, we have: \[ a \cdot \mathrm{id}(x) + b \cdot \mathrm{id}(y) \leq \mathrm{id}(a \cdot x + b \cdot y). \]
ConvexOn.congr theorem
(hf : ConvexOn π•œ s f) (hfg : EqOn f g s) : ConvexOn π•œ s g
Full source 
theorem ConvexOn.congr (hf : ConvexOn π•œ s f) (hfg : EqOn f g s) : ConvexOn π•œ s g :=
  ⟨hf.1, fun x hx y hy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab⟩
Preservation of Convexity Under Pointwise Equality
Informal description
Let $f, g : E \to \beta$ be functions defined on a vector space $E$ with values in $\beta$, and let $s \subseteq E$ be a convex set with respect to scalars $\mathbb{K}$. If $f$ is convex on $s$ and $f(x) = g(x)$ for all $x \in s$, then $g$ is also convex on $s$.
ConcaveOn.congr theorem
(hf : ConcaveOn π•œ s f) (hfg : EqOn f g s) : ConcaveOn π•œ s g
Full source 
theorem ConcaveOn.congr (hf : ConcaveOn π•œ s f) (hfg : EqOn f g s) : ConcaveOn π•œ s g :=
  ⟨hf.1, fun x hx y hy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab⟩
Preservation of Concavity Under Pointwise Equality
Informal description
Let $f, g : E \to \beta$ be functions and $s \subseteq E$ be a convex set. If $f$ is concave on $s$ with respect to scalars $\mathbb{K}$ and $f(x) = g(x)$ for all $x \in s$, then $g$ is also concave on $s$ with respect to $\mathbb{K}$.
StrictConvexOn.congr theorem
(hf : StrictConvexOn π•œ s f) (hfg : EqOn f g s) : StrictConvexOn π•œ s g
Full source 
theorem StrictConvexOn.congr (hf : StrictConvexOn π•œ s f) (hfg : EqOn f g s) :
    StrictConvexOn π•œ s g :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab⟩
Preservation of Strict Convexity Under Pointwise Equality
Informal description
Let $f, g : E \to \beta$ be functions and $s \subseteq E$ be a convex set. If $f$ is strictly convex on $s$ with respect to scalars $\mathbb{K}$ and $f(x) = g(x)$ for all $x \in s$, then $g$ is also strictly convex on $s$ with respect to $\mathbb{K}$.
StrictConcaveOn.congr theorem
(hf : StrictConcaveOn π•œ s f) (hfg : EqOn f g s) : StrictConcaveOn π•œ s g
Full source 
theorem StrictConcaveOn.congr (hf : StrictConcaveOn π•œ s f) (hfg : EqOn f g s) :
    StrictConcaveOn π•œ s g :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab⟩
Preservation of Strict Concavity Under Pointwise Equality
Informal description
Let $f, g : E \to \beta$ be functions and $s \subseteq E$ be a convex set. If $f$ is strictly concave on $s$ with respect to scalars $\mathbb{K}$ and $f(x) = g(x)$ for all $x \in s$, then $g$ is also strictly concave on $s$ with respect to $\mathbb{K}$.
ConvexOn.subset theorem
{t : Set E} (hf : ConvexOn π•œ t f) (hst : s βŠ† t) (hs : Convex π•œ s) : ConvexOn π•œ s f
Full source 
theorem ConvexOn.subset {t : Set E} (hf : ConvexOn π•œ t f) (hst : s βŠ† t) (hs : Convex π•œ s) :
    ConvexOn π•œ s f :=
  ⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩
Convexity is Preserved Under Subset Restriction
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, and let $s, t \subseteq E$ be sets with $s \subseteq t$. If $f : E \to \beta$ is a convex function on $t$ and $s$ is a convex set, then $f$ is also convex on $s$.
ConcaveOn.subset theorem
{t : Set E} (hf : ConcaveOn π•œ t f) (hst : s βŠ† t) (hs : Convex π•œ s) : ConcaveOn π•œ s f
Full source 
theorem ConcaveOn.subset {t : Set E} (hf : ConcaveOn π•œ t f) (hst : s βŠ† t) (hs : Convex π•œ s) :
    ConcaveOn π•œ s f :=
  ⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩
Restriction of Concave Function to Convex Subset Preserves Concavity
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, $s$ and $t$ be subsets of $E$ with $s \subseteq t$, and $f : E \to \beta$ be a function. If $f$ is concave on $t$ with respect to $\mathbb{K}$ and $s$ is convex, then $f$ is concave on $s$ with respect to $\mathbb{K}$.
StrictConvexOn.subset theorem
{t : Set E} (hf : StrictConvexOn π•œ t f) (hst : s βŠ† t) (hs : Convex π•œ s) : StrictConvexOn π•œ s f
Full source 
theorem StrictConvexOn.subset {t : Set E} (hf : StrictConvexOn π•œ t f) (hst : s βŠ† t)
    (hs : Convex π•œ s) : StrictConvexOn π•œ s f :=
  ⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩
Strict Convexity is Preserved Under Subset Restriction
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, and let $s, t \subseteq E$ be sets with $s \subseteq t$. If $f : E \to \beta$ is a strictly convex function on $t$ and $s$ is a convex set, then $f$ is strictly convex on $s$.
StrictConcaveOn.subset theorem
{t : Set E} (hf : StrictConcaveOn π•œ t f) (hst : s βŠ† t) (hs : Convex π•œ s) : StrictConcaveOn π•œ s f
Full source 
theorem StrictConcaveOn.subset {t : Set E} (hf : StrictConcaveOn π•œ t f) (hst : s βŠ† t)
    (hs : Convex π•œ s) : StrictConcaveOn π•œ s f :=
  ⟨hs, fun _ hx _ hy => hf.2 (hst hx) (hst hy)⟩
Restriction of Strictly Concave Function to Convex Subset Preserves Strict Concavity
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, $s$ and $t$ be subsets of $E$ with $s \subseteq t$, and $f : E \to \beta$ be a function. If $f$ is strictly concave on $t$ with respect to $\mathbb{K}$ and $s$ is convex, then $f$ is strictly concave on $s$ with respect to $\mathbb{K}$.
ConvexOn.comp theorem
(hg : ConvexOn π•œ (f '' s) g) (hf : ConvexOn π•œ s f) (hg' : MonotoneOn g (f '' s)) : ConvexOn π•œ s (g ∘ f)
Full source 
theorem ConvexOn.comp (hg : ConvexOn π•œ (f '' s) g) (hf : ConvexOn π•œ s f)
    (hg' : MonotoneOn g (f '' s)) : ConvexOn π•œ s (g ∘ f) :=
  ⟨hf.1, fun _ hx _ hy _ _ ha hb hab =>
    (hg' (mem_image_of_mem f <| hf.1 hx hy ha hb hab)
            (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab) <|
          hf.2 hx hy ha hb hab).trans <|
      hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab⟩
Convexity of Composition of Convex and Monotone Functions
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a convex function on $s$, and $g : \beta \to \gamma$ is a convex function on the image $f(s)$. If $g$ is monotone on $f(s)$, then the composition $g \circ f$ is convex on $s$.
ConcaveOn.comp theorem
(hg : ConcaveOn π•œ (f '' s) g) (hf : ConcaveOn π•œ s f) (hg' : MonotoneOn g (f '' s)) : ConcaveOn π•œ s (g ∘ f)
Full source 
theorem ConcaveOn.comp (hg : ConcaveOn π•œ (f '' s) g) (hf : ConcaveOn π•œ s f)
    (hg' : MonotoneOn g (f '' s)) : ConcaveOn π•œ s (g ∘ f) :=
  ⟨hf.1, fun _ hx _ hy _ _ ha hb hab =>
    (hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab).trans <|
      hg' (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha hb hab)
          (mem_image_of_mem f <| hf.1 hx hy ha hb hab) <|
        hf.2 hx hy ha hb hab⟩
Concavity of Composition of Concave and Monotone Functions
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a concave function on $s$, and $g : \beta \to \gamma$ is a concave function on the image $f(s)$. If $g$ is monotone on $f(s)$, then the composition $g \circ f$ is concave on $s$.
ConvexOn.comp_concaveOn theorem
(hg : ConvexOn π•œ (f '' s) g) (hf : ConcaveOn π•œ s f) (hg' : AntitoneOn g (f '' s)) : ConvexOn π•œ s (g ∘ f)
Full source 
theorem ConvexOn.comp_concaveOn (hg : ConvexOn π•œ (f '' s) g) (hf : ConcaveOn π•œ s f)
    (hg' : AntitoneOn g (f '' s)) : ConvexOn π•œ s (g ∘ f) :=
  hg.dual.comp hf hg'
Convexity of Composition of Convex and Antitone Functions with Concave Base
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a concave function on $s$, and $g : \beta \to \gamma$ is a convex function on the image $f(s)$. If $g$ is antitone (monotonically decreasing) on $f(s)$, then the composition $g \circ f$ is convex on $s$.
ConcaveOn.comp_convexOn theorem
(hg : ConcaveOn π•œ (f '' s) g) (hf : ConvexOn π•œ s f) (hg' : AntitoneOn g (f '' s)) : ConcaveOn π•œ s (g ∘ f)
Full source 
theorem ConcaveOn.comp_convexOn (hg : ConcaveOn π•œ (f '' s) g) (hf : ConvexOn π•œ s f)
    (hg' : AntitoneOn g (f '' s)) : ConcaveOn π•œ s (g ∘ f) :=
  hg.dual.comp hf hg'
Concavity of Composition of Convex and Antitone Functions
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a convex function on $s$, and $g : \beta \to \gamma$ is a concave function on the image $f(s)$. If $g$ is antitone (decreasing) on $f(s)$, then the composition $g \circ f$ is concave on $s$.
StrictConvexOn.comp theorem
(hg : StrictConvexOn π•œ (f '' s) g) (hf : StrictConvexOn π•œ s f) (hg' : StrictMonoOn g (f '' s)) (hf' : s.InjOn f) : StrictConvexOn π•œ s (g ∘ f)
Full source 
theorem StrictConvexOn.comp (hg : StrictConvexOn π•œ (f '' s) g) (hf : StrictConvexOn π•œ s f)
    (hg' : StrictMonoOn g (f '' s)) (hf' : s.InjOn f) : StrictConvexOn π•œ s (g ∘ f) :=
  ⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab =>
    (hg' (mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab)
            (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab) <|
          hf.2 hx hy hxy ha hb hab).trans <|
      hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab⟩
Strict Convexity of Composition under Strictly Increasing and Injective Conditions
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a strictly convex function on $s$, and $g : \beta \to \beta$ is a strictly convex function on the image $f(s)$. If $g$ is strictly monotone increasing on $f(s)$ and $f$ is injective on $s$, then the composition $g \circ f$ is strictly convex on $s$.
StrictConcaveOn.comp theorem
(hg : StrictConcaveOn π•œ (f '' s) g) (hf : StrictConcaveOn π•œ s f) (hg' : StrictMonoOn g (f '' s)) (hf' : s.InjOn f) : StrictConcaveOn π•œ s (g ∘ f)
Full source 
theorem StrictConcaveOn.comp (hg : StrictConcaveOn π•œ (f '' s) g) (hf : StrictConcaveOn π•œ s f)
    (hg' : StrictMonoOn g (f '' s)) (hf' : s.InjOn f) : StrictConcaveOn π•œ s (g ∘ f) :=
  ⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab =>
    (hg.2 (mem_image_of_mem f hx) (mem_image_of_mem f hy) (mt (hf' hx hy) hxy) ha hb hab).trans <|
      hg' (hg.1 (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab)
          (mem_image_of_mem f <| hf.1 hx hy ha.le hb.le hab) <|
        hf.2 hx hy hxy ha hb hab⟩
Strict Concavity of Composition of Strictly Concave and Strictly Increasing Functions
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a strictly concave function on $s$, and $g : \beta \to \beta$ is a strictly concave function on the image $f(s)$. If $g$ is strictly increasing on $f(s)$ and $f$ is injective on $s$, then the composition $g \circ f$ is strictly concave on $s$. That is, for any distinct $x, y \in s$ and any $a, b > 0$ with $a + b = 1$, \[ a \cdot (g \circ f)(x) + b \cdot (g \circ f)(y) < (g \circ f)(a \cdot x + b \cdot y). \]
StrictConvexOn.comp_strictConcaveOn theorem
(hg : StrictConvexOn π•œ (f '' s) g) (hf : StrictConcaveOn π•œ s f) (hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) : StrictConvexOn π•œ s (g ∘ f)
Full source 
theorem StrictConvexOn.comp_strictConcaveOn (hg : StrictConvexOn π•œ (f '' s) g)
    (hf : StrictConcaveOn π•œ s f) (hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) :
    StrictConvexOn π•œ s (g ∘ f) :=
  hg.dual.comp hf hg' hf'
Strict Convexity of Composition of Strictly Convex and Strictly Decreasing Functions
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a strictly concave function on $s$, and $g : \beta \to \beta$ is a strictly convex function on the image $f(s)$. If $g$ is strictly decreasing on $f(s)$ and $f$ is injective on $s$, then the composition $g \circ f$ is strictly convex on $s$. That is, for any distinct $x, y \in s$ and any $a, b > 0$ with $a + b = 1$, \[ (g \circ f)(a \cdot x + b \cdot y) < a \cdot (g \circ f)(x) + b \cdot (g \circ f)(y). \]
StrictConcaveOn.comp_strictConvexOn theorem
(hg : StrictConcaveOn π•œ (f '' s) g) (hf : StrictConvexOn π•œ s f) (hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) : StrictConcaveOn π•œ s (g ∘ f)
Full source 
theorem StrictConcaveOn.comp_strictConvexOn (hg : StrictConcaveOn π•œ (f '' s) g)
    (hf : StrictConvexOn π•œ s f) (hg' : StrictAntiOn g (f '' s)) (hf' : s.InjOn f) :
    StrictConcaveOn π•œ s (g ∘ f) :=
  hg.dual.comp hf hg' hf'
Strict Concavity of Composition of Strictly Convex and Strictly Decreasing Functions
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \beta$ is a strictly convex function on $s$, and $g : \beta \to \beta$ is a strictly concave function on the image $f(s)$. If $g$ is strictly decreasing on $f(s)$ and $f$ is injective on $s$, then the composition $g \circ f$ is strictly concave on $s$. That is, for any distinct $x, y \in s$ and any $a, b > 0$ with $a + b = 1$, \[ a \cdot (g \circ f)(x) + b \cdot (g \circ f)(y) > (g \circ f)(a \cdot x + b \cdot y). \]
ConvexOn.add theorem
(hf : ConvexOn π•œ s f) (hg : ConvexOn π•œ s g) : ConvexOn π•œ s (f + g)
Full source 
theorem ConvexOn.add (hf : ConvexOn π•œ s f) (hg : ConvexOn π•œ s g) : ConvexOn π•œ s (f + g) :=
  ⟨hf.1, fun x hx y hy a b ha hb hab =>
    calc
      f (a β€’ x + b β€’ y) + g (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y + (a β€’ g x + b β€’ g y) :=
        add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
      _ = a β€’ (f x + g x) + b β€’ (f y + g y) := by rw [smul_add, smul_add, add_add_add_comm]
      ⟩
Sum of Convex Functions is Convex
Informal description
Let $f$ and $g$ be convex functions defined on a convex set $s$ over a scalar field $\mathbb{K}$. Then the sum $f + g$ is also convex on $s$.
ConcaveOn.add theorem
(hf : ConcaveOn π•œ s f) (hg : ConcaveOn π•œ s g) : ConcaveOn π•œ s (f + g)
Full source 
theorem ConcaveOn.add (hf : ConcaveOn π•œ s f) (hg : ConcaveOn π•œ s g) : ConcaveOn π•œ s (f + g) :=
  hf.dual.add hg
Sum of Concave Functions is Concave
Informal description
Let $f$ and $g$ be concave functions defined on a convex set $s$ over a scalar field $\mathbb{K}$. Then the sum $f + g$ is also concave on $s$.
convexOn_const theorem
(c : Ξ²) (hs : Convex π•œ s) : ConvexOn π•œ s fun _ : E => c
Full source 
theorem convexOn_const (c : Ξ²) (hs : Convex π•œ s) : ConvexOn π•œ s fun _ : E => c :=
  ⟨hs, fun _ _ _ _ _ _ _ _ hab => (Convex.combo_self hab c).ge⟩
Convexity of Constant Functions on Convex Sets
Informal description
For any constant $c \in \beta$ and any convex set $s \subseteq E$ over a scalar field $\mathbb{K}$, the constant function $f(x) = c$ is convex on $s$.
concaveOn_const theorem
(c : Ξ²) (hs : Convex π•œ s) : ConcaveOn π•œ s fun _ => c
Full source 
theorem concaveOn_const (c : Ξ²) (hs : Convex π•œ s) : ConcaveOn π•œ s fun _ => c :=
  convexOn_const (Ξ² := Ξ²α΅’α΅ˆ) _ hs
Concavity of Constant Functions on Convex Sets
Informal description
For any constant $c \in \beta$ and any convex set $s \subseteq E$ over a scalar field $\mathbb{K}$, the constant function $f(x) = c$ is concave on $s$.
ConvexOn.add_const theorem
[IsOrderedAddMonoid Ξ²] (hf : ConvexOn π•œ s f) (b : Ξ²) : ConvexOn π•œ s (f + fun _ => b)
Full source 
theorem ConvexOn.add_const [IsOrderedAddMonoid Ξ²] (hf : ConvexOn π•œ s f) (b : Ξ²) :
    ConvexOn π•œ s (f + fun _ => b) :=
  hf.add (convexOn_const _ hf.1)
Convexity is preserved under addition of a constant
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$, where $\beta$ is an ordered additive monoid. Then for any constant $b \in \beta$, the function $f + b$ (defined pointwise as $(f + b)(x) = f(x) + b$) is also convex on $s$ with respect to $\mathbb{K}$.
ConcaveOn.add_const theorem
[IsOrderedAddMonoid Ξ²] (hf : ConcaveOn π•œ s f) (b : Ξ²) : ConcaveOn π•œ s (f + fun _ => b)
Full source 
theorem ConcaveOn.add_const [IsOrderedAddMonoid Ξ²] (hf : ConcaveOn π•œ s f) (b : Ξ²) :
    ConcaveOn π•œ s (f + fun _ => b) :=
  hf.add (concaveOn_const _ hf.1)
Concavity is preserved under addition of a constant
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$, where $\beta$ is an ordered additive monoid. Then for any constant $b \in \beta$, the function $f + b$ (defined pointwise as $(f + b)(x) = f(x) + b$) is also concave on $s$ with respect to $\mathbb{K}$.
convexOn_of_convex_epigraph theorem
(h : Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 ≀ p.2}) : ConvexOn π•œ s f
Full source 
theorem convexOn_of_convex_epigraph (h : Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 ≀ p.2 }) :
    ConvexOn π•œ s f :=
  ⟨fun x hx y hy a b ha hb hab => (@h (x, f x) ⟨hx, le_rfl⟩ (y, f y) ⟨hy, le_rfl⟩ a b ha hb hab).1,
    fun x hx y hy a b ha hb hab => (@h (x, f x) ⟨hx, le_rfl⟩ (y, f y) ⟨hy, le_rfl⟩ a b ha hb hab).2⟩
Convexity of Function via Convex Epigraph
Informal description
Given a function $f : E \to \beta$ and a set $s \subseteq E$, if the epigraph $\{(x, y) \in E \times \beta \mid x \in s \text{ and } f(x) \leq y\}$ is convex with respect to scalars $\mathbb{K}$, then $f$ is convex on $s$ with respect to $\mathbb{K}$.
concaveOn_of_convex_hypograph theorem
(h : Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 ≀ f p.1}) : ConcaveOn π•œ s f
Full source 
theorem concaveOn_of_convex_hypograph (h : Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 ≀ f p.1 }) :
    ConcaveOn π•œ s f :=
  convexOn_of_convex_epigraph (Ξ² := Ξ²α΅’α΅ˆ) h
Concavity of Function via Convex Hypograph
Informal description
Given a function $f : E \to \beta$ and a set $s \subseteq E$, if the hypograph $\{(x, y) \in E \times \beta \mid x \in s \text{ and } y \leq f(x)\}$ is convex with respect to scalars $\mathbb{K}$, then $f$ is concave on $s$ with respect to $\mathbb{K}$.
ConvexOn.convex_le theorem
(hf : ConvexOn π•œ s f) (r : Ξ²) : Convex π•œ ({x ∈ s | f x ≀ r})
Full source 
theorem ConvexOn.convex_le (hf : ConvexOn π•œ s f) (r : Ξ²) : Convex π•œ ({ x ∈ s | f x ≀ r }) :=
  fun x hx y hy a b ha hb hab =>
  ⟨hf.1 hx.1 hy.1 ha hb hab,
    calc
      f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := hf.2 hx.1 hy.1 ha hb hab
      _ ≀ a β€’ r + b β€’ r := by
        gcongr
        Β· exact hx.2
        Β· exact hy.2
      _ = r := Convex.combo_self hab r
      ⟩
Convexity of Sublevel Sets for Convex Functions
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $\beta$ be an ordered additive monoid. If $f : E \to \beta$ is a convex function on a convex set $s \subseteq E$, then for any $r \in \beta$, the sublevel set $\{x \in s \mid f(x) \leq r\}$ is convex in $E$.
ConcaveOn.convex_ge theorem
(hf : ConcaveOn π•œ s f) (r : Ξ²) : Convex π•œ ({x ∈ s | r ≀ f x})
Full source 
theorem ConcaveOn.convex_ge (hf : ConcaveOn π•œ s f) (r : Ξ²) : Convex π•œ ({ x ∈ s | r ≀ f x }) :=
  hf.dual.convex_le r
Convexity of Superlevel Sets for Concave Functions
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $\beta$ be an ordered additive monoid. If $f : E \to \beta$ is a concave function on a convex set $s \subseteq E$, then for any $r \in \beta$, the superlevel set $\{x \in s \mid r \leq f(x)\}$ is convex in $E$.
ConvexOn.convex_epigraph theorem
(hf : ConvexOn π•œ s f) : Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 ≀ p.2}
Full source 
theorem ConvexOn.convex_epigraph (hf : ConvexOn π•œ s f) :
    Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 ≀ p.2 } := by
  rintro ⟨x, r⟩ ⟨hx, hr⟩ ⟨y, t⟩ ⟨hy, ht⟩ a b ha hb hab
  refine ⟨hf.1 hx hy ha hb hab, ?_⟩
  calc
    f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := hf.2 hx hy ha hb hab
    _ ≀ a β€’ r + b β€’ t := by gcongr
Convexity of the Epigraph for Convex Functions
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$ and $\beta$ be an ordered additive monoid. For a convex function $f : E \to \beta$ defined on a convex set $s \subseteq E$, the epigraph $\{(x, y) \in E \times \beta \mid x \in s \text{ and } f(x) \leq y\}$ is a convex set in $E \times \beta$.
ConcaveOn.convex_hypograph theorem
(hf : ConcaveOn π•œ s f) : Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 ≀ f p.1}
Full source 
theorem ConcaveOn.convex_hypograph (hf : ConcaveOn π•œ s f) :
    Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 ≀ f p.1 } :=
  hf.dual.convex_epigraph
Convexity of the Hypograph for Concave Functions
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$ and $\beta$ be an ordered additive monoid. For a concave function $f : E \to \beta$ defined on a convex set $s \subseteq E$, the hypograph $\{(x, y) \in E \times \beta \mid x \in s \text{ and } y \leq f(x)\}$ is a convex set in $E \times \beta$.
convexOn_iff_convex_epigraph theorem
: ConvexOn π•œ s f ↔ Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 ≀ p.2}
Full source 
theorem convexOn_iff_convex_epigraph :
    ConvexOnConvexOn π•œ s f ↔ Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 ≀ p.2 } :=
  ⟨ConvexOn.convex_epigraph, convexOn_of_convex_epigraph⟩
Characterization of Convex Functions via Convex Epigraph
Informal description
A function $f : E \to \beta$ is convex on a set $s \subseteq E$ with respect to scalars $\mathbb{K}$ if and only if its epigraph $\{(x, y) \in E \times \beta \mid x \in s \text{ and } f(x) \leq y\}$ is a convex set in $E \times \beta$.
concaveOn_iff_convex_hypograph theorem
: ConcaveOn π•œ s f ↔ Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 ≀ f p.1}
Full source 
theorem concaveOn_iff_convex_hypograph :
    ConcaveOnConcaveOn π•œ s f ↔ Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 ≀ f p.1 } :=
  convexOn_iff_convex_epigraph (Ξ² := Ξ²α΅’α΅ˆ)
Characterization of Concave Functions via Convex Hypograph
Informal description
A function $f : E \to \beta$ is concave on a convex set $s \subseteq E$ with respect to scalars $\mathbb{K}$ if and only if its hypograph $\{(x, y) \in E \times \beta \mid x \in s \text{ and } y \leq f(x)\}$ is a convex set in $E \times \beta$.
ConvexOn.translate_right theorem
(hf : ConvexOn π•œ s f) (c : E) : ConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
Full source 
/-- Right translation preserves convexity. -/
theorem ConvexOn.translate_right (hf : ConvexOn π•œ s f) (c : E) :
    ConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
  ⟨hf.1.translate_preimage_right _, fun x hx y hy a b ha hb hab =>
    calc
      f (c + (a β€’ x + b β€’ y)) = f (a β€’ (c + x) + b β€’ (c + y)) := by
        rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]
      _ ≀ a β€’ f (c + x) + b β€’ f (c + y) := hf.2 hx hy ha hb hab
      ⟩
Convexity is preserved under right translation
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the right-translated function $f_c(z) := f(c + z)$ is convex on the preimage set $s_c := \{z \in E \mid c + z \in s\}$.
ConcaveOn.translate_right theorem
(hf : ConcaveOn π•œ s f) (c : E) : ConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
Full source 
/-- Right translation preserves concavity. -/
theorem ConcaveOn.translate_right (hf : ConcaveOn π•œ s f) (c : E) :
    ConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
  hf.dual.translate_right _
Right Translation Preserves Concavity
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the right-translated function $f_c(z) := f(c + z)$ is concave on the preimage set $s_c := \{z \in E \mid c + z \in s\}$.
ConvexOn.translate_left theorem
(hf : ConvexOn π•œ s f) (c : E) : ConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
Full source 
/-- Left translation preserves convexity. -/
theorem ConvexOn.translate_left (hf : ConvexOn π•œ s f) (c : E) :
    ConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c) := by
  simpa only [add_comm c] using hf.translate_right c
Convexity is preserved under left translation
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the left-translated function $f_c(z) := f(z + c)$ is convex on the preimage set $s_c := \{z \in E \mid z + c \in s\}$.
ConcaveOn.translate_left theorem
(hf : ConcaveOn π•œ s f) (c : E) : ConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
Full source 
/-- Left translation preserves concavity. -/
theorem ConcaveOn.translate_left (hf : ConcaveOn π•œ s f) (c : E) :
    ConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c) :=
  hf.dual.translate_left _
Left Translation Preserves Concavity
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the left-translated function $f_c(z) := f(z + c)$ is concave on the preimage set $s_c := \{z \in E \mid z + c \in s\}$.
convexOn_iff_forall_pos theorem
{s : Set E} {f : E β†’ Ξ²} : ConvexOn π•œ s f ↔ Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’ f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y
Full source 
theorem convexOn_iff_forall_pos {s : Set E} {f : E β†’ Ξ²} :
    ConvexOnConvexOn π•œ s f ↔ Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’
      a + b = 1 β†’ f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := by
  refine and_congr_right'
    ⟨fun h x hx y hy a b ha hb hab => h hx hy ha.le hb.le hab, fun h x hx y hy a b ha hb hab => ?_⟩
  obtain rfl | ha' := ha.eq_or_lt
  Β· rw [zero_add] at hab
    subst b
    simp_rw [zero_smul, zero_add, one_smul, le_rfl]
  obtain rfl | hb' := hb.eq_or_lt
  Β· rw [add_zero] at hab
    subst a
    simp_rw [zero_smul, add_zero, one_smul, le_rfl]
  exact h hx hy ha' hb' hab
Characterization of Convex Functions via Positive Weights
Informal description
A function $f : E \to \beta$ is convex on a set $s$ with respect to scalars $\mathbb{K}$ if and only if $s$ is a convex set and for any two points $x, y \in s$ and any positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the following inequality holds: \[ f(a \cdot x + b \cdot y) \leq a \cdot f(x) + b \cdot f(y). \]
concaveOn_iff_forall_pos theorem
{s : Set E} {f : E β†’ Ξ²} : ConcaveOn π•œ s f ↔ Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’ a β€’ f x + b β€’ f y ≀ f (a β€’ x + b β€’ y)
Full source 
theorem concaveOn_iff_forall_pos {s : Set E} {f : E β†’ Ξ²} :
    ConcaveOnConcaveOn π•œ s f ↔
      Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, y ∈ s β†’ βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’
        a β€’ f x + b β€’ f y ≀ f (a β€’ x + b β€’ y) :=
  convexOn_iff_forall_pos (Ξ² := Ξ²α΅’α΅ˆ)
Characterization of Concave Functions via Positive Weights
Informal description
A function $f : E \to \beta$ is concave on a convex set $s$ with respect to scalars $\mathbb{K}$ if and only if for any two points $x, y \in s$ and any positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the following inequality holds: \[ a \cdot f(x) + b \cdot f(y) \leq f(a \cdot x + b \cdot y). \]
convexOn_iff_pairwise_pos theorem
{s : Set E} {f : E β†’ Ξ²} : ConvexOn π•œ s f ↔ Convex π•œ s ∧ s.Pairwise fun x y => βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’ f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y
Full source 
theorem convexOn_iff_pairwise_pos {s : Set E} {f : E β†’ Ξ²} :
    ConvexOnConvexOn π•œ s f ↔
      Convex π•œ s ∧
        s.Pairwise fun x y =>
          βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’ f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := by
  rw [convexOn_iff_forall_pos]
  refine
    and_congr_right'
      ⟨fun h x hx y hy _ a b ha hb hab => h hx hy ha hb hab, fun h x hx y hy a b ha hb hab => ?_⟩
  obtain rfl | hxy := eq_or_ne x y
  Β· rw [Convex.combo_self hab, Convex.combo_self hab]
  exact h hx hy hxy ha hb hab
Characterization of Convex Functions via Pairwise Positive Weights
Informal description
A function $f : E \to \beta$ is convex on a set $s$ with respect to scalars $\mathbb{K}$ if and only if $s$ is a convex set and for any two distinct points $x, y \in s$ and any positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the following inequality holds: \[ f(a \cdot x + b \cdot y) \leq a \cdot f(x) + b \cdot f(y). \]
concaveOn_iff_pairwise_pos theorem
{s : Set E} {f : E β†’ Ξ²} : ConcaveOn π•œ s f ↔ Convex π•œ s ∧ s.Pairwise fun x y => βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’ a β€’ f x + b β€’ f y ≀ f (a β€’ x + b β€’ y)
Full source 
theorem concaveOn_iff_pairwise_pos {s : Set E} {f : E β†’ Ξ²} :
    ConcaveOnConcaveOn π•œ s f ↔
      Convex π•œ s ∧
        s.Pairwise fun x y =>
          βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’ a β€’ f x + b β€’ f y ≀ f (a β€’ x + b β€’ y) :=
  convexOn_iff_pairwise_pos (Ξ² := Ξ²α΅’α΅ˆ)
Characterization of Concave Functions via Pairwise Positive Weights
Informal description
A function $f : E \to \beta$ is concave on a set $s$ with respect to scalars $\mathbb{K}$ if and only if $s$ is a convex set and for any two distinct points $x, y \in s$ and any positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the following inequality holds: \[ a \cdot f(x) + b \cdot f(y) \leq f(a \cdot x + b \cdot y). \]
LinearMap.convexOn theorem
(f : E β†’β‚—[π•œ] Ξ²) {s : Set E} (hs : Convex π•œ s) : ConvexOn π•œ s f
Full source 
/-- A linear map is convex. -/
theorem LinearMap.convexOn (f : E β†’β‚—[π•œ] Ξ²) {s : Set E} (hs : Convex π•œ s) : ConvexOn π•œ s f :=
  ⟨hs, fun _ _ _ _ _ _ _ _ _ => by rw [f.map_add, f.map_smul, f.map_smul]⟩
Convexity of Linear Maps on Convex Sets
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $f : E \to \beta$ be a linear map. For any convex set $s \subseteq E$, the function $f$ is convex on $s$ with respect to $\mathbb{K}$.
LinearMap.concaveOn theorem
(f : E β†’β‚—[π•œ] Ξ²) {s : Set E} (hs : Convex π•œ s) : ConcaveOn π•œ s f
Full source 
/-- A linear map is concave. -/
theorem LinearMap.concaveOn (f : E β†’β‚—[π•œ] Ξ²) {s : Set E} (hs : Convex π•œ s) : ConcaveOn π•œ s f :=
  ⟨hs, fun _ _ _ _ _ _ _ _ _ => by rw [f.map_add, f.map_smul, f.map_smul]⟩
Concavity of Linear Maps on Convex Sets
Informal description
Let $E$ and $\beta$ be vector spaces over a scalar field $\mathbb{K}$, and let $f : E \to \beta$ be a linear map. For any convex set $s \subseteq E$, the function $f$ is concave on $s$ with respect to $\mathbb{K}$.
StrictConvexOn.convexOn theorem
{s : Set E} {f : E β†’ Ξ²} (hf : StrictConvexOn π•œ s f) : ConvexOn π•œ s f
Full source 
theorem StrictConvexOn.convexOn {s : Set E} {f : E β†’ Ξ²} (hf : StrictConvexOn π•œ s f) :
    ConvexOn π•œ s f :=
  convexOn_iff_pairwise_pos.mpr
    ⟨hf.1, fun _ hx _ hy hxy _ _ ha hb hab => (hf.2 hx hy hxy ha hb hab).le⟩
Strictly convex functions are convex
Informal description
Let $E$ be a vector space over an ordered semiring $\mathbb{K}$, and let $\beta$ be an ordered additive commutative monoid. If a function $f : E \to \beta$ is strictly convex on a convex set $s \subseteq E$, then $f$ is convex on $s$.
StrictConcaveOn.concaveOn theorem
{s : Set E} {f : E β†’ Ξ²} (hf : StrictConcaveOn π•œ s f) : ConcaveOn π•œ s f
Full source 
theorem StrictConcaveOn.concaveOn {s : Set E} {f : E β†’ Ξ²} (hf : StrictConcaveOn π•œ s f) :
    ConcaveOn π•œ s f :=
  hf.dual.convexOn
Strictly concave functions are concave
Informal description
Let $E$ be a vector space over an ordered semiring $\mathbb{K}$, and let $\beta$ be an ordered additive commutative monoid. If a function $f : E \to \beta$ is strictly concave on a convex set $s \subseteq E$, then $f$ is concave on $s$.
StrictConvexOn.convex_lt theorem
(hf : StrictConvexOn π•œ s f) (r : Ξ²) : Convex π•œ ({x ∈ s | f x < r})
Full source 
theorem StrictConvexOn.convex_lt (hf : StrictConvexOn π•œ s f) (r : Ξ²) :
    Convex π•œ ({ x ∈ s | f x < r }) :=
  convex_iff_pairwise_pos.2 fun x hx y hy hxy a b ha hb hab =>
    ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
      calc
        f (a β€’ x + b β€’ y) < a β€’ f x + b β€’ f y := hf.2 hx.1 hy.1 hxy ha hb hab
        _ ≀ a β€’ r + b β€’ r := by
          gcongr
          Β· exact hx.2.le
          Β· exact hy.2.le
        _ = r := Convex.combo_self hab r
        ⟩
Convexity of Sublevel Sets of Strictly Convex Functions
Informal description
Let $E$ be a vector space over an ordered semiring $\mathbb{K}$, and let $\beta$ be an ordered additive commutative monoid. Given a strictly convex function $f : E \to \beta$ on a convex set $s \subseteq E$ and an element $r \in \beta$, the sublevel set $\{x \in s \mid f(x) < r\}$ is convex in $E$.
StrictConcaveOn.convex_gt theorem
(hf : StrictConcaveOn π•œ s f) (r : Ξ²) : Convex π•œ ({x ∈ s | r < f x})
Full source 
theorem StrictConcaveOn.convex_gt (hf : StrictConcaveOn π•œ s f) (r : Ξ²) :
    Convex π•œ ({ x ∈ s | r < f x }) :=
  hf.dual.convex_lt r
Convexity of Superlevel Sets of Strictly Concave Functions
Informal description
Let $E$ be a vector space over an ordered semiring $\mathbb{K}$, and let $\beta$ be an ordered additive commutative monoid. Given a strictly concave function $f : E \to \beta$ on a convex set $s \subseteq E$ and an element $r \in \beta$, the superlevel set $\{x \in s \mid r < f(x)\}$ is convex in $E$.
LinearOrder.convexOn_of_lt theorem
(hs : Convex π•œ s) (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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
Full source 
/-- 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.convexOn_of_lt (hs : Convex π•œ s)
    (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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 := by
  refine convexOn_iff_pairwise_pos.2 ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩
  wlog h : x < y
  Β· rw [add_comm (a β€’ x), add_comm (a β€’ f x)]
    rw [add_comm] at hab
    exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_lt.resolve_left h)
  exact hf hx hy h ha hb hab
Sufficient condition for convexity via inequality for ordered pairs
Informal description
Let $s$ be a convex set in a vector space $E$ over an ordered semiring $\mathbb{K}$, and let $f : E \to \beta$ be a function. Suppose that for any two points $x, y \in s$ with $x < y$ and any positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the inequality \[ f(a x + b y) \leq a f(x) + b f(y) \] holds. Then $f$ is convex on $s$ with respect to $\mathbb{K}$.
LinearOrder.concaveOn_of_lt theorem
(hs : Convex π•œ s) (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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
Full source 
/-- 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.concaveOn_of_lt (hs : Convex π•œ s)
    (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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 :=
  LinearOrder.convexOn_of_lt (Ξ² := Ξ²α΅’α΅ˆ) hs hf
Sufficient condition for concavity via inequality for ordered pairs
Informal description
Let $s$ be a convex set in a vector space $E$ over an ordered semiring $\mathbb{K}$, and let $f : E \to \beta$ be a function. Suppose that for any two points $x, y \in s$ with $x < y$ and any positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the inequality \[ a f(x) + b f(y) \leq f(a x + b y) \] holds. Then $f$ is concave on $s$ with respect to $\mathbb{K}$.
LinearOrder.strictConvexOn_of_lt theorem
(hs : Convex π•œ s) (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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
Full source 
/-- 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.strictConvexOn_of_lt (hs : Convex π•œ s)
    (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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 := by
  refine ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩
  wlog h : x < y
  Β· rw [add_comm (a β€’ x), add_comm (a β€’ f x)]
    rw [add_comm] at hab
    exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_lt.resolve_left h)
  exact hf hx hy h ha hb hab
Sufficient condition for strict convexity via inequality for ordered pairs
Informal description
Let $s$ be a convex set in a vector space $E$ over a linearly ordered field $\mathbb{K}$, and let $f : E \to \beta$ be a function. If for any two distinct points $x, y \in s$ with $x < y$ and any positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the strict inequality \[ f(a x + b y) < a f(x) + b f(y) \] holds, then $f$ is strictly convex on $s$ with respect to $\mathbb{K}$.
LinearOrder.strictConcaveOn_of_lt theorem
(hs : Convex π•œ s) (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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
Full source 
/-- 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 LinearOrder.strictConcaveOn_of_lt (hs : Convex π•œ s)
    (hf : βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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 :=
  LinearOrder.strictConvexOn_of_lt (Ξ² := Ξ²α΅’α΅ˆ) hs hf
Sufficient condition for strict concavity via inequality for ordered pairs
Informal description
Let $s$ be a convex set in a vector space $E$ over a linearly ordered field $\mathbb{K}$, and let $f : E \to \beta$ be a function. If for any two distinct points $x, y \in s$ with $x < y$ and any positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the strict inequality \[ a f(x) + b f(y) < f(a x + b y) \] holds, then $f$ is strictly concave on $s$ with respect to $\mathbb{K}$.
ConvexOn.comp_linearMap theorem
{f : F β†’ Ξ²} {s : Set F} (hf : ConvexOn π•œ s f) (g : E β†’β‚—[π•œ] F) : ConvexOn π•œ (g ⁻¹' s) (f ∘ g)
Full source 
/-- If `g` is convex on `s`, so is `(f ∘ g)` on `f ⁻¹' s` for a linear `f`. -/
theorem ConvexOn.comp_linearMap {f : F β†’ Ξ²} {s : Set F} (hf : ConvexOn π•œ s f) (g : E β†’β‚—[π•œ] F) :
    ConvexOn π•œ (g ⁻¹' s) (f ∘ g) :=
  ⟨hf.1.linear_preimage _, fun x hx y hy a b ha hb hab =>
    calc
      f (g (a β€’ x + b β€’ y)) = f (a β€’ g x + b β€’ g y) := by rw [g.map_add, g.map_smul, g.map_smul]
      _ ≀ a β€’ f (g x) + b β€’ f (g y) := hf.2 hx hy ha hb hab⟩
Convexity of Composition with Linear Map
Informal description
Let $f : F \to \beta$ be a convex function on a convex set $s \subseteq F$ with respect to scalars $\mathbb{K}$, and let $g : E \to F$ be a linear map. Then the composition $f \circ g$ is convex on the preimage $g^{-1}(s) \subseteq E$.
ConcaveOn.comp_linearMap theorem
{f : F β†’ Ξ²} {s : Set F} (hf : ConcaveOn π•œ s f) (g : E β†’β‚—[π•œ] F) : ConcaveOn π•œ (g ⁻¹' s) (f ∘ g)
Full source 
/-- If `g` is concave on `s`, so is `(g ∘ f)` on `f ⁻¹' s` for a linear `f`. -/
theorem ConcaveOn.comp_linearMap {f : F β†’ Ξ²} {s : Set F} (hf : ConcaveOn π•œ s f) (g : E β†’β‚—[π•œ] F) :
    ConcaveOn π•œ (g ⁻¹' s) (f ∘ g) :=
  hf.dual.comp_linearMap g
Concavity of Composition with Linear Map
Informal description
Let $f : F \to \beta$ be a concave function on a convex set $s \subseteq F$ with respect to scalars $\mathbb{K}$, and let $g : E \to F$ be a linear map. Then the composition $f \circ g$ is concave on the preimage $g^{-1}(s) \subseteq E$.
StrictConvexOn.add_convexOn theorem
(hf : StrictConvexOn π•œ s f) (hg : ConvexOn π•œ s g) : StrictConvexOn π•œ s (f + g)
Full source 
theorem StrictConvexOn.add_convexOn (hf : StrictConvexOn π•œ s f) (hg : ConvexOn π•œ s g) :
    StrictConvexOn π•œ s (f + g) :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab =>
    calc
      f (a β€’ x + b β€’ y) + g (a β€’ x + b β€’ y) < a β€’ f x + b β€’ f y + (a β€’ g x + b β€’ g y) :=
        add_lt_add_of_lt_of_le (hf.2 hx hy hxy ha hb hab) (hg.2 hx hy ha.le hb.le hab)
      _ = a β€’ (f x + g x) + b β€’ (f y + g y) := by rw [smul_add, smul_add, add_add_add_comm]⟩
Sum of Strictly Convex and Convex Functions is Strictly Convex
Informal description
Let $f : E \to \beta$ be a strictly convex function on a convex set $s$ with respect to scalars $\mathbb{K}$, and let $g : E \to \beta$ be a convex function on $s$. Then the sum $f + g$ is strictly convex on $s$.
ConvexOn.add_strictConvexOn theorem
(hf : ConvexOn π•œ s f) (hg : StrictConvexOn π•œ s g) : StrictConvexOn π•œ s (f + g)
Full source 
theorem ConvexOn.add_strictConvexOn (hf : ConvexOn π•œ s f) (hg : StrictConvexOn π•œ s g) :
    StrictConvexOn π•œ s (f + g) :=
  add_comm g f β–Έ hg.add_convexOn hf
Sum of Convex and Strictly Convex Functions is Strictly Convex
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$, and let $g : E \to \beta$ be a strictly convex function on $s$. Then the sum $f + g$ is strictly convex on $s$.
StrictConvexOn.add theorem
(hf : StrictConvexOn π•œ s f) (hg : StrictConvexOn π•œ s g) : StrictConvexOn π•œ s (f + g)
Full source 
theorem StrictConvexOn.add (hf : StrictConvexOn π•œ s f) (hg : StrictConvexOn π•œ s g) :
    StrictConvexOn π•œ s (f + g) :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab =>
    calc
      f (a β€’ x + b β€’ y) + g (a β€’ x + b β€’ y) < a β€’ f x + b β€’ f y + (a β€’ g x + b β€’ g y) :=
        add_lt_add (hf.2 hx hy hxy ha hb hab) (hg.2 hx hy hxy ha hb hab)
      _ = a β€’ (f x + g x) + b β€’ (f y + g y) := by rw [smul_add, smul_add, add_add_add_comm]⟩
Sum of Strictly Convex Functions is Strictly Convex
Informal description
Let $f, g : E \to \beta$ be strictly convex functions on a convex set $s$ with respect to scalars $\mathbb{K}$. Then the sum $f + g$ is strictly convex on $s$.
StrictConcaveOn.add_concaveOn theorem
(hf : StrictConcaveOn π•œ s f) (hg : ConcaveOn π•œ s g) : StrictConcaveOn π•œ s (f + g)
Full source 
theorem StrictConcaveOn.add_concaveOn (hf : StrictConcaveOn π•œ s f) (hg : ConcaveOn π•œ s g) :
    StrictConcaveOn π•œ s (f + g) :=
  hf.dual.add_convexOn hg.dual
Sum of Strictly Concave and Concave Functions is Strictly Concave
Informal description
Let $f : E \to \beta$ be a strictly concave function on a convex set $s$ with respect to scalars $\mathbb{K}$, and let $g : E \to \beta$ be a concave function on $s$. Then the sum $f + g$ is strictly concave on $s$.
ConcaveOn.add_strictConcaveOn theorem
(hf : ConcaveOn π•œ s f) (hg : StrictConcaveOn π•œ s g) : StrictConcaveOn π•œ s (f + g)
Full source 
theorem ConcaveOn.add_strictConcaveOn (hf : ConcaveOn π•œ s f) (hg : StrictConcaveOn π•œ s g) :
    StrictConcaveOn π•œ s (f + g) :=
  hf.dual.add_strictConvexOn hg.dual
Sum of Concave and Strictly Concave Functions is Strictly Concave
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If $f : E \to \beta$ is a concave function on $s$ and $g : E \to \beta$ is a strictly concave function on $s$ with respect to $\mathbb{K}$, then their sum $f + g$ is strictly concave on $s$.
StrictConcaveOn.add theorem
(hf : StrictConcaveOn π•œ s f) (hg : StrictConcaveOn π•œ s g) : StrictConcaveOn π•œ s (f + g)
Full source 
theorem StrictConcaveOn.add (hf : StrictConcaveOn π•œ s f) (hg : StrictConcaveOn π•œ s g) :
    StrictConcaveOn π•œ s (f + g) :=
  hf.dual.add hg
Sum of Strictly Concave Functions is Strictly Concave
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If $f, g : E \to \beta$ are strictly concave functions on $s$ with respect to $\mathbb{K}$, then their sum $f + g$ is also strictly concave on $s$.
StrictConvexOn.add_const theorem
{Ξ³ : Type*} {f : E β†’ Ξ³} [AddCommMonoid Ξ³] [PartialOrder Ξ³] [IsOrderedCancelAddMonoid Ξ³] [Module π•œ Ξ³] (hf : StrictConvexOn π•œ s f) (b : Ξ³) : StrictConvexOn π•œ s (f + fun _ => b)
Full source 
theorem StrictConvexOn.add_const {Ξ³ : Type*} {f : E β†’ Ξ³}
    [AddCommMonoid Ξ³] [PartialOrder Ξ³] [IsOrderedCancelAddMonoid Ξ³]
    [Module π•œ Ξ³] (hf : StrictConvexOn π•œ s f) (b : Ξ³) : StrictConvexOn π•œ s (f + fun _ => b) :=
  hf.add_convexOn (convexOn_const _ hf.1)
Strict convexity is preserved under addition of a constant
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \gamma$ is a strictly convex function on $s$ with respect to $\mathbb{K}$, where $\gamma$ is an ordered cancellative additive monoid equipped with a $\mathbb{K}$-module structure. Then for any constant $b \in \gamma$, the function $f + b$ (defined pointwise as $(f + b)(x) = f(x) + b$) is also strictly convex on $s$.
StrictConcaveOn.add_const theorem
{Ξ³ : Type*} {f : E β†’ Ξ³} [AddCommMonoid Ξ³] [PartialOrder Ξ³] [IsOrderedCancelAddMonoid Ξ³] [Module π•œ Ξ³] (hf : StrictConcaveOn π•œ s f) (b : Ξ³) : StrictConcaveOn π•œ s (f + fun _ => b)
Full source 
theorem StrictConcaveOn.add_const {Ξ³ : Type*} {f : E β†’ Ξ³}
    [AddCommMonoid Ξ³] [PartialOrder Ξ³] [IsOrderedCancelAddMonoid Ξ³]
    [Module π•œ Ξ³] (hf : StrictConcaveOn π•œ s f) (b : Ξ³) : StrictConcaveOn π•œ s (f + fun _ => b) :=
  hf.add_concaveOn (concaveOn_const _ hf.1)
Strict Concavity is Preserved Under Addition of a Constant
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Suppose $f : E \to \gamma$ is a strictly concave function on $s$ with respect to $\mathbb{K}$, where $\gamma$ is an ordered cancellative additive monoid equipped with a $\mathbb{K}$-module structure. Then for any constant $b \in \gamma$, the function $f + b$ (defined pointwise as $(f + b)(x) = f(x) + b$) is also strictly concave on $s$.
ConvexOn.convex_lt theorem
(hf : ConvexOn π•œ s f) (r : Ξ²) : Convex π•œ ({x ∈ s | f x < r})
Full source 
theorem ConvexOn.convex_lt (hf : ConvexOn π•œ s f) (r : Ξ²) : Convex π•œ ({ x ∈ s | f x < r }) :=
  convex_iff_forall_pos.2 fun x hx y hy a b ha hb hab =>
    ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
      calc
        f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := hf.2 hx.1 hy.1 ha.le hb.le hab
        _ < a β€’ r + b β€’ r :=
          (add_lt_add_of_lt_of_le (smul_lt_smul_of_pos_left hx.2 ha)
            (smul_le_smul_of_nonneg_left hy.2.le hb.le))
        _ = r := Convex.combo_self hab _⟩
Convexity of sublevel sets of a convex function
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. Then for any $r \in \beta$, the sublevel set $\{x \in s \mid f(x) < r\}$ is convex in $\mathbb{K}$.
ConcaveOn.convex_gt theorem
(hf : ConcaveOn π•œ s f) (r : Ξ²) : Convex π•œ ({x ∈ s | r < f x})
Full source 
theorem ConcaveOn.convex_gt (hf : ConcaveOn π•œ s f) (r : Ξ²) : Convex π•œ ({ x ∈ s | r < f x }) :=
  hf.dual.convex_lt r
Convexity of Superlevel Sets of a Concave Function
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f : E \to \beta$ a concave function on $s$ with respect to $\mathbb{K}$. Then for any $r \in \beta$, the superlevel set $\{x \in s \mid r < f(x)\}$ is convex in $\mathbb{K}$.
ConvexOn.openSegment_subset_strict_epigraph theorem
(hf : ConvexOn π•œ s f) (p 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}
Full source 
theorem ConvexOn.openSegment_subset_strict_epigraph (hf : ConvexOn π•œ s f) (p q : E Γ— Ξ²)
    (hp : p.1 ∈ sp.1 ∈ s ∧ f p.1 < p.2) (hq : q.1 ∈ sq.1 ∈ s ∧ f q.1 ≀ q.2) :
    openSegmentopenSegment π•œ p q βŠ† { p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 < p.2 } := by
  rintro _ ⟨a, b, ha, hb, hab, rfl⟩
  refine ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, ?_⟩
  calc
    f (a β€’ p.1 + b β€’ q.1) ≀ a β€’ f p.1 + b β€’ f q.1 := hf.2 hp.1 hq.1 ha.le hb.le hab
    _ < a β€’ p.2 + b β€’ q.2 := add_lt_add_of_lt_of_le
       (smul_lt_smul_of_pos_left hp.2 ha) (smul_le_smul_of_nonneg_left hq.2 hb.le)
Open Segment in Strict Epigraph of a Convex Function
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f : E \to \beta$ a convex function on $s$ with respect to $\mathbb{K}$. For any two points $p, q \in E \times \beta$ such that: - $p_1 \in s$ and $f(p_1) < p_2$, - $q_1 \in s$ and $f(q_1) \leq q_2$, the open segment joining $p$ and $q$ is entirely contained in the strict epigraph of $f$, i.e., $\{ (x, y) \in E \times \beta \mid x \in s \text{ and } f(x) < y \}$.
ConcaveOn.openSegment_subset_strict_hypograph theorem
(hf : ConcaveOn π•œ s f) (p 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}
Full source 
theorem ConcaveOn.openSegment_subset_strict_hypograph (hf : ConcaveOn π•œ s f) (p q : E Γ— Ξ²)
    (hp : p.1 ∈ sp.1 ∈ s ∧ p.2 < f p.1) (hq : q.1 ∈ sq.1 ∈ s ∧ q.2 ≀ f q.1) :
    openSegmentopenSegment π•œ p q βŠ† { p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 < f p.1 } :=
  hf.dual.openSegment_subset_strict_epigraph p q hp hq
Open Segment in Strict Hypograph of a Concave Function
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f : E \to \beta$ a concave function on $s$ with respect to $\mathbb{K}$. For any two points $p, q \in E \times \beta$ such that: - $p_1 \in s$ and $p_2 < f(p_1)$, - $q_1 \in s$ and $q_2 \leq f(q_1)$, the open segment joining $p$ and $q$ is entirely contained in the strict hypograph of $f$, i.e., $\{ (x, y) \in E \times \beta \mid x \in s \text{ and } y < f(x) \}$.
ConvexOn.convex_strict_epigraph theorem
[ZeroLEOneClass π•œ] (hf : ConvexOn π•œ s f) : Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 < p.2}
Full source 
theorem ConvexOn.convex_strict_epigraph [ZeroLEOneClass π•œ] (hf : ConvexOn π•œ s f) :
    Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ f p.1 < p.2 } :=
  convex_iff_openSegment_subset.mpr fun p hp q hq =>
    hf.openSegment_subset_strict_epigraph p q hp ⟨hq.1, hq.2.le⟩
Convexity of the Strict Epigraph of a Convex Function
Informal description
Let $\mathbb{K}$ be an ordered scalar ring with $0 \leq 1$, $E$ a vector space over $\mathbb{K}$, and $\beta$ an ordered additive commutative monoid. If $f : E \to \beta$ is a convex function on a convex set $s \subseteq E$, then the strict epigraph of $f$, defined as $\{(x, y) \in E \times \beta \mid x \in s \text{ and } f(x) < y\}$, is a convex set with respect to $\mathbb{K}$.
ConcaveOn.convex_strict_hypograph theorem
[ZeroLEOneClass π•œ] (hf : ConcaveOn π•œ s f) : Convex π•œ {p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 < f p.1}
Full source 
theorem ConcaveOn.convex_strict_hypograph [ZeroLEOneClass π•œ] (hf : ConcaveOn π•œ s f) :
    Convex π•œ { p : E Γ— Ξ² | p.1 ∈ s ∧ p.2 < f p.1 } :=
  hf.dual.convex_strict_epigraph
Convexity of Strict Hypograph of a Concave Function
Informal description
Let $\mathbb{K}$ be an ordered scalar ring with $0 \leq 1$, $E$ a vector space over $\mathbb{K}$, and $\beta$ an ordered additive commutative monoid. If $f : E \to \beta$ is a concave function on a convex set $s \subseteq E$, then the strict hypograph of $f$, defined as $\{(x, y) \in E \times \beta \mid x \in s \text{ and } y < f(x)\}$, is a convex set with respect to $\mathbb{K}$.
ConvexOn.sup theorem
(hf : ConvexOn π•œ s f) (hg : ConvexOn π•œ s g) : ConvexOn π•œ s (f βŠ” g)
Full source 
/-- The pointwise maximum of convex functions is convex. -/
theorem ConvexOn.sup (hf : ConvexOn π•œ s f) (hg : ConvexOn π•œ s g) : ConvexOn π•œ s (f βŠ” g) := by
  refine ⟨hf.left, fun x hx y hy a b ha hb hab => sup_le ?_ ?_⟩
  Β· calc
      f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := hf.right hx hy ha hb hab
      _ ≀ a β€’ (f x βŠ” g x) + b β€’ (f y βŠ” g y) := by gcongr <;> apply le_sup_left
  Β· calc
      g (a β€’ x + b β€’ y) ≀ a β€’ g x + b β€’ g y := hg.right hx hy ha hb hab
      _ ≀ a β€’ (f x βŠ” g x) + b β€’ (f y βŠ” g y) := by gcongr <;> apply le_sup_right
Convexity of Pointwise Supremum of Convex Functions
Informal description
Let $\mathbb{K}$ be an ordered scalar ring, $E$ a vector space over $\mathbb{K}$, and $\beta$ an ordered additive commutative monoid. Let $s \subseteq E$ be a convex set, and $f, g : E \to \beta$ be convex functions on $s$. Then the pointwise supremum function $f \sqcup g$ (defined by $(f \sqcup g)(x) = \max(f(x), g(x))$ for all $x \in s$) is also convex on $s$.
ConcaveOn.inf theorem
(hf : ConcaveOn π•œ s f) (hg : ConcaveOn π•œ s g) : ConcaveOn π•œ s (f βŠ“ g)
Full source 
/-- The pointwise minimum of concave functions is concave. -/
theorem ConcaveOn.inf (hf : ConcaveOn π•œ s f) (hg : ConcaveOn π•œ s g) : ConcaveOn π•œ s (f βŠ“ g) :=
  hf.dual.sup hg
Pointwise Infimum of Concave Functions is Concave
Informal description
Let $\mathbb{K}$ be an ordered scalar ring, $E$ a vector space over $\mathbb{K}$, and $\beta$ an ordered additive commutative monoid. Let $s \subseteq E$ be a convex set, and $f, g : E \to \beta$ be concave functions on $s$. Then the pointwise infimum function $f \sqcap g$ (defined by $(f \sqcap g)(x) = \min(f(x), g(x))$ for all $x \in s$) is also concave on $s$.
StrictConvexOn.sup theorem
(hf : StrictConvexOn π•œ s f) (hg : StrictConvexOn π•œ s g) : StrictConvexOn π•œ s (f βŠ” g)
Full source 
/-- The pointwise maximum of strictly convex functions is strictly convex. -/
theorem StrictConvexOn.sup (hf : StrictConvexOn π•œ s f) (hg : StrictConvexOn π•œ s g) :
    StrictConvexOn π•œ s (f βŠ” g) :=
  ⟨hf.left, fun x hx y hy hxy a b ha hb hab =>
    max_lt
      (calc
        f (a β€’ x + b β€’ y) < a β€’ f x + b β€’ f y := hf.2 hx hy hxy ha hb hab
        _ ≀ a β€’ (f x βŠ” g x) + b β€’ (f y βŠ” g y) := by gcongr <;> apply le_sup_left)
      (calc
        g (a β€’ x + b β€’ y) < a β€’ g x + b β€’ g y := hg.2 hx hy hxy ha hb hab
        _ ≀ a β€’ (f x βŠ” g x) + b β€’ (f y βŠ” g y) := by gcongr <;> apply le_sup_right)⟩
Pointwise Supremum of Strictly Convex Functions is Strictly Convex
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If $f, g : E \to \beta$ are strictly convex functions on $s$, then their pointwise supremum $f \sqcup g$ (defined by $(f \sqcup g)(x) = \max(f(x), g(x))$ for all $x \in s$) is also strictly convex on $s$.
StrictConcaveOn.inf theorem
(hf : StrictConcaveOn π•œ s f) (hg : StrictConcaveOn π•œ s g) : StrictConcaveOn π•œ s (f βŠ“ g)
Full source 
/-- The pointwise minimum of strictly concave functions is strictly concave. -/
theorem StrictConcaveOn.inf (hf : StrictConcaveOn π•œ s f) (hg : StrictConcaveOn π•œ s g) :
    StrictConcaveOn π•œ s (f βŠ“ g) :=
  hf.dual.sup hg
Pointwise Infimum of Strictly Concave Functions is Strictly Concave
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If $f, g : E \to \beta$ are strictly concave functions on $s$, then their pointwise infimum $f \sqcap g$ (defined by $(f \sqcap g)(x) = \min(f(x), g(x))$ for all $x \in s$) is also strictly concave on $s$.
ConvexOn.le_on_segment' theorem
(hf : ConvexOn π•œ s f) {x 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)
Full source 
/-- A convex function on a segment is upper-bounded by the max of its endpoints. -/
theorem ConvexOn.le_on_segment' (hf : ConvexOn π•œ s f) {x 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) :=
  calc
    f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := hf.2 hx hy ha hb hab
    _ ≀ a β€’ max (f x) (f y) + b β€’ max (f x) (f y) := by
      gcongr
      Β· apply le_max_left
      Β· apply le_max_right
    _ = max (f x) (f y) := Convex.combo_self hab _
Convex Function Bounded by Maximum on Segment
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the value of $f$ at the convex combination $a \cdot x + b \cdot y$ is bounded above by the maximum of $f(x)$ and $f(y)$, i.e., \[ f(a \cdot x + b \cdot y) \leq \max(f(x), f(y)). \]
ConcaveOn.ge_on_segment' theorem
(hf : ConcaveOn π•œ s f) {x 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)
Full source 
/-- A concave function on a segment is lower-bounded by the min of its endpoints. -/
theorem ConcaveOn.ge_on_segment' (hf : ConcaveOn π•œ s f) {x 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) :=
  hf.dual.le_on_segment' hx hy ha hb hab
Concave Function Bounded by Minimum on Segment
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the value of $f$ at the convex combination $a \cdot x + b \cdot y$ is bounded below by the minimum of $f(x)$ and $f(y)$, i.e., \[ \min(f(x), f(y)) \leq f(a \cdot x + b \cdot y). \]
ConvexOn.le_on_segment theorem
(hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[π•œ] y]) : f z ≀ max (f x) (f y)
Full source 
/-- A convex function on a segment is upper-bounded by the max of its endpoints. -/
theorem ConvexOn.le_on_segment (hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ [x -[π•œ] y]) : f z ≀ max (f x) (f y) :=
  let ⟨_, _, ha, hb, hab, hz⟩ := hz
  hz β–Έ hf.le_on_segment' hx hy ha hb hab
Convex Function Bounded by Maximum on Segment
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and any point $z$ in the segment $[x, y]$, the value of $f$ at $z$ is bounded above by the maximum of $f(x)$ and $f(y)$, i.e., \[ f(z) \leq \max(f(x), f(y)). \]
ConcaveOn.ge_on_segment theorem
(hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[π•œ] y]) : min (f x) (f y) ≀ f z
Full source 
/-- A concave function on a segment is lower-bounded by the min of its endpoints. -/
theorem ConcaveOn.ge_on_segment (hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ [x -[π•œ] y]) : min (f x) (f y) ≀ f z :=
  hf.dual.le_on_segment hx hy hz
Concave Function Bounded Below by Minimum on Segment
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and any point $z$ in the segment $[x, y]$, the value of $f$ at $z$ is bounded below by the minimum of $f(x)$ and $f(y)$, i.e., \[ \min(f(x), f(y)) \leq f(z). \]
StrictConvexOn.lt_on_open_segment' theorem
(hf : StrictConvexOn π•œ s f) {x 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)
Full source 
/-- A strictly convex function on an open segment is strictly upper-bounded by the max of its
endpoints. -/
theorem StrictConvexOn.lt_on_open_segment' (hf : StrictConvexOn π•œ s f) {x 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) :=
  calc
    f (a β€’ x + b β€’ y) < a β€’ f x + b β€’ f y := hf.2 hx hy hxy ha hb hab
    _ ≀ a β€’ max (f x) (f y) + b β€’ max (f x) (f y) := by
      gcongr
      Β· apply le_max_left
      Β· apply le_max_right
    _ = max (f x) (f y) := Convex.combo_self hab _
Strict Convexity Implies Strict Upper Bound on Open Segments
Informal description
Let $f : E \to \beta$ be a strictly convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two distinct points $x, y \in s$ and positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the value of $f$ at the point $a \cdot x + b \cdot y$ is strictly less than the maximum of $f(x)$ and $f(y)$, i.e., \[ f(a \cdot x + b \cdot y) < \max(f(x), f(y)). \]
StrictConcaveOn.lt_on_open_segment' theorem
(hf : StrictConcaveOn π•œ s f) {x 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)
Full source 
/-- A strictly concave function on an open segment is strictly lower-bounded by the min of its
endpoints. -/
theorem StrictConcaveOn.lt_on_open_segment' (hf : StrictConcaveOn π•œ s f) {x 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) :=
  hf.dual.lt_on_open_segment' hx hy hxy ha hb hab
Strict Concavity Implies Strict Lower Bound on Open Segments
Informal description
Let $f : E \to \beta$ be a strictly concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two distinct points $x, y \in s$ and positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the value of $f$ at the point $a \cdot x + b \cdot y$ is strictly greater than the minimum of $f(x)$ and $f(y)$, i.e., \[ \min(f(x), f(y)) < f(a \cdot x + b \cdot y). \]
StrictConvexOn.lt_on_openSegment theorem
(hf : StrictConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x β‰  y) (hz : z ∈ openSegment π•œ x y) : f z < max (f x) (f y)
Full source 
/-- A strictly convex function on an open segment is strictly upper-bounded by the max of its
endpoints. -/
theorem StrictConvexOn.lt_on_openSegment (hf : StrictConvexOn π•œ s f) {x y z : E} (hx : x ∈ s)
    (hy : y ∈ s) (hxy : x β‰  y) (hz : z ∈ openSegment π•œ x y) : f z < max (f x) (f y) :=
  let ⟨_, _, ha, hb, hab, hz⟩ := hz
  hz β–Έ hf.lt_on_open_segment' hx hy hxy ha hb hab
Strictly Convex Functions are Strictly Bounded by Max on Open Segments
Informal description
Let $f : E \to \beta$ be a strictly convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two distinct points $x, y \in s$ and any point $z$ in the open segment between $x$ and $y$, the value of $f$ at $z$ is strictly less than the maximum of $f(x)$ and $f(y)$, i.e., \[ f(z) < \max(f(x), f(y)). \]
StrictConcaveOn.lt_on_openSegment theorem
(hf : StrictConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x β‰  y) (hz : z ∈ openSegment π•œ x y) : min (f x) (f y) < f z
Full source 
/-- A strictly concave function on an open segment is strictly lower-bounded by the min of its
endpoints. -/
theorem StrictConcaveOn.lt_on_openSegment (hf : StrictConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s)
    (hy : y ∈ s) (hxy : x β‰  y) (hz : z ∈ openSegment π•œ x y) : min (f x) (f y) < f z :=
  hf.dual.lt_on_openSegment hx hy hxy hz
Strictly Concave Functions are Strictly Lower-Bounded by Minimum on Open Segments
Informal description
Let $f : E \to \beta$ be a strictly concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two distinct points $x, y \in s$ and any point $z$ in the open segment between $x$ and $y$, the value of $f$ at $z$ is strictly greater than the minimum of $f(x)$ and $f(y)$, i.e., \[ \min(f(x), f(y)) < f(z). \]
ConvexOn.le_left_of_right_le' theorem
(hf : ConvexOn π•œ s f) {x 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
Full source 
theorem ConvexOn.le_left_of_right_le' (hf : ConvexOn π•œ s f) {x 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 :=
  le_of_not_lt fun h ↦ lt_irrefl (f (a β€’ x + b β€’ y)) <|
    calc
      f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := hf.2 hx hy ha.le hb hab
      _ < a β€’ f (a β€’ x + b β€’ y) + b β€’ f (a β€’ x + b β€’ y) := add_lt_add_of_lt_of_le
          (smul_lt_smul_of_pos_left h ha) (smul_le_smul_of_nonneg_left hfy hb)
      _ = f (a β€’ x + b β€’ y) := Convex.combo_self hab _
Convex Function Inequality: $f(y) \leq f(ax + by) \implies f(ax + by) \leq f(x)$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and scalars $a, b \in \mathbb{K}$ such that $a > 0$, $b \geq 0$, and $a + b = 1$, if $f(y) \leq f(a \cdot x + b \cdot y)$, then $f(a \cdot x + b \cdot y) \leq f(x)$.
ConcaveOn.left_le_of_le_right' theorem
(hf : ConcaveOn π•œ s f) {x 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)
Full source 
theorem ConcaveOn.left_le_of_le_right' (hf : ConcaveOn π•œ s f) {x 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) :=
  hf.dual.le_left_of_right_le' hx hy ha hb hab hfy
Concave Function Inequality: $f(ax + by) \leq f(y) \implies f(x) \leq f(ax + by)$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and scalars $a, b \in \mathbb{K}$ such that $a > 0$, $b \geq 0$, and $a + b = 1$, if $f(a \cdot x + b \cdot y) \leq f(y)$, then $f(x) \leq f(a \cdot x + b \cdot y)$.
ConvexOn.le_right_of_left_le' theorem
(hf : ConvexOn π•œ s f) {x 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
Full source 
theorem ConvexOn.le_right_of_left_le' (hf : ConvexOn π•œ s f) {x 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 := by
  rw [add_comm] at hab hfx ⊒
  exact hf.le_left_of_right_le' hy hx hb ha hab hfx
Convex Function Inequality: $f(x) \leq f(ax + by) \implies f(ax + by) \leq f(y)$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and scalars $a, b \in \mathbb{K}$ such that $a \geq 0$, $b > 0$, and $a + b = 1$, if $f(x) \leq f(a \cdot x + b \cdot y)$, then $f(a \cdot x + b \cdot y) \leq f(y)$.
ConcaveOn.right_le_of_le_left' theorem
(hf : ConcaveOn π•œ s f) {x 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)
Full source 
theorem ConcaveOn.right_le_of_le_left' (hf : ConcaveOn π•œ s f) {x 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) :=
  hf.dual.le_right_of_left_le' hx hy ha hb hab hfx
Concave Function Inequality: $f(ax + by) \leq f(x) \implies f(y) \leq f(ax + by)$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and scalars $a, b \in \mathbb{K}$ such that $a \geq 0$, $b > 0$, and $a + b = 1$, if $f(a \cdot x + b \cdot y) \leq f(x)$, then $f(y) \leq f(a \cdot x + b \cdot y)$.
ConvexOn.le_left_of_right_le theorem
(hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hyz : f y ≀ f z) : f z ≀ f x
Full source 
theorem ConvexOn.le_left_of_right_le (hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hyz : f y ≀ f z) : f z ≀ f x := by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.le_left_of_right_le' hx hy ha hb.le hab hyz
Convex Function Inequality: $f(y) \leq f(z) \implies f(z) \leq f(x)$ for $z$ in Segment $[x, y]$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z \in \text{openSegment}_{\mathbb{K}}(x, y)$), if $f(y) \leq f(z)$, then $f(z) \leq f(x)$.
ConcaveOn.left_le_of_le_right theorem
(hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hyz : f z ≀ f y) : f x ≀ f z
Full source 
theorem ConcaveOn.left_le_of_le_right (hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hyz : f z ≀ f y) : f x ≀ f z :=
  hf.dual.le_left_of_right_le hx hy hz hyz
Concave Function Inequality: $f(z) \leq f(y) \implies f(x) \leq f(z)$ for $z$ in Segment $[x, y]$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z \in \text{openSegment}_{\mathbb{K}}(x, y)$), if $f(z) \leq f(y)$, then $f(x) \leq f(z)$.
ConvexOn.le_right_of_left_le theorem
(hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hxz : f x ≀ f z) : f z ≀ f y
Full source 
theorem ConvexOn.le_right_of_left_le (hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hxz : f x ≀ f z) : f z ≀ f y := by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.le_right_of_left_le' hx hy ha.le hb hab hxz
Convex Function Inequality: $f(x) \leq f(z) \implies f(z) \leq f(y)$ for $z$ in Segment $(x, y)$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z = (1-t)x + t y$ for some $t \in (0,1)$), if $f(x) \leq f(z)$, then $f(z) \leq f(y)$.
ConcaveOn.right_le_of_le_left theorem
(hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hxz : f z ≀ f x) : f y ≀ f z
Full source 
theorem ConcaveOn.right_le_of_le_left (hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hxz : f z ≀ f x) : f y ≀ f z :=
  hf.dual.le_right_of_left_le hx hy hz hxz
Concave Function Inequality: $f(z) \leq f(x) \implies f(y) \leq f(z)$ for $z$ in Segment $(x, y)$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z = (1-t)x + t y$ for some $t \in (0,1)$), if $f(z) \leq f(x)$, then $f(y) \leq f(z)$.
ConvexOn.lt_left_of_right_lt' theorem
(hf : ConvexOn π•œ s f) {x 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
Full source 
theorem ConvexOn.lt_left_of_right_lt' (hf : ConvexOn π•œ s f) {x 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 :=
  not_le.1 fun h ↦ lt_irrefl (f (a β€’ x + b β€’ y)) <|
    calc
      f (a β€’ x + b β€’ y) ≀ a β€’ f x + b β€’ f y := hf.2 hx hy ha.le hb.le hab
      _ < a β€’ f (a β€’ x + b β€’ y) + b β€’ f (a β€’ x + b β€’ y) := add_lt_add_of_le_of_lt
          (smul_le_smul_of_nonneg_left h ha.le) (smul_lt_smul_of_pos_left hfy hb)
      _ = f (a β€’ x + b β€’ y) := Convex.combo_self hab _
Convex Function Inequality: $f(y) < f(ax + by) \Rightarrow f(ax + by) < f(x)$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, if $f(y) < f(a \cdot x + b \cdot y)$, then $f(a \cdot x + b \cdot y) < f(x)$.
ConcaveOn.left_lt_of_lt_right' theorem
(hf : ConcaveOn π•œ s f) {x 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)
Full source 
theorem ConcaveOn.left_lt_of_lt_right' (hf : ConcaveOn π•œ s f) {x 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) :=
  hf.dual.lt_left_of_right_lt' hx hy ha hb hab hfy
Concave Function Inequality: $f(ax + by) < f(y) \Rightarrow f(x) < f(ax + by)$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, if $f(a \cdot x + b \cdot y) < f(y)$, then $f(x) < f(a \cdot x + b \cdot y)$.
ConvexOn.lt_right_of_left_lt' theorem
(hf : ConvexOn π•œ s f) {x 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
Full source 
theorem ConvexOn.lt_right_of_left_lt' (hf : ConvexOn π•œ s f) {x 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 := by
  rw [add_comm] at hab hfx ⊒
  exact hf.lt_left_of_right_lt' hy hx hb ha hab hfx
Convex Function Inequality: $f(x) < f(ax + by) \Rightarrow f(ax + by) < f(y)$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, if $f(x) < f(a \cdot x + b \cdot y)$, then $f(a \cdot x + b \cdot y) < f(y)$.
ConcaveOn.lt_right_of_left_lt' theorem
(hf : ConcaveOn π•œ s f) {x 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)
Full source 
theorem ConcaveOn.lt_right_of_left_lt' (hf : ConcaveOn π•œ s f) {x 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) :=
  hf.dual.lt_right_of_left_lt' hx hy ha hb hab hfx
Concave Function Inequality: $f(ax + by) < f(x) \Rightarrow f(y) < f(ax + by)$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, if $f(a \cdot x + b \cdot y) < f(x)$, then $f(y) < f(a \cdot x + b \cdot y)$.
ConvexOn.lt_left_of_right_lt theorem
(hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hyz : f y < f z) : f z < f x
Full source 
theorem ConvexOn.lt_left_of_right_lt (hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hyz : f y < f z) : f z < f x := by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.lt_left_of_right_lt' hx hy ha hb hab hyz
Convex Function Inequality: $f(y) < f(z) \Rightarrow f(z) < f(x)$ for $z$ in Open Segment
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z \in \text{openSegment}_{\mathbb{K}}(x, y)$), if $f(y) < f(z)$, then $f(z) < f(x)$.
ConcaveOn.left_lt_of_lt_right theorem
(hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hyz : f z < f y) : f x < f z
Full source 
theorem ConcaveOn.left_lt_of_lt_right (hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hyz : f z < f y) : f x < f z :=
  hf.dual.lt_left_of_right_lt hx hy hz hyz
Concave Function Inequality: $f(z) < f(y) \Rightarrow f(x) < f(z)$ for $z$ in Open Segment
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z = (1-t)x + ty$ for some $t \in (0,1)$), if $f(z) < f(y)$, then $f(x) < f(z)$.
ConvexOn.lt_right_of_left_lt theorem
(hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hxz : f x < f z) : f z < f y
Full source 
theorem ConvexOn.lt_right_of_left_lt (hf : ConvexOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hxz : f x < f z) : f z < f y := by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.lt_right_of_left_lt' hx hy ha hb hab hxz
Convex Function Inequality: $f(x) < f(z) \Rightarrow f(z) < f(y)$ for $z$ in Open Segment
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z = (1-t)x + t y$ for some $t \in (0,1)$), if $f(x) < f(z)$, then $f(z) < f(y)$.
ConcaveOn.lt_right_of_left_lt theorem
(hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment π•œ x y) (hxz : f z < f x) : f y < f z
Full source 
theorem ConcaveOn.lt_right_of_left_lt (hf : ConcaveOn π•œ s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment π•œ x y) (hxz : f z < f x) : f y < f z :=
  hf.dual.lt_right_of_left_lt hx hy hz hxz
Concave Function Inequality: $f(z) < f(x) \Rightarrow f(y) < f(z)$ for $z$ in Open Segment
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any two points $x, y \in s$ and a point $z$ in the open segment between $x$ and $y$ (i.e., $z = (1-t)x + ty$ for some $t \in (0,1)$), if $f(z) < f(x)$, then $f(y) < f(z)$.
neg_convexOn_iff theorem
: ConvexOn π•œ s (-f) ↔ ConcaveOn π•œ s f
Full source 
/-- A function `-f` is convex iff `f` is concave. -/
@[simp]
theorem neg_convexOn_iff : ConvexOnConvexOn π•œ s (-f) ↔ ConcaveOn π•œ s f := by
  constructor
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩
    simp? [neg_apply, neg_le, add_comm] at h says
      simp only [Pi.neg_apply, smul_neg, le_add_neg_iff_add_le, add_comm,
        add_neg_le_iff_le_add] at h
    exact h hx hy ha hb hab
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩
    rw [← neg_le_neg_iff]
    simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
    exact h hx hy ha hb hab
Negation of Convex Function is Concave
Informal description
For a function $f : E \to \beta$ and a convex set $s \subseteq E$, the function $-f$ is convex on $s$ with respect to scalars $\mathbb{K}$ if and only if $f$ is concave on $s$ with respect to $\mathbb{K}$.
neg_concaveOn_iff theorem
: ConcaveOn π•œ s (-f) ↔ ConvexOn π•œ s f
Full source 
/-- A function `-f` is concave iff `f` is convex. -/
@[simp]
theorem neg_concaveOn_iff : ConcaveOnConcaveOn π•œ s (-f) ↔ ConvexOn π•œ s f := by
  rw [← neg_convexOn_iff, neg_neg f]
Negation of Concave Function is Convex
Informal description
For a function $f : E \to \beta$ and a convex set $s \subseteq E$, the function $-f$ is concave on $s$ with respect to scalars $\mathbb{K}$ if and only if $f$ is convex on $s$ with respect to $\mathbb{K}$.
neg_strictConvexOn_iff theorem
: StrictConvexOn π•œ s (-f) ↔ StrictConcaveOn π•œ s f
Full source 
/-- A function `-f` is strictly convex iff `f` is strictly concave. -/
@[simp]
theorem neg_strictConvexOn_iff : StrictConvexOnStrictConvexOn π•œ s (-f) ↔ StrictConcaveOn π•œ s f := by
  constructor
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy hxy a b ha hb hab => ?_⟩
    simp only [ne_eq, Pi.neg_apply, smul_neg, lt_add_neg_iff_add_lt, add_comm,
      add_neg_lt_iff_lt_add] at h
    exact h hx hy hxy ha hb hab
  · rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy hxy a b ha hb hab => ?_⟩
    rw [← neg_lt_neg_iff]
    simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
    exact h hx hy hxy ha hb hab
Negation of Strictly Convex Function is Strictly Concave
Informal description
For a function $f : E \to \beta$ and a convex set $s \subseteq E$, the function $-f$ is strictly convex on $s$ with respect to scalars $\mathbb{K}$ if and only if $f$ is strictly concave on $s$ with respect to $\mathbb{K}$.
neg_strictConcaveOn_iff theorem
: StrictConcaveOn π•œ s (-f) ↔ StrictConvexOn π•œ s f
Full source 
/-- A function `-f` is strictly concave iff `f` is strictly convex. -/
@[simp]
theorem neg_strictConcaveOn_iff : StrictConcaveOnStrictConcaveOn π•œ s (-f) ↔ StrictConvexOn π•œ s f := by
  rw [← neg_strictConvexOn_iff, neg_neg f]
Negation of Strictly Concave Function is Strictly Convex
Informal description
For a function $f : E \to \beta$ and a convex set $s \subseteq E$, the function $-f$ is strictly concave on $s$ with respect to scalars $\mathbb{K}$ if and only if $f$ is strictly convex on $s$ with respect to $\mathbb{K}$.
ConvexOn.sub theorem
(hf : ConvexOn π•œ s f) (hg : ConcaveOn π•œ s g) : ConvexOn π•œ s (f - g)
Full source 
theorem ConvexOn.sub (hf : ConvexOn π•œ s f) (hg : ConcaveOn π•œ s g) : ConvexOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add hg.neg
Convexity of the Difference of a Convex and a Concave Function
Informal description
Let $f : E \to \beta$ be a convex function and $g : E \to \beta$ be a concave function on a convex set $s \subseteq E$ with respect to scalars $\mathbb{K}$. Then the difference $f - g$ is convex on $s$.
ConcaveOn.sub theorem
(hf : ConcaveOn π•œ s f) (hg : ConvexOn π•œ s g) : ConcaveOn π•œ s (f - g)
Full source 
theorem ConcaveOn.sub (hf : ConcaveOn π•œ s f) (hg : ConvexOn π•œ s g) : ConcaveOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add hg.neg
Concavity of the Difference of a Concave and a Convex Function
Informal description
Let $f : E \to \beta$ be a concave function and $g : E \to \beta$ be a convex function on a convex set $s \subseteq E$ with respect to scalars $\mathbb{K}$. Then the difference $f - g$ is concave on $s$.
StrictConvexOn.sub theorem
(hf : StrictConvexOn π•œ s f) (hg : StrictConcaveOn π•œ s g) : StrictConvexOn π•œ s (f - g)
Full source 
theorem StrictConvexOn.sub (hf : StrictConvexOn π•œ s f) (hg : StrictConcaveOn π•œ s g) :
    StrictConvexOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add hg.neg
Difference of Strictly Convex and Strictly Concave Functions is Strictly Convex
Informal description
Let $f : E \to \beta$ be a strictly convex function and $g : E \to \beta$ be a strictly concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. Then the difference $f - g$ is strictly convex on $s$.
StrictConcaveOn.sub theorem
(hf : StrictConcaveOn π•œ s f) (hg : StrictConvexOn π•œ s g) : StrictConcaveOn π•œ s (f - g)
Full source 
theorem StrictConcaveOn.sub (hf : StrictConcaveOn π•œ s f) (hg : StrictConvexOn π•œ s g) :
    StrictConcaveOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add hg.neg
Difference of Strictly Concave and Strictly Convex Functions is Strictly Concave
Informal description
Let $E$ be a vector space over a scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If $f : E \to \beta$ is a strictly concave function and $g : E \to \beta$ is a strictly convex function on $s$ with respect to $\mathbb{K}$, then the difference $f - g$ is strictly concave on $s$.
ConvexOn.sub_strictConcaveOn theorem
(hf : ConvexOn π•œ s f) (hg : StrictConcaveOn π•œ s g) : StrictConvexOn π•œ s (f - g)
Full source 
theorem ConvexOn.sub_strictConcaveOn (hf : ConvexOn π•œ s f) (hg : StrictConcaveOn π•œ s g) :
    StrictConvexOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add_strictConvexOn hg.neg
Difference of Convex and Strictly Concave Functions is Strictly Convex
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$, and let $g : E \to \beta$ be a strictly concave function on $s$. Then the difference $f - g$ is strictly convex on $s$.
ConcaveOn.sub_strictConvexOn theorem
(hf : ConcaveOn π•œ s f) (hg : StrictConvexOn π•œ s g) : StrictConcaveOn π•œ s (f - g)
Full source 
theorem ConcaveOn.sub_strictConvexOn (hf : ConcaveOn π•œ s f) (hg : StrictConvexOn π•œ s g) :
    StrictConcaveOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add_strictConcaveOn hg.neg
Difference of Concave and Strictly Convex Functions is Strictly Concave
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If $f : E \to \beta$ is a concave function on $s$ and $g : E \to \beta$ is a strictly convex function on $s$ with respect to $\mathbb{K}$, then the difference $f - g$ is strictly concave on $s$.
StrictConvexOn.sub_concaveOn theorem
(hf : StrictConvexOn π•œ s f) (hg : ConcaveOn π•œ s g) : StrictConvexOn π•œ s (f - g)
Full source 
theorem StrictConvexOn.sub_concaveOn (hf : StrictConvexOn π•œ s f) (hg : ConcaveOn π•œ s g) :
    StrictConvexOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add_convexOn hg.neg
Difference of Strictly Convex and Concave Functions is Strictly Convex
Informal description
Let $f : E \to \beta$ be a strictly convex function on a convex set $s$ with respect to scalars $\mathbb{K}$, and let $g : E \to \beta$ be a concave function on $s$. Then the difference $f - g$ is strictly convex on $s$.
StrictConcaveOn.sub_convexOn theorem
(hf : StrictConcaveOn π•œ s f) (hg : ConvexOn π•œ s g) : StrictConcaveOn π•œ s (f - g)
Full source 
theorem StrictConcaveOn.sub_convexOn (hf : StrictConcaveOn π•œ s f) (hg : ConvexOn π•œ s g) :
    StrictConcaveOn π•œ s (f - g) :=
  (sub_eq_add_neg f g).symm β–Έ hf.add_concaveOn hg.neg
Difference of Strictly Concave and Convex Functions is Strictly Concave
Informal description
Let $f : E \to \beta$ be a strictly concave function on a convex set $s$ with respect to scalars $\mathbb{K}$, and let $g : E \to \beta$ be a convex function on $s$. Then the difference $f - g$ is strictly concave on $s$.
StrictConvexOn.translate_right theorem
(hf : StrictConvexOn π•œ s f) (c : E) : StrictConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
Full source 
/-- Right translation preserves strict convexity. -/
theorem StrictConvexOn.translate_right (hf : StrictConvexOn π•œ s f) (c : E) :
    StrictConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
  ⟨hf.1.translate_preimage_right _, fun x hx y hy hxy a b ha hb hab =>
    calc
      f (c + (a β€’ x + b β€’ y)) = f (a β€’ (c + x) + b β€’ (c + y)) := by
        rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]
      _ < a β€’ f (c + x) + b β€’ f (c + y) := hf.2 hx hy ((add_right_injective c).ne hxy) ha hb hab⟩
Right Translation Preserves Strict Convexity
Informal description
Let $f : E \to \beta$ be a strictly convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the function $f$ remains strictly convex on the translated set $\{z \in E \mid c + z \in s\}$ when composed with the right translation map $z \mapsto c + z$. In other words, the function $g(z) = f(c + z)$ is strictly convex on the preimage of $s$ under the translation $z \mapsto c + z$.
StrictConcaveOn.translate_right theorem
(hf : StrictConcaveOn π•œ s f) (c : E) : StrictConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z)
Full source 
/-- Right translation preserves strict concavity. -/
theorem StrictConcaveOn.translate_right (hf : StrictConcaveOn π•œ s f) (c : E) :
    StrictConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
  hf.dual.translate_right _
Right Translation Preserves Strict Concavity
Informal description
Let $f : E \to \beta$ be a strictly concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the function $f$ remains strictly concave on the translated set $\{z \in E \mid c + z \in s\}$ when composed with the right translation map $z \mapsto c + z$. In other words, the function $g(z) = f(c + z)$ is strictly concave on the preimage of $s$ under the translation $z \mapsto c + z$.
StrictConvexOn.translate_left theorem
(hf : StrictConvexOn π•œ s f) (c : E) : StrictConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
Full source 
/-- Left translation preserves strict convexity. -/
theorem StrictConvexOn.translate_left (hf : StrictConvexOn π•œ s f) (c : E) :
    StrictConvexOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c) := by
  simpa only [add_comm] using hf.translate_right c
Left Translation Preserves Strict Convexity
Informal description
Let $f : E \to \beta$ be a strictly convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the function $f$ remains strictly convex on the translated set $\{z \in E \mid c + z \in s\}$ when composed with the left translation map $z \mapsto z + c$. In other words, the function $g(z) = f(z + c)$ is strictly convex on the preimage of $s$ under the translation $z \mapsto z + c$.
StrictConcaveOn.translate_left theorem
(hf : StrictConcaveOn π•œ s f) (c : E) : StrictConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
Full source 
/-- Left translation preserves strict concavity. -/
theorem StrictConcaveOn.translate_left (hf : StrictConcaveOn π•œ s f) (c : E) :
    StrictConcaveOn π•œ ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c) := by
  simpa only [add_comm] using hf.translate_right c
Left Translation Preserves Strict Concavity
Informal description
Let $f : E \to \beta$ be a strictly concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any vector $c \in E$, the function $f$ remains strictly concave on the translated set $\{z \in E \mid c + z \in s\}$ when composed with the left translation map $z \mapsto z + c$. In other words, the function $g(z) = f(z + c)$ is strictly concave on the preimage of $s$ under the translation $z \mapsto z + c$.
ConvexOn.smul theorem
{c : π•œ} (hc : 0 ≀ c) (hf : ConvexOn π•œ s f) : ConvexOn π•œ s fun x => c β€’ f x
Full source 
theorem ConvexOn.smul {c : π•œ} (hc : 0 ≀ c) (hf : ConvexOn π•œ s f) : ConvexOn π•œ s fun x => c β€’ f x :=
  ⟨hf.1, fun x hx y hy a b ha hb hab =>
    calc
      c β€’ f (a β€’ x + b β€’ y) ≀ c β€’ (a β€’ f x + b β€’ f y) :=
        smul_le_smul_of_nonneg_left (hf.2 hx hy ha hb hab) hc
      _ = a β€’ c β€’ f x + b β€’ c β€’ f y := by rw [smul_add, smul_comm c, smul_comm c]⟩
Convexity is preserved under non-negative scalar multiplication
Informal description
Let $\mathbb{K}$ be an ordered semiring, $E$ be a vector space over $\mathbb{K}$, and $\beta$ be an ordered additive commutative monoid with a scalar multiplication by $\mathbb{K}$. Let $s$ be a convex subset of $E$ and $f : E \to \beta$ be a convex function on $s$. For any scalar $c \in \mathbb{K}$ with $0 \leq c$, the function $x \mapsto c \cdot f(x)$ is also convex on $s$.
ConcaveOn.smul theorem
{c : π•œ} (hc : 0 ≀ c) (hf : ConcaveOn π•œ s f) : ConcaveOn π•œ s fun x => c β€’ f x
Full source 
theorem ConcaveOn.smul {c : π•œ} (hc : 0 ≀ c) (hf : ConcaveOn π•œ s f) :
    ConcaveOn π•œ s fun x => c β€’ f x :=
  hf.dual.smul hc
Concavity is preserved under non-negative scalar multiplication
Informal description
Let $\mathbb{K}$ be an ordered semiring, $E$ be a vector space over $\mathbb{K}$, and $\beta$ be an ordered additive commutative monoid with a scalar multiplication by $\mathbb{K}$. Let $s$ be a convex subset of $E$ and $f : E \to \beta$ be a concave function on $s$. For any scalar $c \in \mathbb{K}$ with $0 \leq c$, the function $x \mapsto c \cdot f(x)$ is also concave on $s$.
ConvexOn.comp_affineMap theorem
{f : F β†’ Ξ²} (g : E →ᡃ[π•œ] F) {s : Set F} (hf : ConvexOn π•œ s f) : ConvexOn π•œ (g ⁻¹' s) (f ∘ g)
Full source 
/-- If a function is convex on `s`, it remains convex when precomposed by an affine map. -/
theorem ConvexOn.comp_affineMap {f : F β†’ Ξ²} (g : E →ᡃ[π•œ] F) {s : Set F} (hf : ConvexOn π•œ s f) :
    ConvexOn π•œ (g ⁻¹' s) (f ∘ g) :=
  ⟨hf.1.affine_preimage _, fun x hx y hy a b ha hb hab =>
    calc
      (f ∘ g) (a β€’ x + b β€’ y) = f (g (a β€’ x + b β€’ y)) := rfl
      _ = f (a β€’ g x + b β€’ g y) := by rw [Convex.combo_affine_apply hab]
      _ ≀ a β€’ f (g x) + b β€’ f (g y) := hf.2 hx hy ha hb hab⟩
Convexity is preserved under affine precomposition
Informal description
Let $E$ and $F$ be vector spaces over an ordered semiring $\mathbb{K}$, and let $\beta$ be an ordered additive commutative monoid with a scalar multiplication by $\mathbb{K}$. Given a convex function $f : F \to \beta$ on a convex set $s \subseteq F$, and an affine map $g : E \to F$, the composition $f \circ g$ is convex on the preimage $g^{-1}(s) \subseteq E$.
ConcaveOn.comp_affineMap theorem
{f : F β†’ Ξ²} (g : E →ᡃ[π•œ] F) {s : Set F} (hf : ConcaveOn π•œ s f) : ConcaveOn π•œ (g ⁻¹' s) (f ∘ g)
Full source 
/-- If a function is concave on `s`, it remains concave when precomposed by an affine map. -/
theorem ConcaveOn.comp_affineMap {f : F β†’ Ξ²} (g : E →ᡃ[π•œ] F) {s : Set F} (hf : ConcaveOn π•œ s f) :
    ConcaveOn π•œ (g ⁻¹' s) (f ∘ g) :=
  hf.dual.comp_affineMap g
Concavity is preserved under affine precomposition
Informal description
Let $E$ and $F$ be vector spaces over an ordered semiring $\mathbb{K}$, and let $\beta$ be an ordered additive commutative monoid with a scalar multiplication by $\mathbb{K}$. Given a concave function $f : F \to \beta$ on a convex set $s \subseteq F$, and an affine map $g : E \to F$, the composition $f \circ g$ is concave on the preimage $g^{-1}(s) \subseteq E$.
convexOn_iff_div theorem
{f : E β†’ Ξ²} : ConvexOn π•œ s f ↔ Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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
Full source 
theorem convexOn_iff_div {f : E β†’ Ξ²} :
    ConvexOnConvexOn π•œ s f ↔
      Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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 :=
  and_congr Iff.rfl ⟨by
    intro h x hx y hy a b ha hb hab
    apply h hx hy (div_nonneg ha hab.le) (div_nonneg hb hab.le)
    rw [← add_div, div_self hab.ne'], by
    intro h x hx y hy a b ha hb hab
    simpa [hab, zero_lt_one] using h hx hy ha hb⟩
Characterization of Convex Functions via Weighted Averages
Informal description
A function $f : E \to \beta$ is convex on a set $s$ with respect to scalars $\mathbb{K}$ if and only if $s$ is a convex set and for any two points $x, y \in s$ and any non-negative scalars $a, b \in \mathbb{K}$ with $a + b > 0$, the following inequality holds: \[ f\left(\frac{a}{a + b} x + \frac{b}{a + b} y\right) \leq \frac{a}{a + b} f(x) + \frac{b}{a + b} f(y). \]
concaveOn_iff_div theorem
{f : E β†’ Ξ²} : ConcaveOn π•œ s f ↔ Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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)
Full source 
theorem concaveOn_iff_div {f : E β†’ Ξ²} :
    ConcaveOnConcaveOn π•œ s f ↔
      Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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) :=
  convexOn_iff_div (Ξ² := Ξ²α΅’α΅ˆ)
Characterization of Concave Functions via Weighted Averages
Informal description
A function $f \colon E \to \beta$ is concave on a convex set $s \subseteq E$ with respect to scalars $\mathbb{K}$ if and only if $s$ is convex and for any two points $x, y \in s$ and any non-negative scalars $a, b \in \mathbb{K}$ with $a + b > 0$, the following inequality holds: \[ \frac{a}{a + b} f(x) + \frac{b}{a + b} f(y) \leq f\left(\frac{a}{a + b} x + \frac{b}{a + b} y\right). \]
strictConvexOn_iff_div theorem
{f : E β†’ Ξ²} : StrictConvexOn π•œ s f ↔ Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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
Full source 
theorem strictConvexOn_iff_div {f : E β†’ Ξ²} :
    StrictConvexOnStrictConvexOn π•œ s f ↔
      Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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 :=
  and_congr Iff.rfl ⟨by
    intro h x hx y hy hxy a b ha hb
    have hab := add_pos ha hb
    apply h hx hy hxy (div_pos ha hab) (div_pos hb hab)
    rw [← add_div, div_self hab.ne'], by
    intro h x hx y hy hxy a b ha hb hab
    simpa [hab, zero_lt_one] using h hx hy hxy ha hb⟩
Characterization of Strictly Convex Functions via Weighted Averages
Informal description
A function $f : E \to \beta$ is strictly convex on a convex set $s$ with respect to scalars $\mathbb{K}$ if and only if $s$ is convex and for any two distinct points $x, y \in s$ and any positive scalars $a, b \in \mathbb{K}$ with $a + b > 0$, the following strict inequality holds: \[ f\left(\frac{a}{a + b} \cdot x + \frac{b}{a + b} \cdot y\right) < \frac{a}{a + b} \cdot f(x) + \frac{b}{a + b} \cdot f(y). \]
strictConcaveOn_iff_div theorem
{f : E β†’ Ξ²} : StrictConcaveOn π•œ s f ↔ Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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)
Full source 
theorem strictConcaveOn_iff_div {f : E β†’ Ξ²} :
    StrictConcaveOnStrictConcaveOn π•œ s f ↔
      Convex π•œ s ∧ βˆ€ ⦃x⦄, x ∈ s β†’ βˆ€ ⦃y⦄, 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) :=
  strictConvexOn_iff_div (Ξ² := Ξ²α΅’α΅ˆ)
Characterization of Strictly Concave Functions via Weighted Averages
Informal description
A function $f : E \to \beta$ is strictly concave on a convex set $s$ with respect to scalars $\mathbb{K}$ if and only if $s$ is convex and for any two distinct points $x, y \in s$ and any positive scalars $a, b \in \mathbb{K}$ with $a + b > 0$, the following strict inequality holds: \[ \frac{a}{a + b} \cdot f(x) + \frac{b}{a + b} \cdot f(y) < f\left(\frac{a}{a + b} \cdot x + \frac{b}{a + b} \cdot y\right). \]
OrderIso.strictConvexOn_symm theorem
(f : Ξ± ≃o Ξ²) (hf : StrictConcaveOn π•œ univ f) : StrictConvexOn π•œ univ f.symm
Full source 
theorem OrderIso.strictConvexOn_symm (f : Ξ± ≃o Ξ²) (hf : StrictConcaveOn π•œ univ f) :
    StrictConvexOn π•œ univ f.symm := by
  refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  have hxy' : x' β‰  y' := by rw [← f.injective.ne_iff, ← hx'', ← hy'']; exact hxy
  simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]
  rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) hxy' ha hb hab
Strict Convexity of the Inverse of a Strictly Concave Order Isomorphism
Informal description
Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$. If $f$ is strictly concave on the universal set $\text{univ} \subseteq \alpha$ with respect to scalars $\mathbb{K}$, then its inverse $f^{-1} : \beta \to \alpha$ is strictly convex on the universal set $\text{univ} \subseteq \beta$ with respect to the same scalars $\mathbb{K}$.
OrderIso.convexOn_symm theorem
(f : Ξ± ≃o Ξ²) (hf : ConcaveOn π•œ univ f) : ConvexOn π•œ univ f.symm
Full source 
theorem OrderIso.convexOn_symm (f : Ξ± ≃o Ξ²) (hf : ConcaveOn π•œ univ f) :
    ConvexOn π•œ univ f.symm := by
  refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]
  rw [← f.le_iff_le, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab
Convexity of Inverse Function under Concave Order Isomorphism
Informal description
Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$. If $f$ is concave on the universal set $\text{univ} \subseteq \alpha$ with respect to scalars $\mathbb{K}$, then its inverse function $f^{-1} : \beta \to \alpha$ is convex on the universal set $\text{univ} \subseteq \beta$ with respect to the same scalars $\mathbb{K}$.
OrderIso.strictConcaveOn_symm theorem
(f : Ξ± ≃o Ξ²) (hf : StrictConvexOn π•œ univ f) : StrictConcaveOn π•œ univ f.symm
Full source 
theorem OrderIso.strictConcaveOn_symm (f : Ξ± ≃o Ξ²) (hf : StrictConvexOn π•œ univ f) :
    StrictConcaveOn π•œ univ f.symm := by
  refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  have hxy' : x' β‰  y' := by rw [← f.injective.ne_iff, ← hx'', ← hy'']; exact hxy
  simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]
  rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) hxy' ha hb hab
Strict Convexity of Order Isomorphism Implies Strict Concavity of Its Inverse
Informal description
Let $f \colon \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$. If $f$ is strictly convex on the universal set $\alpha$ with respect to scalars $\mathbb{K}$, then its inverse $f^{-1} \colon \beta \to \alpha$ is strictly concave on the universal set $\beta$ with respect to the same scalars $\mathbb{K}$.
OrderIso.concaveOn_symm theorem
(f : Ξ± ≃o Ξ²) (hf : ConvexOn π•œ univ f) : ConcaveOn π•œ univ f.symm
Full source 
theorem OrderIso.concaveOn_symm (f : Ξ± ≃o Ξ²) (hf : ConvexOn π•œ univ f) :
    ConcaveOn π•œ univ f.symm := by
  refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]
  rw [← f.le_iff_le, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab
Concavity of the Inverse of a Convex Order Isomorphism
Informal description
Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$. If $f$ is convex on the universal set $\text{univ} \subseteq \alpha$ with respect to scalars $\mathbb{K}$, then its inverse $f^{-1} : \beta \to \alpha$ is concave on the universal set $\text{univ} \subseteq \beta$ with respect to the same scalars $\mathbb{K}$.
ConvexOn.le_right_of_left_le'' theorem
(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
Full source 
theorem ConvexOn.le_right_of_left_le'' (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 :=
  hyz.eq_or_lt.elim (fun hyz => (congr_arg f hyz).le) fun hyz =>
    hf.le_right_of_left_le hx hz (Ioo_subset_openSegment ⟨hxy, hyz⟩) h
Convex Function Inequality: $f(x) \leq f(y) \implies f(y) \leq f(z)$ for $x < y \leq z$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any points $x, y, z \in s$ such that $x < y \leq z$, if $f(x) \leq f(y)$, then $f(y) \leq f(z)$.
ConvexOn.le_left_of_right_le'' theorem
(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
Full source 
theorem ConvexOn.le_left_of_right_le'' (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 :=
  hxy.eq_or_lt.elim (fun hxy => (congr_arg f hxy).ge) fun hxy =>
    hf.le_left_of_right_le hx hz (Ioo_subset_openSegment ⟨hxy, hyz⟩) h
Convex Function Inequality: $f(z) \leq f(y) \implies f(y) \leq f(x)$ for $x \leq y < z$
Informal description
Let $f : E \to \beta$ be a convex function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any points $x, y, z \in s$ such that $x \leq y < z$, if $f(z) \leq f(y)$, then $f(y) \leq f(x)$.
ConcaveOn.right_le_of_le_left'' theorem
(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
Full source 
theorem ConcaveOn.right_le_of_le_left'' (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 :=
  hf.dual.le_right_of_left_le'' hx hz hxy hyz h
Concave Function Inequality: $f(y) \leq f(x) \implies f(z) \leq f(y)$ for $x < y \leq z$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any points $x, y, z \in s$ such that $x < y \leq z$, if $f(y) \leq f(x)$, then $f(z) \leq f(y)$.
ConcaveOn.left_le_of_le_right'' theorem
(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
Full source 
theorem ConcaveOn.left_le_of_le_right'' (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 :=
  hf.dual.le_left_of_right_le'' hx hz hxy hyz h
Concave Function Inequality: $f(y) \leq f(z) \implies f(x) \leq f(y)$ for $x \leq y < z$
Informal description
Let $f : E \to \beta$ be a concave function on a convex set $s$ with respect to scalars $\mathbb{K}$. For any points $x, y, z \in s$ such that $x \leq y < z$, if $f(y) \leq f(z)$, then $f(x) \leq f(y)$.