def epigraph {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : Set ((Fin n → ℝ) × ℝ)

Definition 4.1: Let f be a function with values in R union {plus or minus infinity} whose domain is a subset S of R^n. The set {(x, mu) | x in S, mu in R, mu >= f x} is called the epigraph of f, denoted epi f.

Equations

• epigraph S f = {p : (Fin n → ℝ) × ℝ | S p.1 ∧ f p.1 ≤ ↑p.2}

def ConvexFunctionOn {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : Prop

Definition 4.2: A function f on S is a convex function if epi f is convex as a subset of R^{n+1}.

Equations

• ConvexFunctionOn S f = Convex ℝ (epigraph S f)

theorem epigraph_mem_of_le_aux {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} (hx : x ∈ S) (hμ : f x ≤ ↑μ) : (x, μ) ∈ epigraph S f

If x ∈ S and f x ≤ μ, then (x, μ) belongs to the epigraph.

theorem convex_combo_mem_epigraph_aux {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {μ v t : ℝ} (hconv : Convex ℝ (epigraph S f)) (hx : (x, μ) ∈ epigraph S f) (hy : (y, v) ∈ epigraph S f) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (1 - t) • (x, μ) + t • (y, v) ∈ epigraph S f

Convexity of the epigraph yields convex combinations of its points.

theorem epigraph_combo_proj_aux {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {μ v t : ℝ} : (1 - t) • (x, μ) + t • (y, v) ∈ epigraph S f → (1 - t) • x + t • y ∈ S ∧ f ((1 - t) • x + t • y) ≤ ↑((1 - t) * μ + t * v)

Unpack epigraph membership of a convex combination.

theorem epigraph_combo_ineq_aux {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {μ v t : ℝ} (hconv : Convex ℝ (epigraph S f)) (hx : x ∈ S) (hy : y ∈ S) (hμ : f x ≤ ↑μ) (hv : f y ≤ ↑v) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : f ((1 - t) • x + t • y) ≤ ↑((1 - t) * μ + t * v)

Convexity of the epigraph gives a real upper bound along segments.

theorem convexFunctionOn_iff_segment_inequality {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} (hC : Convex ℝ C) (hnotbot : ∀ x ∈ C, f x ≠ ⊥) : ConvexFunctionOn C f ↔ ∀ x ∈ C, ∀ y ∈ C, ∀ (t : ℝ), 0 < t → t < 1 → f ((1 - t) • x + t • y) ≤ ↑(1 - t) * f x + ↑t * f y

Theorem 4.1: Let f be a function from C to (-∞, +∞], where C is convex. Then f is convex on C iff f ((1 - λ) • x + λ • y) ≤ (1 - λ) * f x + λ * f y for 0 < λ < 1, for every x and y in C.

theorem ereal_exists_real_between_of_lt {u : EReal} {α : ℝ} (h : u < ↑α) : ∃ (μ : ℝ), u ≤ ↑μ ∧ μ < α

Choose a real bound between an EReal value and a real upper bound.

theorem ereal_convex_combo_lt_of_lt {μ α v β t : ℝ} (hμ : μ < α) (hv : v < β) (ht0 : 0 < t) (ht1 : t < 1) : ↑(1 - t) * ↑μ + ↑t * ↑v < ↑(1 - t) * ↑α + ↑t * ↑β

Strict inequality for convex combinations of real bounds in EReal.

theorem segment_inequality_le_of_strict {n : ℕ} {f : (Fin n → ℝ) → EReal} (hstrict : ∀ (x y : Fin n → ℝ) (α β t : ℝ), f x < ↑α → f y < ↑β → 0 < t → t < 1 → f ((1 - t) • x + t • y) < ↑(1 - t) * ↑α + ↑t * ↑β) (x y : Fin n → ℝ) (μ v t : ℝ) : f x ≤ ↑μ → f y ≤ ↑v → 0 < t → t < 1 → f ((1 - t) • x + t • y) ≤ ↑((1 - t) * μ + t * v)

Strict segment bounds yield a non-strict bound with real upper bounds.

theorem convexFunctionOn_univ_iff_strict_inequality {n : ℕ} {f : (Fin n → ℝ) → EReal} : ConvexFunctionOn Set.univ f ↔ ∀ (x y : Fin n → ℝ) (α β t : ℝ), f x < ↑α → f y < ↑β → 0 < t → t < 1 → f ((1 - t) • x + t • y) < ↑(1 - t) * ↑α + ↑t * ↑β

Theorem 4.2: Let f be a function from ℝ^n to [-∞, +∞]. Then f is convex iff f ((1 - λ) • x + λ • y) < (1 - λ) * α + λ * β for 0 < λ < 1, whenever f x < α and f y < β.

theorem EReal.mul_sum_of_nonneg_of_ne_top {α : Type u_1} {s : Finset α} {a : EReal} (ha : 0 ≤ a) (ha_top : a ≠ ⊤) (f : α → EReal) : a * s.sum f = ∑ i ∈ s, a * f i

Distribute a finite nonnegative scalar over a finite EReal sum.

theorem tail_weights_zero_of_head_eq_one {m : ℕ} {w : Fin (m + 1) → ℝ} (hw : ∀ (i : Fin (m + 1)), 0 ≤ w i) (hsum : ∑ i : Fin (m + 1), w i = 1) (h0 : w 0 = 1) (i : Fin m) : w i.succ = 0

If nonnegative weights sum to one and the head weight is one, all tail weights vanish.

theorem jensen_inequality_of_convexFunctionOn_univ {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) (hnotbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (m : ℕ) (w : Fin m → ℝ) (x : Fin m → Fin n → ℝ) : (∀ (i : Fin m), 0 ≤ w i) → ∑ i : Fin m, w i = 1 → f (∑ i : Fin m, w i • x i) ≤ ∑ i : Fin m, ↑(w i) * f (x i)

Jensen inequality from convexity on the whole space.

theorem segment_inequality_of_jensen {n : ℕ} {f : (Fin n → ℝ) → EReal} (hjensen : ∀ (m : ℕ) (w : Fin m → ℝ) (x : Fin m → Fin n → ℝ), (∀ (i : Fin m), 0 ≤ w i) → ∑ i : Fin m, w i = 1 → f (∑ i : Fin m, w i • x i) ≤ ∑ i : Fin m, ↑(w i) * f (x i)) (x y : Fin n → ℝ) (t : ℝ) : 0 < t → t < 1 → f ((1 - t) • x + t • y) ≤ ↑(1 - t) * f x + ↑t * f y

Jensen inequality for m = 2 yields the segment inequality.

theorem convexFunctionOn_univ_iff_jensen_inequality {n : ℕ} (f : (Fin n → ℝ) → EReal) (hnotbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : ConvexFunctionOn Set.univ f ↔ ∀ (m : ℕ) (w : Fin m → ℝ) (x : Fin m → Fin n → ℝ), (∀ (i : Fin m), 0 ≤ w i) → ∑ i : Fin m, w i = 1 → f (∑ i : Fin m, w i • x i) ≤ ∑ i : Fin m, ↑(w i) * f (x i)

Theorem 4.3 (Jensen's Inequality): Let f be a function from R^n to (-∞, +∞]. Then f is convex iff f (lambda_1 x_1 + ... + lambda_m x_m) ≤ lambda_1 f x_1 + ... + lambda_m f x_m whenever lambda_1, ..., lambda_m ≥ 0 and lambda_1 + ... + lambda_m = 1.

def AffineFunctionOn {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : Prop

Definition 4.3: An affine function on S is a function which is finite, convex, and concave.

Equations

• AffineFunctionOn S f = ((∀ x ∈ S, f x ≠ ⊥ ∧ f x ≠ ⊤) ∧ ConvexFunctionOn S f ∧ Convex ℝ {p : (Fin n → ℝ) × ℝ | p.1 ∈ S ∧ ↑p.2 ≤ f p.1})

theorem derivWithin_Ioo_eq_deriv {g : ℝ → ℝ} {α β x : ℝ} (hx : x ∈ Set.Ioo α β) : derivWithin g (Set.Ioo α β) x = deriv g x

On an open interval, the derivative within equals the usual derivative.

theorem convexOn_Ioo_of_second_deriv_nonneg {f : ℝ → ℝ} {α β : ℝ} (hcont : ContDiffOn ℝ 2 f (Set.Ioo α β)) (hderiv2 : ∀ x ∈ Set.Ioo α β, 0 ≤ deriv (deriv f) x) : ConvexOn ℝ (Set.Ioo α β) f

Nonnegative second derivative implies convexity on an open interval.

theorem second_deriv_nonneg_of_convexOn_Ioo {f : ℝ → ℝ} {α β : ℝ} (hcont : ContDiffOn ℝ 2 f (Set.Ioo α β)) (hconv : ConvexOn ℝ (Set.Ioo α β) f) (x : ℝ) : x ∈ Set.Ioo α β → 0 ≤ deriv (deriv f) x

Convexity on an open interval forces a nonnegative second derivative.

theorem convexOn_interval_iff_second_deriv_nonneg {f : ℝ → ℝ} {α β : ℝ} (hcont : ContDiffOn ℝ 2 f (Set.Ioo α β)) : ConvexOn ℝ (Set.Ioo α β) f ↔ ∀ x ∈ Set.Ioo α β, 0 ≤ deriv (deriv f) x

Theorem 4.4: Let f be a twice continuously differentiable real-valued function on an open interval (α, β). Then f is convex iff its second derivative f'' is nonnegative throughout (α, β).

theorem contDiffOn_line_restrict {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hcont : ContDiffOn ℝ 2 f C) {y z : Fin n → ℝ} {a b : ℝ} (hmem : ∀ t ∈ Set.Ioo a b, y + t • z ∈ C) : ContDiffOn ℝ 2 (fun (t : ℝ) => f (y + t • z)) (Set.Ioo a b)

Restricting a C^2 function to a line is C^2 on any interval contained in C.

theorem exists_line_interval_subset {n : ℕ} {C : Set (Fin n → ℝ)} (hopen : IsOpen C) {x : Fin n → ℝ} (hx : x ∈ C) (z : Fin n → ℝ) : ∃ (ε : ℝ), 0 < ε ∧ ∀ t ∈ Set.Ioo (-ε) ε, x + t • z ∈ C

An open set contains a small open interval of a line through any point.

theorem convexOn_line_restrict {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hconv : ConvexOn ℝ C f) {y z : Fin n → ℝ} {a b : ℝ} (hmem : ∀ t ∈ Set.Ioo a b, y + t • z ∈ C) : ConvexOn ℝ (Set.Ioo a b) fun (t : ℝ) => f (y + t • z)

Convexity of a function on C implies convexity of its restriction to any line segment in C.

noncomputable def hessianMatrix {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

The Hessian matrix defined by iterated coordinate derivatives.

Equations

• hessianMatrix f x i j = deriv (fun (t : ℝ) => deriv (fun (s : ℝ) => f (x + s • Pi.single i 1 + t • Pi.single j 1)) 0) 0

theorem posSemidef_iff_real {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : M.PosSemidef ↔ M.IsHermitian ∧ ∀ (x : Fin n → ℝ), 0 ≤ x ⬝ᵥ M.mulVec x

Over ℝ, the quadratic form in Matrix.PosSemidef uses no conjugation.

theorem line_deriv_eq_fderiv {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y z : Fin n → ℝ} {t : ℝ} (hderiv : DifferentiableAt ℝ f (y + t • z)) : deriv (fun (s : ℝ) => f (y + s • z)) t = (fderiv ℝ f (y + t • z)) z

Derivative along a line equals the Fréchet derivative applied to the direction.

theorem hessian_entry_eq_fderiv {n : ℕ} {f : (Fin n → ℝ) → ℝ} {x : Fin n → ℝ} (hcont : ContDiffAt ℝ 2 f x) (i j : Fin n) : hessianMatrix f x i j = ((fderiv ℝ (fderiv ℝ f) x) (Pi.single i 1)) (Pi.single j 1)

Coordinate second derivatives match the second Fréchet derivative on basis vectors.

theorem line_second_deriv_eq_quadratic_form {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hopen : IsOpen C) (hcont : ContDiffOn ℝ 2 f C) {y z : Fin n → ℝ} {t : ℝ} (ht : y + t • z ∈ C) : deriv (deriv fun (s : ℝ) => f (y + s • z)) t = star z ⬝ᵥ (hessianMatrix f (y + t • z)).mulVec z

Second derivatives along lines are given by the Hessian quadratic form.

theorem hessian_symm {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hopen : IsOpen C) (hcont : ContDiffOn ℝ 2 f C) {x : Fin n → ℝ} (hx : x ∈ C) : (hessianMatrix f x).IsHermitian

The Hessian matrix is Hermitian at points of an open C^2 set.

theorem hessian_posSemidef_of_convexOn {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hopen : IsOpen C) (hcont : ContDiffOn ℝ 2 f C) (hconv : ConvexOn ℝ C f) (x : Fin n → ℝ) : x ∈ C → (hessianMatrix f x).PosSemidef

Convexity implies positive semidefiniteness of the Hessian.

theorem convexOn_of_hessian_posSemidef {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC : Convex ℝ C) (hopen : IsOpen C) (hcont : ContDiffOn ℝ 2 f C) (hpos : ∀ x ∈ C, (hessianMatrix f x).PosSemidef) : ConvexOn ℝ C f

Positive semidefinite Hessian implies convexity.

theorem convexOn_iff_hessian_posSemidef {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC : Convex ℝ C) (hopen : IsOpen C) (hcont : ContDiffOn ℝ 2 f C) : ConvexOn ℝ C f ↔ ∀ x ∈ C, Matrix.PosSemidef fun (i j : Fin n) => deriv (fun (t : ℝ) => deriv (fun (s : ℝ) => f (x + s • Pi.single i 1 + t • Pi.single j 1)) 0) 0

Theorem 4.5: Let f be a twice continuously differentiable real-valued function on an open convex set C in ℝ^n. Then f is convex on C iff its Hessian matrix Q_x = (q_ij(x)) with q_ij(x) = ∂^2 f / ∂ ξ_i ∂ ξ_j (x) is positive semidefinite for every x ∈ C.

theorem convexFunctionOn_of_convexOn_real {n : ℕ} {S : Set (Fin n → ℝ)} {g : (Fin n → ℝ) → ℝ} (hg : ConvexOn ℝ S g) : ConvexFunctionOn S fun (x : Fin n → ℝ) => ↑(g x)

Lift real convexity to ConvexFunctionOn for finite-valued functions.

theorem convexFunctionOn_univ_if_top {n : ℕ} {C : Set (Fin n → ℝ)} {g : (Fin n → ℝ) → ℝ} (hg : ConvexOn ℝ C g) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => if x ∈ C then ↑(g x) else ⊤

Extending by ⊤ outside a convex domain preserves convexity on Set.univ.

theorem convexOn_comp_proj {s : Set ℝ} {f : ℝ → ℝ} (hf : ConvexOn ℝ s f) : ConvexOn ℝ (⇑(LinearMap.proj 0) ⁻¹' s) fun (x : Fin 1 → ℝ) => f (x 0)

Pull back convexity along the coordinate projection on Fin 1.

theorem convexOn_rpow_Ioi_of_nonpos {p : ℝ} (hp : p ≤ 0) : ConvexOn ℝ (Set.Ioi 0) fun (x : ℝ) => x ^ p

x ↦ x^p is convex on (0, ∞) for p ≤ 0.

theorem antitoneOn_rpow_Ioi_of_nonpos {p : ℝ} (hp : p ≤ 0) : AntitoneOn (fun (x : ℝ) => x ^ p) (Set.Ioi 0)

x ↦ x^p is antitone on (0, ∞) for p ≤ 0.

theorem concaveOn_sub_sq_Ioo (a : ℝ) : ConcaveOn ℝ (Set.Ioo (-a) a) fun (x : ℝ) => a ^ 2 - x ^ 2

x ↦ a^2 - x^2 is concave on (-a, a).

theorem image_sub_sq_Ioo {a : ℝ} (ha : 0 < a) : (fun (x : ℝ) => a ^ 2 - x ^ 2) '' Set.Ioo (-a) a = Set.Ioc 0 (a ^ 2)

Image of x ↦ a^2 - x^2 on (-a, a) is (0, a^2].

theorem convexFunctionOn_example_functions : (∀ (a : ℝ), ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => ↑(Real.exp (a * x 0))) ∧ (∀ (p : ℝ), 1 ≤ p → ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => if 0 ≤ x 0 then ↑((x 0).rpow p) else ⊤) ∧ (∀ (p : ℝ), 0 ≤ p → p ≤ 1 → ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => if 0 ≤ x 0 then ↑(-(x 0).rpow p) else ⊤) ∧ (∀ p ≤ 0, ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => if 0 < x 0 then ↑((x 0).rpow p) else ⊤) ∧ (∀ (a : ℝ), 0 < a → ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => if |x 0| < a then ↑((a ^ 2 - x 0 ^ 2).rpow (-(1 / 2))) else ⊤) ∧ ConvexFunctionOn Set.univ fun (x : Fin 1 → ℝ) => if 0 < x 0 then ↑(-Real.log (x 0)) else ⊤

Example 4.4.1: Here are some functions on Real whose convexity is a consequence of Theorem 4.4: (i) f(x) = exp(alpha * x) for -infty < alpha < infty; (ii) f(x) = x^p if x >= 0, f(x) = infty if x < 0, where 1 <= p < infty; (iii) f(x) = -x^p if x >= 0, f(x) = infty if x < 0, where 0 <= p <= 1; (iv) f(x) = x^p if x > 0, f(x) = infty if x <= 0, where -infty < p <= 0; (v) f(x) = (alpha^2 - x^2)^(-1/2) if |x| < alpha, f(x) = infty if |x| >= alpha, where alpha > 0; (vi) f(x) = -log x if x > 0, f(x) = infty if x <= 0.

def effectiveDomain {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : Set (Fin n → ℝ)

Definition 4.4: The effective domain of a convex function f on S, denoted dom f, is the projection of epi f onto R^n; equivalently, dom f = {x | ∃ μ, (x, μ) ∈ epi f} = {x | f x < +infty}.

Equations

• effectiveDomain S f = {x : Fin n → ℝ | ∃ (μ : ℝ), (x, μ) ∈ epigraph S f}

theorem effectiveDomain_eq {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : effectiveDomain S f = {x : Fin n → ℝ | x ∈ S ∧ f x < ⊤}

theorem effectiveDomain_eq_image_fst {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : effectiveDomain S f = ⇑(LinearMap.fst ℝ (Fin n → ℝ) ℝ) '' epigraph S f

The effective domain is the projection of the epigraph onto the first coordinate.

theorem convex_image_fst_epigraph {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn S f) : Convex ℝ (⇑(LinearMap.fst ℝ (Fin n → ℝ) ℝ) '' epigraph S f)

The image of the epigraph under the first projection is convex.