theorem convexOn_closure_of_continuousOn {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hconv : ConvexOn ℝ C f) (hcont : ContinuousOn f (closure C)) : ConvexOn ℝ (closure C) f

Extend convexity to the closure under continuity.

theorem convexOn_negGeomMean_nonneg {n : ℕ} (hn : n ≠ 0) : ConvexOn ℝ {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i} fun (x : Fin n → ℝ) => -(∏ i : Fin n, x i).rpow (1 / ↑n)

Convexity of the negative geometric mean on the nonnegative orthant.

theorem effectiveDomain_negativeGeometricMean {n : ℕ} : (effectiveDomain Set.univ fun (x : Fin n → ℝ) => if ∀ (i : Fin n), 0 ≤ x i then -↑((∏ i : Fin n, x i).rpow (1 / ↑n)) else ⊤) = {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i}

The effective domain of the negative geometric mean is the nonnegative orthant.

theorem convexFunction_negativeGeometricMean {n : ℕ} : have f := fun (x : Fin n → ℝ) => if ∀ (i : Fin n), 0 ≤ x i then -↑((∏ i : Fin n, x i).rpow (1 / ↑n)) else ⊤; ConvexFunction f

theorem convexOn_univ_euclidean_norm {n : ℕ} : ConvexOn ℝ Set.univ fun (x : EuclideanSpace ℝ (Fin n)) => ‖x‖

Remark 4.5.3: One of the most important convex functions on ℝ^n is the Euclidean norm |x| = ⟪x, x⟫^{1/2} = (xi_1^2 + ... + xi_n^2)^{1/2}.

theorem euclidean_norm_eq_abs (x : ℝ) : ‖x‖ = |x|

Remark 4.5.3: This Euclidean norm is the absolute value when n = 1.

theorem convex_sublevel_lt_real_of_convexFunction {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (r : ℝ) : Convex ℝ {x : Fin n → ℝ | f x < ↑r}

Strict real sublevel sets of a convex function are convex.

theorem convex_sublevel_lt_top_of_convexFunction {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) : Convex ℝ {x : Fin n → ℝ | f x < ⊤}

The strict sublevel at ⊤ is the effective domain, hence convex.

theorem sublevel_le_eq_iInter_lt_real {n : ℕ} {f : (Fin n → ℝ) → EReal} (α : EReal) : {x : Fin n → ℝ | f x ≤ α} = ⋂ (β : { β : ℝ // α < ↑β }), {x : Fin n → ℝ | f x < ↑↑β}

A non-strict sublevel is the intersection of strict real sublevels above it.

theorem convexFunction_level_sets_convex {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (α : EReal) : Convex ℝ {x : Fin n → ℝ | f x < α} ∧ Convex ℝ {x : Fin n → ℝ | f x ≤ α}

Theorem 4.6: For any convex function f and any α ∈ [-∞, +∞], the level sets {x | f x < α} and {x | f x ≤ α} are convex.

theorem convex_quadratic_inequality_set {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} {a : Fin n → ℝ} {α : ℝ} (hQ : Q.PosSemidef) : Convex ℝ {x : Fin n → ℝ | 1 / 2 * x ⬝ᵥ Q.mulVec x + x ⬝ᵥ a + α ≤ 0}

Remark 4.6.1: Taking f to be a quadratic convex function in Theorem 4.6, the set {x | (1/2) ⟪x, Q x⟫ + ⟪x, a⟫ + α ≤ 0} is convex when Q is positive semidefinite (Theorem 4.5). Sets of this form include solid ellipsoids and paraboloids, in particular the ball {x | ⟪x, x⟫ ≤ 1}.

theorem convex_iInter_sublevel_sets {n : ℕ} {I : Type u_1} (f : I → (Fin n → ℝ) → EReal) (α : I → ℝ) (hf : ∀ (i : I), ConvexFunction (f i)) : Convex ℝ {x : Fin n → ℝ | ∀ (i : I), f i x ≤ ↑(α i)}

Corollary 4.6.1: Let f_i be a convex function on ℝ^n and α_i be a real number for each i ∈ I. Then C = {x | f_i(x) ≤ α_i, ∀ i ∈ I} is a convex set.

theorem convexity_inequality_analysis {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (hnotbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (β : EReal) {I : Type u_1} (g : I → (Fin n → ℝ) → EReal) (α : I → ℝ) (hg : ∀ (i : I), ConvexFunction (g i)) : (Convex ℝ {x : Fin n → ℝ | f x < β} ∧ Convex ℝ {x : Fin n → ℝ | f x ≤ β}) ∧ Convex ℝ {x : Fin n → ℝ | ∀ (i : I), g i x ≤ ↑(α i)} ∧ ∀ (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)

Remark 4.6.2: Theorem 4.6 and Corollary 4.6.1 are significant for systems of nonlinear inequalities. Convexity also enters other aspects of inequality theory, since various classical inequalities can be regarded as special cases of Theorem 4.3.

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

Definition 4.6: A convex function f is proper if its epigraph is nonempty and contains no vertical lines (equivalently, f x ≠ ⊥ for all x ∈ S).

Equations

• ProperConvexFunctionOn S f = (ConvexFunctionOn S f ∧ (epigraph S f).Nonempty ∧ ∀ x ∈ S, f x ≠ ⊥)

theorem nonempty_epigraph_iff_nonempty_effectiveDomain {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : (epigraph S f).Nonempty ↔ (effectiveDomain S f).Nonempty

The epigraph is nonempty iff the effective domain is nonempty.

theorem mem_effectiveDomain_imp_ne_top {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} : x ∈ effectiveDomain S f → f x ≠ ⊤

Points in the effective domain have value different from ⊤.

theorem not_mem_effectiveDomain_imp_ne_bot {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hxS : x ∈ S) (hx : x ∉ effectiveDomain S f) : f x ≠ ⊥

Points in S outside the effective domain cannot take value ⊥.

theorem properConvexFunctionOn_iff_effectiveDomain_nonempty_finite {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : ProperConvexFunctionOn S f ↔ ConvexFunctionOn S f ∧ (effectiveDomain S f).Nonempty ∧ ∀ x ∈ effectiveDomain S f, f x ≠ ⊥ ∧ f x ≠ ⊤

Remark 4.6.1: f is proper iff the convex set C = dom f is nonempty and the restriction of f to C is finite; equivalently, a proper convex function on ℝ^n comes from a finite convex function on a nonempty convex set C and is extended by f x = +∞ outside C.

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

Definition 4.7: A convex function which is not proper is improper.

Equations

• ImproperConvexFunctionOn S f = (ConvexFunctionOn S f ∧ ¬ProperConvexFunctionOn S f)

theorem improperConvexExample : have f := fun (x : Fin 1 → ℝ) => if |x 0| < 1 then ⊥ else if |x 0| = 1 then ↑0 else ⊤; ImproperConvexFunctionOn Set.univ f ∧ (¬∀ (x : Fin 1 → ℝ), f x = ⊤) ∧ ¬∀ (x : Fin 1 → ℝ), f x = ⊥

Example 4.7.2: An improper convex function on ℝ that is not identically +∞ or -∞ is given by f x = -∞ if |x| < 1, f x = 0 if |x| = 1, and f x = +∞ if |x| > 1.

def PositivelyHomogeneous {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop

Definition 4.8: A function f on ℝ^n is positively homogeneous (of degree 1) if for every x and every λ with 0 < λ, one has f (λ • x) = λ * f x.

Equations

• PositivelyHomogeneous f = ∀ (x : Fin n → ℝ) (t : ℝ), 0 < t → f (t • x) = ↑t * f x

theorem subadditive_of_convex_posHom {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hconv : ConvexFunction f) (hnotbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (x y : Fin n → ℝ) : f (x + y) ≤ f x + f y

A convex positively homogeneous function is subadditive.

theorem segment_inequality_of_subadditive_posHom {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hsub : ∀ (x y : Fin n → ℝ), f (x + y) ≤ f x + f y) (x y : Fin n → ℝ) (t : ℝ) : 0 < t → t < 1 → f ((1 - t) • x + t • y) ≤ ↑(1 - t) * f x + ↑t * f y

Subadditivity and positive homogeneity yield the segment inequality.

theorem convex_of_subadditive_posHom {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hsub : ∀ (x y : Fin n → ℝ), f (x + y) ≤ f x + f y) (hnotbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : ConvexFunction f

Subadditivity and positive homogeneity imply convexity.

theorem convexFunction_iff_subadditive_of_posHom {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hnotbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : ConvexFunction f ↔ ∀ (x y : Fin n → ℝ), f (x + y) ≤ f x + f y

Theorem 4.7: A positively homogeneous function f from R^n to (-∞, +∞] is convex iff f (x + y) ≤ f x + f y for every x and y in R^n.

theorem convexFunction_jensen_inequality_of_posHom_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) (m : ℕ) : m ≠ 0 → ∀ (w : Fin m → ℝ) (x : Fin m → Fin n → ℝ), (∀ (i : Fin m), 0 < w i) → f (∑ i : Fin m, w i • x i) ≤ ∑ i : Fin m, ↑(w i) * f (x i)

Corollary 4.7.1: If f is a positively homogeneous proper convex function, then f (lambda_1 x_1 + ... + lambda_m x_m) ≤ lambda_1 f x_1 + ... + lambda_m f x_m whenever lambda_1 > 0, ..., lambda_m > 0.

theorem posHom_zero_nonneg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) : 0 ≤ f 0

For a positively homogeneous proper convex function, f 0 is nonnegative.

theorem subadditive_of_posHom_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) (x y : Fin n → ℝ) : f (x + y) ≤ f x + f y

Proper convexity plus positive homogeneity yield subadditivity.

theorem ereal_neg_le_of_add_nonneg {a b : EReal} (ha : a ≠ ⊥) (hb : b ≠ ⊥) (h : 0 ≤ a + b) : -a ≤ b

A nonnegative sum gives a lower bound on the second term.

theorem convexFunction_neg_ge_neg_of_posHom_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) (x : Fin n → ℝ) : f (-x) ≥ -f x

Corollary 4.7.2: If f is a positively homogeneous proper convex function, then f (-x) ≥ -f x for every x.

theorem ne_top_of_neg_eq_neg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hproper : ProperConvexFunctionOn Set.univ f) {x : Fin n → ℝ} (hneg : f (-x) = -f x) : f x ≠ ⊤

Oddness at a point rules out the value ⊤.

theorem coe_toReal_of_neg_eq_neg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hproper : ProperConvexFunctionOn Set.univ f) {x : Fin n → ℝ} (hneg : f (-x) = -f x) : ↑(f x).toReal = f x

Under oddness at x, f x can be rewritten as a real.

theorem posHom_all_real_of_neg_vec {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) {v : Fin n → ℝ} (hnegv : f (-v) = -f v) (t : ℝ) : f (t • v) = ↑t * f v

Oddness at a vector extends positive homogeneity to all real scalars.

theorem additive_on_L_of_neg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) {L : Submodule ℝ (Fin n → ℝ)} (hneg : ∀ (x : ↥L), f (-↑x) = -f ↑x) (x y : ↥L) : f ↑(x + y) = f ↑x + f ↑y

Oddness on a submodule yields additivity there.

theorem linear_map_of_neg_on_L {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) {L : Submodule ℝ (Fin n → ℝ)} (hneg : ∀ (x : ↥L), f (-↑x) = -f ↑x) : ∃ (g : ↥L →ₗ[ℝ] ℝ), ∀ (x : ↥L), f ↑x = ↑(g x)

Oddness on a submodule yields a linear map representing f there.

theorem subadditive_finset_of_posHom_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) (hzero : f 0 = 0) {ι : Type u_1} (s : Finset ι) (g : ι → Fin n → ℝ) : f (s.sum g) ≤ ∑ i ∈ s, f (g i)

Subadditivity extends to finite sums for positively homogeneous proper convex functions.

theorem ereal_sum_coe {ι : Type u_1} (s : Finset ι) (r : ι → ℝ) : ∑ i ∈ s, ↑(r i) = ↑(s.sum r)

A finite sum of real-coe values in EReal is the coe of the real sum.

theorem neg_on_L_of_basis_neg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) {L : Submodule ℝ (Fin n → ℝ)} {ι : Type u_1} [Fintype ι] [Nonempty ι] (b : Module.Basis ι ℝ ↥L) (hnegb : ∀ (i : ι), f (-↑(b i)) = -f ↑(b i)) (x : ↥L) : f (-↑x) = -f ↑x

Oddness on a basis implies oddness on all of the submodule.

theorem positivelyHomogeneous_properConvex_linear_on_submodule_iff_neg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (hproper : ProperConvexFunctionOn Set.univ f) (L : Submodule ℝ (Fin n → ℝ)) : ((∃ (g : ↥L →ₗ[ℝ] ℝ), ∀ (x : ↥L), f ↑x = ↑(g x)) ↔ ∀ (x : ↥L), f (-↑x) = -f ↑x) ∧ ((∃ (ι : Type u_1) (x : Fintype ι) (_ : Nonempty ι) (b : Module.Basis ι ℝ ↥L), ∀ (i : ι), f (-↑(b i)) = -f ↑(b i)) → ∃ (g : ↥L →ₗ[ℝ] ℝ), ∀ (x : ↥L), f ↑x = ↑(g x))

Theorem 4.8: A positively homogeneous proper convex function f is linear on a subspace L iff f (-x) = -f x for every x ∈ L. This is true if merely f (-b_i) = -f b_i for all vectors in some basis b_1, ..., b_m for L.

theorem mem_epigraph_univ_iff {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} : (x, μ) ∈ epigraph Set.univ f ↔ f x ≤ ↑μ

Membership in the epigraph over Set.univ is just the inequality.

theorem ereal_eq_bot_of_le_all_coe {x : EReal} (h : ∀ (μ : ℝ), x ≤ ↑μ) : x = ⊥

An extended real bounded above by every real is ⊥.

theorem ereal_mul_le_mul_of_pos_left {t : ℝ} (ht : 0 < t) {x : EReal} {μ : ℝ} (hx : x ≤ ↑μ) : ↑t * x ≤ ↑(t * μ)

Multiplying by a positive real preserves order against a real upper bound.

theorem epigraph_cone_of_posHom {n : ℕ} {f : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous f) (t : ℝ) : 0 < t → (fun (p : (Fin n → ℝ) × ℝ) => t • p) '' epigraph Set.univ f ⊆ epigraph Set.univ f

Positive homogeneity implies the epigraph is closed under positive scaling.

theorem posHom_of_epigraph_cone {n : ℕ} {f : (Fin n → ℝ) → EReal} (hcone : ∀ (t : ℝ), 0 < t → (fun (p : (Fin n → ℝ) × ℝ) => t • p) '' epigraph Set.univ f ⊆ epigraph Set.univ f) : PositivelyHomogeneous f

The cone property of the epigraph implies positive homogeneity.

theorem positivelyHomogeneous_iff_epigraph_cone {n : ℕ} (f : (Fin n → ℝ) → EReal) : PositivelyHomogeneous f ↔ ∀ (t : ℝ), 0 < t → (fun (p : (Fin n → ℝ) × ℝ) => t • p) '' epigraph Set.univ f ⊆ epigraph Set.univ f

Remark 4.8.1: Obviously, positive homogeneity is equivalent to the epigraph being a cone in ℝ^{n+1}.

theorem posHom_abs_ereal : PositivelyHomogeneous fun (x : Fin 1 → ℝ) => ↑|x 0|

The absolute value is positively homogeneous as an EReal-valued function.

theorem subadditive_abs_ereal (x y : Fin 1 → ℝ) : ↑|x 0 + y 0| ≤ ↑|x 0| + ↑|y 0|

The absolute value is subadditive when coerced to EReal.

theorem abs_not_linear_ereal : ¬∃ (a : ℝ), ∀ (x : Fin 1 → ℝ), ↑|x 0| = ↑(a * x 0)

The absolute value is not linear as an EReal-valued function.

theorem positivelyHomogeneous_convex_abs_not_linear : have f := fun (x : Fin 1 → ℝ) => ↑|x 0|; PositivelyHomogeneous f ∧ ConvexFunction f ∧ ¬∃ (a : ℝ), ∀ (x : Fin 1 → ℝ), f x = ↑(a * x 0)

Example 4.8.2: An example of a positively homogeneous convex function which is not simply a linear function is f(x) = |x|.