def sumLinearMap {n m : ℕ} : (Fin m → EuclideanSpace ℝ (Fin n)) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)

The coordinate-sum linear map on Fin m-indexed tuples.

Equations

• sumLinearMap = { toFun := fun (x : Fin m → EuclideanSpace ℝ (Fin n)) => ∑ i : Fin m, x i, map_add' := ⋯, map_smul' := ⋯ }

theorem image_sumLinearMap_pi_eq_sum {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) : ⇑sumLinearMap '' Set.univ.pi C = ∑ i : Fin m, C i

The image of the product set under the sum map is the Minkowski sum.

noncomputable def euclideanSpace_equiv_prod_block {n m : ℕ} : EuclideanSpace ℝ (Fin (m * n)) ≃ₗ[ℝ] Fin m → EuclideanSpace ℝ (Fin n)

Linear equivalence between EuclideanSpace Real (Fin (m * n)) and block vectors.

Equations

• One or more equations did not get rendered due to their size.

def blockSet {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) : Set (EuclideanSpace ℝ (Fin (m * n)))

The block product set in ℝ^{m n} associated to C.

Equations

• blockSet C = ⇑euclideanSpace_equiv_prod_block ⁻¹' Set.univ.pi C

def blockSumLinearMap {n m : ℕ} : EuclideanSpace ℝ (Fin (m * n)) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)

The block sum linear map on EuclideanSpace Real (Fin (m * n)).

Equations

• blockSumLinearMap = sumLinearMap ∘ₗ ↑euclideanSpace_equiv_prod_block

theorem image_equiv_block_eq_pi {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) : ⇑euclideanSpace_equiv_prod_block '' blockSet C = Set.univ.pi C

The block equivalence sends blockSet to the product set.

theorem mem_closure_block_iff {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (x : EuclideanSpace ℝ (Fin (m * n))) : x ∈ closure (blockSet C) ↔ ∀ (i : Fin m), euclideanSpace_equiv_prod_block x i ∈ closure (C i)

Membership in the closure of blockSet is coordinatewise closure.

theorem mem_recessionCone_block_iff {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (z : EuclideanSpace ℝ (Fin (m * n))) : z ∈ (closure (blockSet C)).recessionCone ↔ ∀ (i : Fin m), euclideanSpace_equiv_prod_block z i ∈ (closure (C i)).recessionCone

Recession cone of the block set is coordinatewise recession.

theorem image_equiv_recessionCone_block_eq_pi {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) : ⇑euclideanSpace_equiv_prod_block '' (closure (blockSet C)).recessionCone = Set.univ.pi fun (i : Fin m) => (closure (C i)).recessionCone

The block equivalence sends the block recession cone to the product of recession cones.

theorem closure_sum_eq_sum_closure_of_recessionCone_sum_zero_lineality {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hlineal : ∀ (z : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), z i ∈ (closure (C i)).recessionCone) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (closure (C i)).linealitySpace) : closure (∑ i : Fin m, C i) = ∑ i : Fin m, closure (C i) ∧ (closure (∑ i : Fin m, C i)).recessionCone = ∑ i : Fin m, (closure (C i)).recessionCone ∧ ((∀ (i : Fin m), IsClosed (C i)) → IsClosed (∑ i : Fin m, C i))

Corollary 9.1.1. Let C1, ..., Cm be non-empty convex sets in R^n. Assume that whenever z1, ..., zm satisfy zi ∈ 0^+ (cl Ci) and z1 + ... + zm = 0, then each zi lies in the lineality space of cl Ci. Then cl (C1 + ... + Cm) = cl C1 + ... + cl Cm and 0^+ (cl (C1 + ... + Cm)) = 0^+ (cl C1) + ... + 0^+ (cl Cm). In particular, if each Ci is closed then C1 + ... + Cm is closed.

theorem closed_sum_of_closed_sets_of_recessionCone_sum_zero_lineality {n m : ℕ} (C : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hCconv : ∀ (i : Fin m), Convex ℝ (C i)) (hlineal : ∀ (z : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), z i ∈ (closure (C i)).recessionCone) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (closure (C i)).linealitySpace) (hCclosed : ∀ (i : Fin m), IsClosed (C i)) : IsClosed (∑ i : Fin m, C i)

Corollary 9.1.1.1. Under the hypotheses of Corollary 9.1.1, if all C_i are closed, then C_1 + ... + C_m is closed.

theorem zero_mem_linealitySpace {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) : 0 ∈ C.linealitySpace

Zero belongs to the lineality space of any set.

theorem lineality_of_no_opposite_recession_fin2 {n : ℕ} (C : Fin 2 → Set (EuclideanSpace ℝ (Fin n))) (hC0closed : IsClosed (C 0)) (hC1closed : IsClosed (C 1)) (hopp : ∀ z ∈ (C 0).recessionCone, -z ∈ (C 1).recessionCone → z = 0) (z : Fin 2 → EuclideanSpace ℝ (Fin n)) : (∀ (i : Fin 2), z i ∈ (closure (C i)).recessionCone) → ∑ i : Fin 2, z i = 0 → ∀ (i : Fin 2), z i ∈ (closure (C i)).linealitySpace

In the Fin 2 case, no-opposite-recession implies lineality.

theorem closed_add_recessionCone_eq_of_no_opposite_recession {n : ℕ} {C1 C2 : Set (EuclideanSpace ℝ (Fin n))} (hC1ne : C1.Nonempty) (hC2ne : C2.Nonempty) (hC1conv : Convex ℝ C1) (hC2conv : Convex ℝ C2) (hC1closed : IsClosed C1) (hC2closed : IsClosed C2) (hopp : ∀ z ∈ C1.recessionCone, -z ∈ C2.recessionCone → z = 0) : IsClosed (C1 + C2) ∧ (C1 + C2).recessionCone = C1.recessionCone + C2.recessionCone

Corollary 9.1.2. Let C1 and C2 be non-empty closed convex sets in R^n. Assume there is no direction of recession of C1 whose opposite is a direction of recession of C2 (in particular, this holds if either C1 or C2 is bounded). Then C1 + C2 is closed and 0^+ (C1 + C2) = 0^+ C1 + 0^+ C2.

theorem convex_of_IsConvexCone_image_equiv {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))} (hKcone : IsConvexCone n (⇑(EuclideanSpace.equiv (Fin n) ℝ) '' K)) : Convex ℝ K

Convexity is preserved when transporting a convex cone through EuclideanSpace.equiv.

theorem pos_smul_mem_of_IsConvexCone_image_equiv {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))} (hKcone : IsConvexCone n (⇑(EuclideanSpace.equiv (Fin n) ℝ) '' K)) (x : EuclideanSpace ℝ (Fin n)) : x ∈ K → ∀ (t : ℝ), 0 < t → t • x ∈ K

Positive scaling in K inherited from the cone structure of its coordinate image.

theorem zero_mem_closure_of_pos_smul_closed {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))} (hKne : K.Nonempty) (hsmul : ∀ x ∈ K, ∀ (t : ℝ), 0 < t → t • x ∈ K) : 0 ∈ closure K

A nonempty set closed under positive scaling has 0 in its closure.

theorem recessionCone_closure_eq_of_convexCone {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))} (hKne : K.Nonempty) (hKcone : IsConvexCone n (⇑(EuclideanSpace.equiv (Fin n) ℝ) '' K)) : (closure K).recessionCone = closure K

The recession cone of the closure of a convex cone is the closure itself.

theorem closure_sum_eq_sum_closure_of_convexCone_sum_zero_lineality {n m : ℕ} (K : Fin m → Set (EuclideanSpace ℝ (Fin n))) (hKne : ∀ (i : Fin m), (K i).Nonempty) (hKcone : ∀ (i : Fin m), IsConvexCone n (⇑(EuclideanSpace.equiv (Fin n) ℝ) '' K i)) (hlineal : ∀ (z : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), z i ∈ closure (K i)) → ∑ i : Fin m, z i = 0 → ∀ (i : Fin m), z i ∈ (closure (K i)).linealitySpace) : closure (∑ i : Fin m, K i) = ∑ i : Fin m, closure (K i)

theorem isClosed_parabola : IsClosed {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 1 ≥ x.ofLp 0 ^ 2}

The parabola set {x | x1 ≥ x0^2} is closed.

theorem image_parabola_eq_univ : have C := {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 1 ≥ x.ofLp 0 ^ 2}; have A := fun (x : EuclideanSpace ℝ (Fin 2)) => (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x_1 : Fin 1) => x.ofLp 0; A '' C = Set.univ

The projection of the parabola set onto the first coordinate is all of ℝ.

theorem recessionCone_parabola_eq : {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 1 ≥ x.ofLp 0 ^ 2}.recessionCone = {z : EuclideanSpace ℝ (Fin 2) | z.ofLp 0 = 0 ∧ 0 ≤ z.ofLp 1}

The recession cone of the parabola is the vertical ray {(0, z2) | z2 ≥ 0}.

theorem image_recessionCone_parabola_eq_singleton : have C := {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 1 ≥ x.ofLp 0 ^ 2}; have A := fun (x : EuclideanSpace ℝ (Fin 2)) => (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x_1 : Fin 1) => x.ofLp 0; A '' C.recessionCone = {0}

The image of the recession cone under the projection is {0}.

theorem recessionCone_image_ne_image_recessionCone_parabola : have C := {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 1 ≥ x.ofLp 0 ^ 2}; have A := fun (x : EuclideanSpace ℝ (Fin 2)) => (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x_1 : Fin 1) => x.ofLp 0; IsClosed C ∧ IsClosed (A '' C) ∧ (A '' C).recessionCone ≠ A '' C.recessionCone

theorem convexFunction_linearMap_infimum {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hconv : ConvexFunction h) : ConvexFunction fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}

The fiber infimum under a linear map is convex when the original function is convex.

theorem nonempty_epigraph_linearMap_infimum {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hne : (epigraph Set.univ h).Nonempty) : (epigraph Set.univ fun (y : Fin m → ℝ) => sInf {z : EReal | ∃ (x : Fin n → ℝ), A x = y ∧ z = h x}).Nonempty

The epigraph of the fiber infimum is nonempty if the original epigraph is nonempty.

def linearMap_prod {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : (Fin n → ℝ) × ℝ →ₗ[ℝ] (Fin m → ℝ) × ℝ

The lifted linear map on product spaces sending (x, μ) to (A x, μ).

Equations

• linearMap_prod A = { toFun := fun (p : (Fin n → ℝ) × ℝ) => (A p.1, p.2), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def prodLinearEquiv_append {n : ℕ} : ((Fin n → ℝ) × ℝ) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin (n + 1))

Linear equivalence between (Fin n → ℝ) × ℝ and ℝ^{n+1} via append.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def linearMap_prod_embedded {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : EuclideanSpace ℝ (Fin (n + 1)) →ₗ[ℝ] EuclideanSpace ℝ (Fin (m + 1))

Conjugate linearMap_prod under the append equivalence.

Equations

• linearMap_prod_embedded A = ↑prodLinearEquiv_append ∘ₗ linearMap_prod A ∘ₗ ↑prodLinearEquiv_append.symm

theorem image_linearMap_prod_embedded {n m : ℕ} {h : (Fin n → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : ⇑prodLinearEquiv_append '' (⇑(linearMap_prod A) '' epigraph Set.univ h) = ⇑(linearMap_prod_embedded A) '' (⇑prodLinearEquiv_append '' epigraph Set.univ h)

The embedded image matches the image under the conjugated linear map.