# Uniformly and strongly convex functions #

In this file, we define uniformly convex functions and strongly convex functions.

For a real normed space E, a uniformly convex function with modulus φ : ℝ → ℝ is a function f : E → ℝ such that f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖ for all t ∈ [0, 1].

A m-strongly convex function is a uniformly convex function with modulus fun r ↦ m / 2 * r ^ 2. If E is an inner product space, this is equivalent to x ↦ f x - m / 2 * ‖x‖ ^ 2 being convex.

## TODO #

Prove derivative properties of strongly convex functions.

def UniformConvexOn {E : Type u_1} [] (s : Set E) (φ : ) (f : E) :

A function f from a real normed space is uniformly convex with modulus φ if f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖ for all t ∈ [0, 1].

φ is usually taken to be a monotone function such that φ r = 0 ↔ r = 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def UniformConcaveOn {E : Type u_1} [] (s : Set E) (φ : ) (f : E) :

A function f from a real normed space is uniformly concave with modulus φ if t • f x + (1 - t) • f y + t * (1 - t) * φ ‖x - y‖ ≤ f (t • x + (1 - t) • y) for all t ∈ [0, 1].

φ is usually taken to be a monotone function such that φ r = 0 ↔ r = 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem uniformConvexOn_zero {E : Type u_1} [] {s : Set E} {f : E} :
@[simp]
theorem uniformConcaveOn_zero {E : Type u_1} [] {s : Set E} {f : E} :
theorem ConvexOn.uniformConvexOn_zero {E : Type u_1} [] {s : Set E} {f : E} :

Alias of the reverse direction of uniformConvexOn_zero.

theorem ConcaveOn.uniformConcaveOn_zero {E : Type u_1} [] {s : Set E} {f : E} :

Alias of the reverse direction of uniformConcaveOn_zero.

theorem UniformConvexOn.mono {E : Type u_1} [] {φ : } {ψ : } {s : Set E} {f : E} (hψφ : ψ φ) (hf : ) :
theorem UniformConcaveOn.mono {E : Type u_1} [] {φ : } {ψ : } {s : Set E} {f : E} (hψφ : ψ φ) (hf : ) :
theorem UniformConvexOn.convexOn {E : Type u_1} [] {φ : } {s : Set E} {f : E} (hf : ) (hφ : 0 φ) :
theorem UniformConcaveOn.concaveOn {E : Type u_1} [] {φ : } {s : Set E} {f : E} (hf : ) (hφ : 0 φ) :
theorem UniformConvexOn.strictConvexOn {E : Type u_1} [] {φ : } {s : Set E} {f : E} (hf : ) (hφ : ∀ (r : ), r 00 < φ r) :
theorem UniformConcaveOn.strictConcaveOn {E : Type u_1} [] {φ : } {s : Set E} {f : E} (hf : ) (hφ : ∀ (r : ), r 00 < φ r) :
theorem UniformConvexOn.add {E : Type u_1} [] {φ : } {ψ : } {s : Set E} {f : E} {g : E} (hf : ) (hg : ) :
UniformConvexOn s (φ + ψ) (f + g)
theorem UniformConcaveOn.add {E : Type u_1} [] {φ : } {ψ : } {s : Set E} {f : E} {g : E} (hf : ) (hg : ) :
UniformConcaveOn s (φ + ψ) (f + g)
theorem UniformConvexOn.neg {E : Type u_1} [] {φ : } {s : Set E} {f : E} (hf : ) :
theorem UniformConcaveOn.neg {E : Type u_1} [] {φ : } {s : Set E} {f : E} (hf : ) :
theorem UniformConvexOn.sub {E : Type u_1} [] {φ : } {ψ : } {s : Set E} {f : E} {g : E} (hf : ) (hg : ) :
UniformConvexOn s (φ + ψ) (f - g)
theorem UniformConcaveOn.sub {E : Type u_1} [] {φ : } {ψ : } {s : Set E} {f : E} {g : E} (hf : ) (hg : ) :
UniformConcaveOn s (φ + ψ) (f - g)
def StrongConvexOn {E : Type u_1} [] (s : Set E) (m : ) :
(E)Prop

A function f from a real normed space is m-strongly convex if it is uniformly convex with modulus φ(r) = m / 2 * r ^ 2.

In an inner product space, this is equivalent to x ↦ f x - m / 2 * ‖x‖ ^ 2 being convex.

Equations
Instances For
def StrongConcaveOn {E : Type u_1} [] (s : Set E) (m : ) :
(E)Prop

A function f from a real normed space is m-strongly concave if is strongly concave with modulus φ(r) = m / 2 * r ^ 2.

In an inner product space, this is equivalent to x ↦ f x + m / 2 * ‖x‖ ^ 2 being concave.

Equations
Instances For
theorem StrongConvexOn.mono {E : Type u_1} [] {s : Set E} {f : E} {m : } {n : } (hmn : m n) (hf : ) :
theorem StrongConcaveOn.mono {E : Type u_1} [] {s : Set E} {f : E} {m : } {n : } (hmn : m n) (hf : ) :
@[simp]
theorem strongConvexOn_zero {E : Type u_1} [] {s : Set E} {f : E} :
@[simp]
theorem strongConcaveOn_zero {E : Type u_1} [] {s : Set E} {f : E} :
theorem StrongConvexOn.strictConvexOn {E : Type u_1} [] {s : Set E} {f : E} {m : } (hf : ) (hm : 0 < m) :
theorem StrongConcaveOn.strictConcaveOn {E : Type u_1} [] {s : Set E} {f : E} {m : } (hf : ) (hm : 0 < m) :
theorem strongConvexOn_iff_convex {E : Type u_1} [] {s : Set E} {m : } {f : E} :
ConvexOn s fun (x : E) => f x - m / 2 * x ^ 2
theorem strongConcaveOn_iff_convex {E : Type u_1} [] {s : Set E} {m : } {f : E} :
ConcaveOn s fun (x : E) => f x + m / 2 * x ^ 2