theorem recessionCone_closed_and_limits_and_closure_cone {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : IsClosed C.recessionCone ∧ C.recessionCone = {y : EuclideanSpace ℝ (Fin n) | ∃ (x : ℕ → EuclideanSpace ℝ (Fin n)) (r : ℕ → ℝ), (∀ (n_1 : ℕ), x n_1 ∈ C) ∧ Antitone r ∧ Filter.Tendsto r Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n_1 : ℕ) => r n_1 • x n_1) Filter.atTop (nhds y)} ∧ have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ); have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0; have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i); have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C}; have K := ↑(ConvexCone.hull ℝ S); closure K = K ∪ {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 0 ∧ tail v ∈ C.recessionCone}

Theorem 8.2. Let C be a non-empty closed convex set in ℝ^n. Then 0^+ C is closed, and it consists of all possible limits of sequences of the form λ_1 x_1, λ_2 x_2, ..., where x_i ∈ C and λ_i decreases to 0. In fact, for the convex cone K in ℝ^(n+1) generated by {(1, x) | x ∈ C} one has cl K = K ∪ {(0, x) | x ∈ 0^+ C}.

theorem halfline_seq_data {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {x0 y : EuclideanSpace ℝ (Fin n)} (hx0 : ∀ (t : ℝ), 0 ≤ t → x0 + t • y ∈ C) : ∃ (x : ℕ → EuclideanSpace ℝ (Fin n)) (r : ℕ → ℝ), (∀ (n_1 : ℕ), x n_1 ∈ C) ∧ Antitone r ∧ Filter.Tendsto r Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n_1 : ℕ) => r n_1 • x n_1) Filter.atTop (nhds y)

Sequence data associated with a half-line inside C.

theorem halfline_mem_recessionCone {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) {x0 y : EuclideanSpace ℝ (Fin n)} (hx0 : ∀ (t : ℝ), 0 ≤ t → x0 + t • y ∈ C) : y ∈ C.recessionCone

A half-line contained in C yields a recession direction.

theorem ri_ray_mem {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCconv : Convex ℝ C) {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ C.recessionCone) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n C) (t : ℝ) : 0 ≤ t → x + t • y ∈ euclideanRelativeInterior n C

Rays from points in the relative interior stay in the relative interior.

theorem recessionCone_ri_of_ri_ray {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {y : EuclideanSpace ℝ (Fin n)} (hri : ∀ x ∈ euclideanRelativeInterior n C, ∀ (t : ℝ), 0 ≤ t → x + t • y ∈ euclideanRelativeInterior n C) : y ∈ (euclideanRelativeInterior n C).recessionCone

A ray property in ri C yields membership in 0^+ (ri C).

theorem recessionCone_of_exists_halfline {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) {y : EuclideanSpace ℝ (Fin n)} (_hy : y ≠ 0) (hex : ∃ (x : EuclideanSpace ℝ (Fin n)), ∀ (t : ℝ), 0 ≤ t → x + t • y ∈ C) : y ∈ C.recessionCone ∧ (∀ x ∈ euclideanRelativeInterior n C, ∀ (t : ℝ), 0 ≤ t → x + t • y ∈ euclideanRelativeInterior n C) ∧ y ∈ (euclideanRelativeInterior n C).recessionCone

Theorem 8.3. Let C be a non-empty closed convex set, and let y ≠ 0. If there exists x such that the half-line {x + λ y | λ ≥ 0} is contained in C, then the same holds for every x ∈ C, i.e. y ∈ 0^+ C. Moreover, for each x ∈ ri C, the half-line {x + λ y | λ ≥ 0} is contained in ri C, so y ∈ 0^+ (ri C).

theorem recessionCone_closure_iff_ray_in_C {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ euclideanRelativeInterior n C) (y : EuclideanSpace ℝ (Fin n)) : y ∈ (closure C).recessionCone ↔ ∀ (t : ℝ), 0 < t → x + t • y ∈ C

Characterization of recession directions of closure C via rays from a point in ri C.

theorem recessionCone_ri_eq_cl_and_characterization {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) : (euclideanRelativeInterior n C).recessionCone = (closure C).recessionCone ∧ ∀ x ∈ euclideanRelativeInterior n C, ∀ (y : EuclideanSpace ℝ (Fin n)), y ∈ (closure C).recessionCone ↔ ∀ (t : ℝ), 0 < t → x + t • y ∈ C

Corollary 8.3.1. For any non-empty convex set C, one has 0^+ (ri C) = 0^+ (cl C). In fact, given any x ∈ ri C, one has y ∈ 0^+ (cl C) if and only if x + λ • y ∈ C for every λ > 0.

theorem recessionCone_subset_inv_smul_set {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hC0 : 0 ∈ C) (y : EuclideanSpace ℝ (Fin n)) : y ∈ C.recessionCone → ∀ (ε : ℝ), 0 < ε → ε⁻¹ • y ∈ C

Elements of the recession cone scale back into C from the origin.

theorem inv_smul_set_subset_recessionCone {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) (y : EuclideanSpace ℝ (Fin n)) : (∀ (ε : ℝ), 0 < ε → ε⁻¹ • y ∈ C) → y ∈ C.recessionCone

If all inverse scalings of y lie in C, then y is a recession direction.

theorem inv_smul_set_eq_iInter_smul {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} : {y : EuclideanSpace ℝ (Fin n) | ∀ (ε : ℝ), 0 < ε → ε⁻¹ • y ∈ C} = ⋂ (ε : ℝ), ⋂ (_ : 0 < ε), ε • C

The inverse-scaling characterization equals the intersection of all positive scalings.

theorem recessionCone_eq_inv_smul_set_and_iInter {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : C.recessionCone = {y : EuclideanSpace ℝ (Fin n) | ∀ (ε : ℝ), 0 < ε → ε⁻¹ • y ∈ C} ∧ {y : EuclideanSpace ℝ (Fin n) | ∀ (ε : ℝ), 0 < ε → ε⁻¹ • y ∈ C} = ⋂ (ε : ℝ), ⋂ (_ : 0 < ε), ε • C

Corollary 8.3.2. If C is a closed convex set containing the origin, then 0^+ C = { y | ε⁻¹ • y ∈ C, ∀ ε > 0 } = ⋂ (ε > 0), ε • C.

theorem recessionCone_iInter_halfline {n : ℕ} {ι : Type u_1} {C : ι → Set (EuclideanSpace ℝ (Fin n))} {x0 y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ (⋂ (i : ι), C i).recessionCone) (hx0 : x0 ∈ ⋂ (i : ι), C i) (i : ι) (t : ℝ) : 0 ≤ t → x0 + t • y ∈ C i

A recession direction for the intersection yields half-lines in each set.

theorem recessionCone_iInter_subset {n : ℕ} {ι : Type u_1} (C : ι → Set (EuclideanSpace ℝ (Fin n))) (hCclosed : ∀ (i : ι), IsClosed (C i)) (hCconv : ∀ (i : ι), Convex ℝ (C i)) (hCne : (⋂ (i : ι), C i).Nonempty) : (⋂ (i : ι), C i).recessionCone ⊆ ⋂ (i : ι), (C i).recessionCone

The recession cone of an intersection is contained in the intersection of recession cones.

theorem iInter_recessionCone_subset {n : ℕ} {ι : Type u_1} (C : ι → Set (EuclideanSpace ℝ (Fin n))) : ⋂ (i : ι), (C i).recessionCone ⊆ (⋂ (i : ι), C i).recessionCone

Recession directions common to all sets are recession directions of the intersection.

theorem recessionCone_iInter_eq_iInter {n : ℕ} {ι : Type u_1} (C : ι → Set (EuclideanSpace ℝ (Fin n))) (hCclosed : ∀ (i : ι), IsClosed (C i)) (hCconv : ∀ (i : ι), Convex ℝ (C i)) (hCne : (⋂ (i : ι), C i).Nonempty) : (⋂ (i : ι), C i).recessionCone = ⋂ (i : ι), (C i).recessionCone

Corollary 8.3.3. If {C_i | i ∈ I} is an arbitrary collection of closed convex sets in ℝ^n whose intersection is not empty, then 0^+ (⋂ i, C_i) = ⋂ i, 0^+ C_i.

theorem preimage_nonempty_implies_C_nonempty {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) {C : Set (EuclideanSpace ℝ (Fin m))} : (⇑A ⁻¹' C).Nonempty → C.Nonempty

Nonempty preimage implies nonempty target set.

theorem recessionCone_preimage_linearMap_subset {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) {C : Set (EuclideanSpace ℝ (Fin m))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCne : (⇑A ⁻¹' C).Nonempty) : (⇑A ⁻¹' C).recessionCone ⊆ ⇑A ⁻¹' C.recessionCone

Recession cone of the preimage lies in the preimage of the recession cone.

theorem preimage_recessionCone_subset_recessionCone_preimage {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) {C : Set (EuclideanSpace ℝ (Fin m))} : ⇑A ⁻¹' C.recessionCone ⊆ (⇑A ⁻¹' C).recessionCone

Preimage of the recession cone lies in the recession cone of the preimage.

theorem recessionCone_preimage_linearMap {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) {C : Set (EuclideanSpace ℝ (Fin m))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCne : (⇑A ⁻¹' C).Nonempty) : (⇑A ⁻¹' C).recessionCone = ⇑A ⁻¹' C.recessionCone

Corollary 8.3.4. Let A be a linear transformation from ℝ^n to ℝ^m, and let C be a closed convex set in ℝ^m such that A ⁻¹' C is nonempty. Then 0^+ (A ⁻¹' C) = A ⁻¹' (0^+ C).

theorem recessionCone_subset_singleton_of_bounded {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCbdd : Bornology.IsBounded C) : C.recessionCone ⊆ {0}

Bounded sets have only the zero recession direction.

theorem exists_strictMono_norm_seq_of_unbounded {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCunbdd : ¬Bornology.IsBounded C) : ∃ (x : ℕ → EuclideanSpace ℝ (Fin n)), (∀ (n_1 : ℕ), x n_1 ∈ C) ∧ (StrictMono fun (n_1 : ℕ) => ‖x n_1‖) ∧ ∀ (n_1 : ℕ), ↑n_1 + 1 ≤ ‖x n_1‖

An unbounded set admits a sequence with strictly increasing norms.

theorem exists_nonzero_mem_recessionCone_of_unbounded {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCunbdd : ¬Bornology.IsBounded C) : ∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ y ∈ C.recessionCone

An unbounded closed convex set has a nonzero recession direction.

theorem bounded_iff_recessionCone_eq_singleton_zero {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : Bornology.IsBounded C ↔ C.recessionCone = {0}

Theorem 8.4. A non-empty closed convex set C in ℝ^n is bounded if and only if its recession cone 0^+ C consists of the zero vector alone.

theorem recessionCone_inter_eq {n : ℕ} {A B : Set (EuclideanSpace ℝ (Fin n))} (hAclosed : IsClosed A) (hBclosed : IsClosed B) (hAconv : Convex ℝ A) (hBconv : Convex ℝ B) (hABne : (A ∩ B).Nonempty) : (A ∩ B).recessionCone = A.recessionCone ∩ B.recessionCone

Recession cone of a nonempty intersection of two closed convex sets.

theorem recessionCone_affine_parallel_eq {n : ℕ} {M M' : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))} (hM : (↑M).Nonempty) (hM' : (↑M').Nonempty) (hparallel : M'.direction = M.direction) : (↑M').recessionCone = (↑M).recessionCone

Parallel nonempty affine subspaces have the same recession cone.

theorem bounded_empty_intersection {n : ℕ} {A B : Set (EuclideanSpace ℝ (Fin n))} (h : ¬(A ∩ B).Nonempty) : Bornology.IsBounded (A ∩ B)

An empty intersection is bounded.

theorem boundedness_via_recessionCone_inter {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) {M M' : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))} (hMCne : (↑M ∩ C).Nonempty) (hMCbdd : Bornology.IsBounded (↑M ∩ C)) (hM'Cne : (↑M' ∩ C).Nonempty) (hparallel : M'.direction = M.direction) : (↑M' ∩ C).recessionCone = {0}

Boundedness transfer via recession cones for parallel affine subspaces.

theorem bounded_inter_of_parallel_affine {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (hMCne : (↑M ∩ C).Nonempty) (hMCbdd : Bornology.IsBounded (↑M ∩ C)) (M' : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) : M'.direction = M.direction → Bornology.IsBounded (↑M' ∩ C)

Corollary 8.4.1. Let C be a closed convex set, and let M be an affine set such that M ∩ C is non-empty and bounded. Then M' ∩ C is bounded for every affine set M' parallel to M.