theorem improperConvexFunctionOn_exists_bot_of_effectiveDomain_nonempty {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) (hne : (effectiveDomain Set.univ f).Nonempty) : ∃ u ∈ effectiveDomain Set.univ f, f u = ⊥

An improper convex function with nonempty effective domain attains ⊥ there.

theorem affine_combo_inverse {n : ℕ} {u x y : EuclideanSpace ℝ (Fin n)} {μ : ℝ} (hμ : μ ≠ 0) (hy : y = (1 - μ) • u + μ • x) : x = (1 - μ⁻¹) • u + μ⁻¹ • y

Inverting an affine combination on a line.

theorem convex_combo_eq_bot_of_bot_point {n : ℕ} {f : (Fin n → ℝ) → EReal} (hconv : ConvexFunctionOn Set.univ f) {u y x : EuclideanSpace ℝ (Fin n)} (hu : f u.ofLp = ⊥) (hy : f y.ofLp < ⊤) {lam : ℝ} (hlam0 : 0 < lam) (hlam1 : lam < 1) (hx : x = (1 - lam) • u + lam • y) : f x.ofLp = ⊥

A convex combination with a ⊥ point is ⊥ when the other point is finite.

theorem improperConvexFunctionOn_eq_bot_on_ri_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) (x : EuclideanSpace ℝ (Fin n)) : x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f) → f x.ofLp = ⊥

Theorem 7.2: If f is an improper convex function, then f x = -∞ for every x ∈ ri (dom f). Thus an improper convex function is necessarily infinite except perhaps at relative boundary points of its effective domain.

theorem lsc_isClosed_sublevel_bot {n : ℕ} {f : (Fin n → ℝ) → EReal} (hls : LowerSemicontinuous f) : IsClosed {x : Fin n → ℝ | f x ≤ ⊥}

Lower semicontinuity implies the ⊥-sublevel set is closed.

theorem improperConvexFunctionOn_eq_bot_on_closure_ri_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hls : LowerSemicontinuous f) (hf : ImproperConvexFunctionOn Set.univ f) (x : EuclideanSpace ℝ (Fin n)) : x ∈ closure (euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)) → f x.ofLp = ⊥

Lower semicontinuity extends f = ⊥ from ri (dom f) to its closure.

theorem mem_closure_ri_effectiveDomain_of_mem {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) {x : Fin n → ℝ} (hx : x ∈ effectiveDomain Set.univ f) : (EuclideanSpace.equiv (Fin n) ℝ).symm x ∈ closure (euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f))

Points of the effective domain lie in the closure of its relative interior.

theorem lowerSemicontinuous_improperConvexFunction_no_finite_values {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) (hls : LowerSemicontinuous f) (x : Fin n → ℝ) : f x = ⊤ ∨ f x = ⊥

Corollary 7.2.1. A lower semi-continuous improper convex function can have no finite values.

theorem convexFunctionClosure_closed_improperConvexFunctionOn_and_agrees_on_ri {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) : (ClosedConvexFunction (convexFunctionClosure f) ∧ ImproperConvexFunctionOn Set.univ (convexFunctionClosure f)) ∧ ∀ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f), convexFunctionClosure f x.ofLp = f x.ofLp

Corollary 7.2.2. Let f be an improper convex function. Then cl f is a closed improper convex function and agrees with f on ri (dom f).

theorem properConvexFunctionOn_univ_imp_bot_lt {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (x : Fin n → ℝ) : ⊥ < f x

A proper convex function on univ is strictly above ⊥ everywhere.

theorem improperConvexFunctionOn_eq_bot_on_effectiveDomain_of_relOpen {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) (hopen : euclideanRelativelyOpen n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)) (x : Fin n → ℝ) : x ∈ effectiveDomain Set.univ f → f x = ⊥

Relative openness of the effective domain forces ⊥ on it for improper functions.

theorem not_mem_effectiveDomain_univ_imp_eq_top {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hx : x ∉ effectiveDomain Set.univ f) : f x = ⊤

Points outside the effective domain on univ must take value ⊤.

theorem convexFunction_relativelyOpen_effectiveDomain_or_infinite {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (hopen : euclideanRelativelyOpen n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)) : (∀ (x : Fin n → ℝ), ⊥ < f x) ∨ ∀ (x : Fin n → ℝ), f x = ⊤ ∨ f x = ⊥

Corollary 7.2.3. If f is a convex function whose effective domain is relatively open (for instance if effectiveDomain Set.univ f = Set.univ), then either f x > -∞ for every x or f x is infinite for every x.

theorem convexFunctionClosure_agrees_on_ri_of_improper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) (x : EuclideanSpace ℝ (Fin n)) : x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f) → convexFunctionClosure f x.ofLp = f x.ofLp

The closure of an improper convex function agrees with the function on ri (dom f).

theorem epigraph_const_bot_univ {n : ℕ} : (epigraph Set.univ fun (x : Fin n → ℝ) => ⊥) = Set.univ

The epigraph of the constant ⊥ function is all of ℝ^n × ℝ.

theorem closure_epigraph_univ_of_exists_bot {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) (_hbot : ∃ (x : Fin n → ℝ), f x = ⊥) (hdense : closure (effectiveDomain Set.univ f) = Set.univ) : closure (epigraph Set.univ f) = Set.univ

If an improper convex function attains ⊥ and has dense effective domain, then its epigraph has dense closure.

theorem convexFunctionClosure_agrees_on_ri_and_same_epigraph_closure {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ImproperConvexFunctionOn Set.univ f) (hdense : closure (effectiveDomain Set.univ f) = Set.univ) : (∀ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f), convexFunctionClosure f x.ofLp = f x.ofLp) ∧ closure (epigraph Set.univ (convexFunctionClosure f)) = closure (epigraph Set.univ f)

Text 7.0.15: Even when a convex function f has -∞ somewhere, its closure cl f is not drastically different: they coincide on ri (dom f), and when dom f is dense their epigraphs have the same closure.

theorem lowerSemicontinuousHull_eq_of_lsc {n : ℕ} {f : (Fin n → ℝ) → EReal} (hls : LowerSemicontinuous f) : lowerSemicontinuousHull f = f

A lower semicontinuous function equals its lower semicontinuous hull.

theorem convexFunctionClosure_eq_of_no_bot {n : ℕ} {f : (Fin n → ℝ) → EReal} (hls : LowerSemicontinuous f) (hbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : convexFunctionClosure f = f

If f is lower semicontinuous and never ⊥, then its closure is itself.

theorem convexFunctionClosure_eq_of_closedConvexFunction {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ClosedConvexFunction f) (hbot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) : convexFunctionClosure f = f

theorem example_inf_over_line_convex_g_eq_sInf_fiber {f : (Fin 2 → ℝ) → EReal} (x : Fin 1 → ℝ) : (⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2) = sInf {z : EReal | ∃ (u : Fin 2 → ℝ), (projectionLinearMap ⋯) u = x ∧ z = f u}

Rewriting the line infimum as an infimum over the projection fiber.

theorem example_inf_over_line_convex_g_convex {f : (Fin 2 → ℝ) → EReal} (hfconv : ConvexFunction f) : ConvexFunction fun (x : Fin 1 → ℝ) => ⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2

The fiber infimum of a convex function is convex.

theorem example_inf_over_line_convex_g_lt_top {f : (Fin 2 → ℝ) → EReal} (hfinite : ∀ (x : Fin 2 → ℝ), f x ≠ ⊤ ∧ f x ≠ ⊥) (x : Fin 1 → ℝ) : (⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2) < ⊤

The infimum along a vertical line is strictly below ⊤ when f is finite.

theorem example_inf_over_line_convex_effectiveDomain_univ {f : (Fin 2 → ℝ) → EReal} (hfinite : ∀ (x : Fin 2 → ℝ), f x ≠ ⊤ ∧ f x ≠ ⊥) : (effectiveDomain Set.univ fun (x : Fin 1 → ℝ) => ⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2) = Set.univ

The effective domain of the line infimum is all of ℝ.

theorem example_inf_over_line_convex_dichotomy {f : (Fin 2 → ℝ) → EReal} (hfconv : ConvexFunction f) (hfinite : ∀ (x : Fin 2 → ℝ), f x ≠ ⊤ ∧ f x ≠ ⊥) : (∀ (x : Fin 1 → ℝ), (⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2) ≠ ⊤ ∧ (⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2) ≠ ⊥) ∨ ∀ (x : Fin 1 → ℝ), (⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2) = ⊥

Corollary 7.2.3 applied to the infimum along vertical lines.

theorem example_inf_over_line_convex_bdd_below {f : (Fin 2 → ℝ) → EReal} (hfconv : ConvexFunction f) (hfinite : ∀ (x : Fin 2 → ℝ), f x ≠ ⊤ ∧ f x ≠ ⊥) : (∃ (xi1 : ℝ) (m : ℝ), ∀ (xi2 : ℝ), ↑m ≤ f fun (i : Fin 2) => if i = 0 then xi1 else xi2) → ∀ (xi1 : ℝ), ∃ (m : ℝ), ∀ (xi2 : ℝ), ↑m ≤ f fun (i : Fin 2) => if i = 0 then xi1 else xi2

Bounded below on one vertical line implies bounded below on all vertical lines.

theorem example_inf_over_line_convex {f : (Fin 2 → ℝ) → EReal} (hfconv : ConvexFunction f) (hfinite : ∀ (x : Fin 2 → ℝ), f x ≠ ⊤ ∧ f x ≠ ⊥) : have g := fun (x : Fin 1 → ℝ) => ⨅ (xi2 : ℝ), f fun (i : Fin 2) => if i = 0 then x 0 else xi2; ConvexFunction g ∧ effectiveDomain Set.univ g = Set.univ ∧ ((∀ (x : Fin 1 → ℝ), g x ≠ ⊤ ∧ g x ≠ ⊥) ∨ ∀ (x : Fin 1 → ℝ), g x = ⊥) ∧ ((∃ (xi1 : ℝ) (m : ℝ), ∀ (xi2 : ℝ), ↑m ≤ f fun (i : Fin 2) => if i = 0 then xi1 else xi2) → ∀ (xi1 : ℝ), ∃ (m : ℝ), ∀ (xi2 : ℝ), ↑m ≤ f fun (i : Fin 2) => if i = 0 then xi1 else xi2)

Example 7.0.22: Let f be a finite convex function on ℝ^2 and define g(xi1) = inf_{xi2 ∈ ℝ} f(xi1, xi2). Then g is convex and dom g = ℝ. By Corollary 7.2.3, either g(xi1) is finite for all xi1 or g(xi1) = -∞ for all xi1. Consequently, if f is bounded below on one line parallel to the xi2-axis, then it is bounded below on every such line.

def riEpigraph {n : ℕ} (f : (Fin n → ℝ) → EReal) : Set (EuclideanSpace ℝ (Fin (n + 1)))

Remark 7.0.23: Theorems 7.2 and later show that comparisons between f and cl f hinge on relative interiors; in particular, the set ri (epi f) plays a key role.

Equations

• One or more equations did not get rendered due to their size.