def Set.RecedesInDirection {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (y : EuclideanSpace ℝ (Fin n)) : Prop

Definition 8.0.1. Let C be a nonempty convex set in ℝ^n. The set C recedes in the direction of a nonzero vector y if x + λ • y ∈ C for all x ∈ C and all λ ≥ 0.

Equations

• C.RecedesInDirection y = (y ≠ 0 ∧ ∀ ⦃x : EuclideanSpace ℝ (Fin n)⦄, x ∈ C → ∀ ⦃t : ℝ⦄, 0 ≤ t → x + t • y ∈ C)

def Set.recessionCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Set E

Definition 8.0.2. Let C be a non-empty convex set. The recession cone of C is the set 0^+ C = { y | x + λ • y ∈ C for all x ∈ C and all λ ≥ 0 }.

Equations

• C.recessionCone = {y : E | ∀ ⦃x : E⦄, x ∈ C → ∀ ⦃t : ℝ⦄, 0 ≤ t → x + t • y ∈ C}

def Set.IsDirectionOfRecession {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (D : EuclideanSpace ℝ (Fin n)) : Prop

Definition 8.0.3. Let C be a non-empty convex set in R^n. A direction D of R^n is called a direction of recession of C if C recedes in the direction D.

Equations

• C.IsDirectionOfRecession D = C.RecedesInDirection D

theorem add_mem_of_add_mem_nat_smul {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {y : EuclideanSpace ℝ (Fin n)} (hadd : ∀ x ∈ C, x + y ∈ C) {x : EuclideanSpace ℝ (Fin n)} (_hx : x ∈ C) (m : ℕ) : x + ↑m • y ∈ C

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

theorem mem_recessionCone_of_add_mem {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hconv : Convex ℝ C) {y : EuclideanSpace ℝ (Fin n)} (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 recessionCone_eq_add_mem {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hconv : Convex ℝ C) : C.recessionCone = {y : EuclideanSpace ℝ (Fin n) | ∀ x ∈ C, x + y ∈ C}

Characterization of the recession cone via unit translation.

theorem recessionCone_convex {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hconv : Convex ℝ C) : Convex ℝ C.recessionCone

The recession cone of a convex set is convex.

theorem recessionCone_smul_pos {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ C.recessionCone) {t : ℝ} (ht : 0 < t) : t • y ∈ C.recessionCone

Positive scaling preserves membership in the recession cone.

theorem recessionCone_convexCone_and_eq {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (_hC : C.Nonempty) (hconv : Convex ℝ C) : Convex ℝ C.recessionCone ∧ (∀ y ∈ C.recessionCone, ∀ (t : ℝ), 0 < t → t • y ∈ C.recessionCone) ∧ 0 ∈ C.recessionCone ∧ C.recessionCone = {y : EuclideanSpace ℝ (Fin n) | ∀ x ∈ C, x + y ∈ C}

Theorem 8.1. Let C be a non-empty convex set. The recession cone 0^+ C is a convex cone containing the origin, and it equals the set of vectors y such that C + y ⊆ C.

theorem direction_subset_recessionCone_affineSubspace {n : ℕ} (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ M.direction) : y ∈ (↑M).recessionCone

A direction vector of an affine subspace belongs to its recession cone.

theorem recessionCone_subset_direction_affineSubspace {n : ℕ} (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (hM : (↑M).Nonempty) {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ (↑M).recessionCone) : y ∈ M.direction

Any vector in the recession cone of a nonempty affine subspace lies in its direction.

theorem recessionCone_affineSubspace_eq_direction {n : ℕ} (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (hM : (↑M).Nonempty) (L : Submodule ℝ (EuclideanSpace ℝ (Fin n))) (hL : L = M.direction) : (↑M).recessionCone = ↑L

Corollary 8.1.1. If M ⊆ ℝ^n is a non-empty affine set and L is the linear subspace parallel to M, then 0^+ M = L.

theorem inner_add_smul_eq {n : ℕ} (x y b : EuclideanSpace ℝ (Fin n)) (t : ℝ) : inner ℝ (x + t • y) b = inner ℝ x b + t * inner ℝ y b

Inner product with a translated point splits into a sum.

theorem nonneg_of_forall_add_smul_ge {a b c : ℝ} (h : ∀ t ≥ 0, a + t * b ≥ c) : 0 ≤ b

If a linear function is bounded below on t ≥ 0, its slope is nonnegative.

theorem recessionCone_subset_inner_ge_zero {n : ℕ} {ι : Type u_1} (I : Set ι) (b : ι → EuclideanSpace ℝ (Fin n)) (β : ι → ℝ) (hC : {x : EuclideanSpace ℝ (Fin n) | ∀ i ∈ I, inner ℝ x (b i) ≥ β i}.Nonempty) {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ {x : EuclideanSpace ℝ (Fin n) | ∀ i ∈ I, inner ℝ x (b i) ≥ β i}.recessionCone) (i : ι) : i ∈ I → inner ℝ y (b i) ≥ 0

Vectors in the recession cone of a nonempty intersection of half-spaces have nonnegative inner products with the defining normals.

theorem recessionCone_isClosed_of_closed {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hC : IsClosed C) : IsClosed C.recessionCone

The recession cone of a closed set is closed.

theorem recessionCone_eq_inner_ge_zero {n : ℕ} {ι : Type u_1} (I : Set ι) (b : ι → EuclideanSpace ℝ (Fin n)) (β : ι → ℝ) (hC : {x : EuclideanSpace ℝ (Fin n) | ∀ i ∈ I, inner ℝ x (b i) ≥ β i}.Nonempty) : {x : EuclideanSpace ℝ (Fin n) | ∀ i ∈ I, inner ℝ x (b i) ≥ β i}.recessionCone = {y : EuclideanSpace ℝ (Fin n) | ∀ i ∈ I, inner ℝ y (b i) ≥ 0}

Corollary 8.1.2. Let C = {x ∈ ℝ^n | ⟪x, b_i⟫ ≥ β_i, ∀ i ∈ I} be nonempty. Then 0^+ C = {y ∈ ℝ^n | ⟪y, b_i⟫ ≥ 0, ∀ i ∈ I}.

theorem recessionCone_subset_seq_limits {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) {y : EuclideanSpace ℝ (Fin n)} (hy : y ∈ C.recessionCone) : ∃ (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)

Elements of the recession cone give limits with decreasing coefficients.

theorem mem_K_of_mem_closure_K_first_pos {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : 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); ∀ v ∈ closure K, 0 < first v → v ∈ K

If a point in closure K has positive first coordinate, then it lies in K.

theorem tail_mem_recessionCone_of_mem_closure_K_first_zero {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : 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); ∀ v ∈ closure K, first v = 0 → tail v ∈ C.recessionCone

Points in closure K with zero first coordinate yield recession directions.

theorem closure_cone_eq_union_recession {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : 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}

The closure of K adds precisely the recession directions at first = 0.

theorem seq_limits_subset_recessionCone {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) {y : EuclideanSpace ℝ (Fin n)} (hy : ∃ (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)) : y ∈ C.recessionCone

Reverse inclusion for the sequence characterization of the recession cone.