theorem convexFunction_const_on_affine_of_finite_boundedAbove {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (M : AffineSubspace ℝ (Fin n → ℝ)) (hfinite : ∀ x ∈ ↑M, f x ≠ ⊥ ∧ f x ≠ ⊤) (hbounded : ∃ (α : ℝ), ∀ x ∈ ↑M, f x ≤ ↑α) : ∃ (c : EReal), ∀ x ∈ ↑M, f x = c

Corollary 8.6.2. A convex function f is constant on any affine set M where it is finite and bounded above.

def Function.constancySpace {n : ℕ} (f0_plus : EuclideanSpace ℝ (Fin n) → EReal) : Set (EuclideanSpace ℝ (Fin n))

Definiton 8.7.0. Let f be a proper convex function on ℝ^n and let f0^+ be its recession function. The constancy space of f is the set { y ∈ ℝ^n | (f0^+)(y) ≤ 0 and (f0^+)(-y) ≤ 0 }.

Equations

• Function.constancySpace f0_plus = {y : EuclideanSpace ℝ (Fin n) | f0_plus y ≤ 0 ∧ f0_plus (-y) ≤ 0}

theorem recessionCone_sublevel_of_antitone {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EReal} {r : ℝ} {y : EuclideanSpace ℝ (Fin n)} : (∀ (x : EuclideanSpace ℝ (Fin n)), Antitone fun (t : ℝ) => f (x + t • y)) → y ∈ {x : EuclideanSpace ℝ (Fin n) | f x ≤ ↑r}.recessionCone

If all rays are antitone, then any sublevel set recedes in direction y.

theorem lineality_eq_constancySpace_of_recessionCone_eq {n : ℕ} {S : Set (EuclideanSpace ℝ (Fin n))} {f0_plus : EuclideanSpace ℝ (Fin n) → EReal} (hEq : S.recessionCone = {y : EuclideanSpace ℝ (Fin n) | f0_plus y ≤ 0}) : -S.recessionCone ∩ S.recessionCone = Function.constancySpace f0_plus

If the recession cone is given by f0_plus y ≤ 0, its lineality space is the constancy space of f0_plus.

theorem liminf_lt_top_of_recessionCone_sublevel {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {r : ℝ} {x y : EuclideanSpace ℝ (Fin n)} (hx : ↑(f x) ≤ ↑r) (hy : y ∈ {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.recessionCone) : Filter.liminf (fun (t : ℝ) => ↑(f (x + t • y))) Filter.atTop < ⊤

If x is in a sublevel set and y in its recession cone, the ray liminf is finite.

theorem antitone_all_of_mem_recessionCone_sublevel {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {f0_plus : EuclideanSpace ℝ (Fin n) → EReal} (hfclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (hfproper : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus ((EuclideanSpace.equiv (Fin n) ℝ).symm y) = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm (x + y)) - f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))}) {r : ℝ} (hnonempty : {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.Nonempty) {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.recessionCone) (x : EuclideanSpace ℝ (Fin n)) : Antitone fun (t : ℝ) => f (x + t • y)

Membership in a sublevel recession cone forces all rays to be antitone.

theorem recessionCone_sublevel_eq_f0plus_le_zero {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {f0_plus : EuclideanSpace ℝ (Fin n) → EReal} (hfclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (hfproper : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus ((EuclideanSpace.equiv (Fin n) ℝ).symm y) = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm (x + y)) - f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))}) {r : ℝ} (hnonempty : {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.Nonempty) : {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.recessionCone = {y : EuclideanSpace ℝ (Fin n) | f0_plus y ≤ 0}

Nonempty sublevel sets share recession cone {y | f0_plus y ≤ 0}.

theorem levelSet_recessionCone_and_lineality_eq_constancySpace {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {f0_plus : EuclideanSpace ℝ (Fin n) → EReal} (hfclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (hfproper : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus ((EuclideanSpace.equiv (Fin n) ℝ).symm y) = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm (x + y)) - f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))}) {r : ℝ} : {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.Nonempty → {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.recessionCone = {y : EuclideanSpace ℝ (Fin n) | f0_plus y ≤ 0} ∧ -{x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.recessionCone ∩ {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}.recessionCone = Function.constancySpace f0_plus

Theorem 8.7. Let f be a closed proper convex function. Then all non-empty level sets {x | f(x) ≤ λ} have the same recession cone and the same lineality space, namely {y | (f0^+)(y) ≤ 0} and the constancy space of f, respectively.

theorem sublevel_isClosed_convex_of_closedConvex {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hfclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (r : ℝ) : IsClosed {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r} ∧ Convex ℝ {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}

Sublevel sets of a closed convex function are closed and convex.

theorem levelSet_bounded_of_bounded_one {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hfclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) (hfproper : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f ((EuclideanSpace.equiv (Fin n) ℝ).symm x))) {r0 : ℝ} (hlevel : {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r0}.Nonempty) (hbounded : Bornology.IsBounded {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r0}) (r : ℝ) : Bornology.IsBounded {x : EuclideanSpace ℝ (Fin n) | ↑(f x) ≤ ↑r}

Corollary 8.7.1. Let f be a closed proper convex function. If the level set {x | f(x) ≤ λ} is non-empty and bounded for one λ, it is bounded for every λ.

theorem ray_eq_of_ineq_pair {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y : Fin n → ℝ} {v : ℝ} (hpos : ∀ (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f (x + t • y) ≤ f x + t * v) (hneg : ∀ (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f (x + t • -y) ≤ f x + t * -v) (x : Fin n → ℝ) (t : ℝ) : f (x + t • y) = f x + t * v

Two-sided ray inequalities force affine behavior along the direction.

theorem embedded_epigraph_neg {n : ℕ} : have eN := (EuclideanSpace.equiv (Fin n) ℝ).symm.toAffineEquiv; have e1 := ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm.toLinearEquiv ≪≫ₗ (EuclideanSpace.equiv (Fin 1) ℝ).symm.toLinearEquiv).toAffineEquiv; have g := eN.prodCongr e1; ∀ (y : Fin n → ℝ) (v : ℝ), (appendAffineEquiv n 1) (g (-y, -v)) = -(appendAffineEquiv n 1) (g (y, v))

Negation commutes with the embedded epigraph map.

theorem mem_recessionCone_embedded_epigraph_iff_ray_ineq {n : ℕ} {f : (Fin n → ℝ) → ℝ} {y : Fin n → ℝ} {v : ℝ} : (have eN := (EuclideanSpace.equiv (Fin n) ℝ).symm.toAffineEquiv; have e1 := ((ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm.toLinearEquiv ≪≫ₗ (EuclideanSpace.equiv (Fin 1) ℝ).symm.toLinearEquiv).toAffineEquiv; have g := eN.prodCongr e1; have epi := ⇑(appendAffineEquiv n 1) '' (⇑g '' epigraph Set.univ fun (x : Fin n → ℝ) => ↑(f x)); have yv := (appendAffineEquiv n 1) (g (y, v)); yv ∈ epi.recessionCone) ↔ ∀ (x : Fin n → ℝ) (t : ℝ), 0 ≤ t → f (x + t • y) ≤ f x + t * v

Membership in the embedded epigraph recession cone is equivalent to ray inequalities.

theorem f0plus_eq_slope_of_affine_ray {n : ℕ} {f f0_plus : (Fin n → ℝ) → ℝ} (hf0_plus : ∀ (y : Fin n → ℝ), ↑(f0_plus y) = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) (hclosed : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) {x : Fin n → ℝ} (_hx : x ∈ effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑(f x)) {y : Fin n → ℝ} {a b : ℝ} : (∀ (t : ℝ), f (x + t • y) = a * t + b) → f0_plus y = a ∧ f0_plus (-y) = -a

An affine ray determines the recession function value.

theorem properConvexFunction_lineality_equiv {n : ℕ} {f f0_plus : (Fin n → ℝ) → ℝ} (hf : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) (hf0_plus : ∀ (y : Fin n → ℝ), ↑(f0_plus y) = sSup {r : EReal | ∃ x ∈ Set.univ, r = ↑(f (x + y) - f x)}) : (∀ (y : Fin n → ℝ) (v : ℝ), ((∀ (x : Fin n → ℝ) (t : ℝ), f (x + t • y) = f x + t * v) ↔ have epi := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ fun (x : Fin n → ℝ) => ↑(f x)); have yv := (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm y, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => v); yv ∈ -epi.recessionCone ∩ epi.recessionCone) ∧ ((have epi := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ fun (x : Fin n → ℝ) => ↑(f x)); have yv := (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm y, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => v); yv ∈ -epi.recessionCone ∩ epi.recessionCone) ↔ -f0_plus (-y) = f0_plus y ∧ f0_plus y = v)) ∧ ∀ (y : Fin n → ℝ), (ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) → (∃ x ∈ effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑(f x), ∃ (a : ℝ) (b : ℝ), ∀ (t : ℝ), f (x + t • y) = a * t + b) → (∀ (x : Fin n → ℝ) (t : ℝ), f (x + t • y) = f x + t * f0_plus y) ∧ (have epi := ⇑(appendAffineEquiv n 1) '' ((fun (p : (Fin n → ℝ) × ℝ) => ((EuclideanSpace.equiv (Fin n) ℝ).symm p.1, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => p.2)) '' epigraph Set.univ fun (x : Fin n → ℝ) => ↑(f x)); have yv := (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm y, (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => f0_plus y); yv ∈ -epi.recessionCone ∩ epi.recessionCone) ∧ -f0_plus (-y) = f0_plus y

Theorem 8.8. For a proper convex function f, the following conditions on a vector y and a real number v are equivalent: (a) f (x + λ • y) = f x + λ v for all x and λ ∈ ℝ; (b) (y, v) belongs to the lineality space of epi f; (c) -(f0^+)(-y) = (f0^+)(y) = v. When f is closed, y satisfies these conditions with v = (f0^+)(y) if there is some x ∈ dom f such that λ ↦ f (x + λ • y) is affine.

def Function.linealitySpace {n : ℕ} (f0_plus : EuclideanSpace ℝ (Fin n) → EReal) : Set (EuclideanSpace ℝ (Fin n))

Definition 8.9.0. Let f be a proper convex function on ℝ^n with recession function f0^+. The set of vectors y such that (f0^+)(-y) = -(f0^+)(y) is called the lineality space of the proper convex function f.

Equations

• Function.linealitySpace f0_plus = {y : EuclideanSpace ℝ (Fin n) | f0_plus (-y) = -f0_plus y}