theorem section14_polar_barrierCone_subset_recessionCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {C : Set E} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : ↑(PointedCone.dual (-LinearMap.applyₗ).flip C.barrierCone) ⊆ C.recessionCone

Points in the polar (w.r.t. flipped evaluation) of the barrier cone of a closed convex set are recession directions.

theorem polar_barrierCone_eq_recessionCone_part4 {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {C : Set E} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : ↑(PointedCone.dual (-LinearMap.applyₗ).flip C.barrierCone) = C.recessionCone

Corollary 14.2.1. The polar of the barrier cone of a non-empty closed convex set C is the recession cone of C.

theorem section14_recessionConeEReal_zero_mem {F : Type u_2} [AddCommGroup F] (f : F → EReal) : 0 ∈ recessionConeEReal f

The zero vector always lies in the recession cone of an EReal function.

theorem section14_polarCone_eq_univ_of_subset_singleton_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (S : Set E) (hS : S ⊆ {0}) : polarCone S = Set.univ

If a set is contained in {0}, then its polar cone is all of the dual space.

theorem section14_polarCone_eq_univ_iff_subset_singleton_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (S : Set E) : polarCone S = Set.univ ↔ S ⊆ {0}

A polar cone is all of the dual space iff the original set is contained in {0}.

theorem section14_eq_singleton_zero_iff_polarCone_eq_univ {E : Type u_1} [AddCommGroup E] [Module ℝ E] {S : Set E} (h0 : 0 ∈ S) : S = {0} ↔ polarCone S = Set.univ

A set equals {0} iff its polar cone is univ, provided it contains 0.

theorem section14_add_mem_of_add_mem_nat_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {y : E} (hadd : ∀ x ∈ C, x + y ∈ C) {x : E} (_hx : x ∈ C) (m : ℕ) : x + ↑m • y ∈ C

If C is closed under translation by y, then all natural translates stay in C.

theorem section14_mem_recessionCone_of_add_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hconv : Convex ℝ C) {y : E} (hadd : ∀ x ∈ C, x + y ∈ C) : y ∈ C.recessionCone

If C is convex and C + y ⊆ C, then y lies in the recession cone.

theorem section14_convex_sublevel {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hfconv : ConvexERealFunction f) (α : ℝ) : Convex ℝ {x : E | f x ≤ ↑α}

Sublevel sets of a Jensen-convex EReal function are convex.

theorem section14_recessionConeEReal_subset_recessionCone_sublevel {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hfconv : ConvexERealFunction f) {α : ℝ} : recessionConeEReal f ⊆ {x : E | f x ≤ ↑α}.recessionCone

A recession direction of f is a recession direction of every real sublevel set of f.

theorem section14_recessionCone_sublevel_subset_recessionConeEReal {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) {α : ℝ} (hne : {x : E | f x ≤ ↑α}.Nonempty) : {x : E | f x ≤ ↑α}.recessionCone ⊆ recessionConeEReal f

If f is proper, convex, and lower semicontinuous, then any recession direction of a nonempty real sublevel set is a recession direction of f.

theorem sublevelSets_bounded_iff_zero_mem_interior_dom_fenchelConjugate {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) : (∀ (α : ℝ), Bornology.IsBounded {x : EuclideanSpace ℝ (Fin n) | f x ≤ ↑α}) ↔ polarCone (recessionConeEReal f) = Set.univ

Corollary 14.2.2. Let f be a closed proper convex function. In order that the sublevel set {x | f x ≤ α} be bounded for every α ∈ ℝ, it is necessary and sufficient that 0 ∈ int (dom f*). Here f* is the Fenchel–Legendre conjugate and dom denotes the effective domain (the set where the value is finite).

In this formalization we record a topology-free equivalent criterion: the polar cone of the recession cone of f is all of the dual space.