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} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) (φ : ℝ → ℝ) (f : E → ℝ) : Prop

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.

def UniformConcaveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) (φ : ℝ → ℝ) (f : E → ℝ) : Prop

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.

@[simp]

theorem uniformConvexOn_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} : UniformConvexOn s 0 f ↔ ConvexOn ℝ s f

@[simp]

theorem uniformConcaveOn_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} : UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f

theorem ConvexOn.uniformConvexOn_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} : ConvexOn ℝ s f → UniformConvexOn s 0 f

Alias of the reverse direction of uniformConvexOn_zero.

theorem ConcaveOn.uniformConcaveOn_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} : ConcaveOn ℝ s f → UniformConcaveOn s 0 f

Alias of the reverse direction of uniformConcaveOn_zero.

theorem UniformConvexOn.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hψφ : ψ ≤ φ) (hf : UniformConvexOn s φ f) : UniformConvexOn s ψ f

theorem UniformConcaveOn.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hψφ : ψ ≤ φ) (hf : UniformConcaveOn s φ f) : UniformConcaveOn s ψ f

theorem UniformConvexOn.convexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hf : UniformConvexOn s φ f) (hφ : 0 ≤ φ) : ConvexOn ℝ s f

theorem UniformConcaveOn.concaveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hf : UniformConcaveOn s φ f) (hφ : 0 ≤ φ) : ConcaveOn ℝ s f

theorem UniformConvexOn.strictConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hf : UniformConvexOn s φ f) (hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r) : StrictConvexOn ℝ s f

theorem UniformConcaveOn.strictConcaveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hf : UniformConcaveOn s φ f) (hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r) : StrictConcaveOn ℝ s f

theorem UniformConvexOn.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ} {g : E → ℝ} (hf : UniformConvexOn s φ f) (hg : UniformConvexOn s ψ g) : UniformConvexOn s (φ + ψ) (f + g)

theorem UniformConcaveOn.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ} {g : E → ℝ} (hf : UniformConcaveOn s φ f) (hg : UniformConcaveOn s ψ g) : UniformConcaveOn s (φ + ψ) (f + g)

theorem UniformConvexOn.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hf : UniformConvexOn s φ f) : UniformConcaveOn s φ (-f)

theorem UniformConcaveOn.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ} (hf : UniformConcaveOn s φ f) : UniformConvexOn s φ (-f)

theorem UniformConvexOn.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ} {g : E → ℝ} (hf : UniformConvexOn s φ f) (hg : UniformConcaveOn s ψ g) : UniformConvexOn s (φ + ψ) (f - g)

theorem UniformConcaveOn.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ℝ → ℝ} {ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ} {g : E → ℝ} (hf : UniformConcaveOn s φ f) (hg : UniformConvexOn s ψ g) : UniformConcaveOn s (φ + ψ) (f - g)

def StrongConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (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

• StrongConvexOn s m = UniformConvexOn s fun (r : ℝ) => m / 2 * r ^ 2

def StrongConcaveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (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

• StrongConcaveOn s m = UniformConcaveOn s fun (r : ℝ) => m / 2 * r ^ 2

theorem StrongConvexOn.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m : ℝ} {n : ℝ} (hmn : m ≤ n) (hf : StrongConvexOn s n f) : StrongConvexOn s m f

theorem StrongConcaveOn.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m : ℝ} {n : ℝ} (hmn : m ≤ n) (hf : StrongConcaveOn s n f) : StrongConcaveOn s m f

@[simp]

theorem strongConvexOn_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} : StrongConvexOn s 0 f ↔ ConvexOn ℝ s f

@[simp]

theorem strongConcaveOn_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} : StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f

theorem StrongConvexOn.strictConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m : ℝ} (hf : StrongConvexOn s m f) (hm : 0 < m) : StrictConvexOn ℝ s f

theorem StrongConcaveOn.strictConcaveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m : ℝ} (hf : StrongConcaveOn s m f) (hm : 0 < m) : StrictConcaveOn ℝ s f

theorem strongConvexOn_iff_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {m : ℝ} {f : E → ℝ} : StrongConvexOn s m f ↔ ConvexOn ℝ s fun (x : E) => f x - m / 2 * ‖x‖ ^ 2

theorem strongConcaveOn_iff_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {m : ℝ} {f : E → ℝ} : StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun (x : E) => f x + m / 2 * ‖x‖ ^ 2