theorem cone_smul_mem_of_nonneg {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) (h0 : 0 ∈ K) {r : ℝ} (hr : 0 ≤ r) {x : Fin n → ℝ} (hx : x ∈ K) : r • x ∈ K

A convex cone containing 0 is closed under nonnegative scaling.

theorem convexJoin_eq_add_of_cones {n : ℕ} (K1 K2 : ConvexCone ℝ (Fin n → ℝ)) (h0K1 : 0 ∈ K1) (h0K2 : 0 ∈ K2) : convexJoin ℝ ↑K1 ↑K2 = ↑K1 + ↑K2

For convex cones containing 0, the convex join equals the Minkowski sum.

theorem inverseAddition_eq_inter_of_cones {n : ℕ} (K1 K2 : ConvexCone ℝ (Fin n → ℝ)) (h0K1 : 0 ∈ K1) (h0K2 : 0 ∈ K2) : (↑K1 # ↑K2) = ↑K1 ∩ ↑K2

For convex cones containing 0, inverse addition equals intersection.

theorem convexCone_add_eq_convexHull_union_and_inverseAddition_eq_inter {n : ℕ} (K1 K2 : ConvexCone ℝ (Fin n → ℝ)) (h0K1 : 0 ∈ K1) (h0K2 : 0 ∈ K2) : ↑K1 + ↑K2 = (convexHull ℝ) (↑K1 ∪ ↑K2) ∧ (↑K1 # ↑K2) = ↑K1 ∩ ↑K2

Theorem 3.8: If K1 and K2 are convex cones containing the origin, then K1 + K2 = conv(K1 ∪ K2) and K1 # K2 = K1 ∩ K2.

def umbra {n : ℕ} (C S : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Text 3.8.1: The umbra of C with respect to S, for disjoint subsets C, S ⊆ ℝ^n, is the set ⋂ x ∈ S, ⋃ λ ≥ 1, ((1 - λ) • x) + λ • C.

Equations

• umbra C S = ⋂ x ∈ S, ⋃ (r : ℝ), ⋃ (_ : r ≥ 1), {(1 - r) • x} + r • C

def penumbra {n : ℕ} (C S : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Text 3.8.2: The penumbra of C with respect to S, for disjoint subsets C, S ⊆ ℝ^n, is the set ⋃ x ∈ S, ⋃ λ ≥ 1, ((1 - λ) • x) + λ • C.

Equations

• penumbra C S = ⋃ x ∈ S, ⋃ (r : ℝ), ⋃ (_ : r ≥ 1), {(1 - r) • x} + r • C

theorem mem_umbra_slice_iff {n : ℕ} {C : Set (Fin n → ℝ)} {x u : Fin n → ℝ} : u ∈ ⋃ (r : ℝ), ⋃ (_ : r ≥ 1), {(1 - r) • x} + r • C ↔ ∃ r ≥ 1, ∃ c ∈ C, u = (1 - r) • x + r • c

Membership in a slice of the umbra can be written with explicit witnesses.

theorem convex_umbra_slice {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (x : Fin n → ℝ) : Convex ℝ (⋃ (r : ℝ), ⋃ (_ : r ≥ 1), {(1 - r) • x} + r • C)

Each umbra slice is convex when C is convex.

theorem convex_umbra_of_convex {n : ℕ} {C S : Set (Fin n → ℝ)} (hC : Convex ℝ C) : Convex ℝ (umbra C S)

Text 3.8.3: The umbra is convex if C is convex.

theorem convex_penumbra_of_convex {n : ℕ} {C S : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hS : Convex ℝ S) : Convex ℝ (penumbra C S)

Text 3.8.4: The penumbra is convex if both S and C are convex.