theorem closedConvexFunction_precomp_linearMap {n m : ℕ} {g : (Fin m → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : ClosedConvexFunction g → ClosedConvexFunction fun (x : Fin n → ℝ) => g (A x)

Precomposition with a linear map preserves closedness of convex functions.

theorem effectiveDomain_precomp_linearMap {n m : ℕ} {g : (Fin m → ℝ) → EReal} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : (effectiveDomain Set.univ fun (x : Fin n → ℝ) => g (A x)) = ⇑A ⁻¹' effectiveDomain Set.univ g

Effective domain of a precomposition is a preimage.

theorem ri_effectiveDomain_preimage_linearMap {n m : ℕ} {g : (Fin m → ℝ) → EReal} (hgproper : ProperConvexFunctionOn Set.univ g) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hri : ∃ (x : Fin n → ℝ), (EuclideanSpace.equiv (Fin m) ℝ).symm (A x) ∈ euclideanRelativeInterior m (⇑(EuclideanSpace.equiv (Fin m) ℝ).symm '' effectiveDomain Set.univ g)) : have e_n := EuclideanSpace.equiv (Fin n) ℝ; have e_m := EuclideanSpace.equiv (Fin m) ℝ; have A_e := ↑e_m.symm.toLinearEquiv ∘ₗ A ∘ₗ ↑e_n.toLinearEquiv; euclideanRelativeInterior n (⇑e_n.symm '' effectiveDomain Set.univ fun (x : Fin n → ℝ) => g (A x)) = ⇑A_e ⁻¹' euclideanRelativeInterior m (⇑e_m.symm '' effectiveDomain Set.univ g)

Relative interior of the effective domain under a linear preimage.

theorem ri_effectiveDomain_preimage_linearMap_preimage {n m : ℕ} {g : (Fin m → ℝ) → EReal} (hgproper : ProperConvexFunctionOn Set.univ g) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hri : ∃ (x : Fin n → ℝ), (EuclideanSpace.equiv (Fin m) ℝ).symm (A x) ∈ euclideanRelativeInterior m (⇑(EuclideanSpace.equiv (Fin m) ℝ).symm '' effectiveDomain Set.univ g)) : have e_n := EuclideanSpace.equiv (Fin n) ℝ; have e_m := EuclideanSpace.equiv (Fin m) ℝ; have A_e := ↑e_m.symm.toLinearEquiv ∘ₗ A ∘ₗ ↑e_n.toLinearEquiv; euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ fun (x : Fin n → ℝ) => g (A x)) = ⇑A_e ⁻¹' euclideanRelativeInterior m ((fun (x : EuclideanSpace ℝ (Fin m)) => x.ofLp) ⁻¹' effectiveDomain Set.univ g)

Relative interior of the effective domain in preimage form under a linear map.

theorem ri_effectiveDomain_closure_eq {m : ℕ} {g : (Fin m → ℝ) → EReal} (hgproper : ProperConvexFunctionOn Set.univ g) : euclideanRelativeInterior m ((fun (x : EuclideanSpace ℝ (Fin m)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (convexFunctionClosure g)) = euclideanRelativeInterior m ((fun (x : EuclideanSpace ℝ (Fin m)) => x.ofLp) ⁻¹' effectiveDomain Set.univ g)

Relative interior of the effective domain is preserved by convex closure.

theorem convexFunctionClosure_precomp_linearMap_eq {n m : ℕ} {g : (Fin m → ℝ) → EReal} (hgproper : ProperConvexFunctionOn Set.univ g) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hri : ∃ (x : Fin n → ℝ), (EuclideanSpace.equiv (Fin m) ℝ).symm (A x) ∈ euclideanRelativeInterior m (⇑(EuclideanSpace.equiv (Fin m) ℝ).symm '' effectiveDomain Set.univ g)) : (convexFunctionClosure fun (x : Fin n → ℝ) => g (A x)) = fun (x : Fin n → ℝ) => convexFunctionClosure g (A x)

Closure commutes with linear precomposition under a relative-interior preimage point.

theorem linearMap_comp_closed_recession_and_closure {n m : ℕ} {g g0_plus : (Fin m → ℝ) → EReal} (hgproper : ProperConvexFunctionOn Set.univ g) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (_hfinite : ∃ (x : Fin n → ℝ), g (A x) ≠ ⊤) : have gA := fun (x : Fin n → ℝ) => g (A x); have gA0_plus := fun (x : Fin n → ℝ) => g0_plus (A x); (ClosedConvexFunction g → ClosedConvexFunction gA ∧ gA0_plus = fun (x : Fin n → ℝ) => g0_plus (A x)) ∧ (¬ClosedConvexFunction g → (∃ (x : Fin n → ℝ), (EuclideanSpace.equiv (Fin m) ℝ).symm (A x) ∈ euclideanRelativeInterior m (⇑(EuclideanSpace.equiv (Fin m) ℝ).symm '' effectiveDomain Set.univ g)) → convexFunctionClosure gA = fun (x : Fin n → ℝ) => convexFunctionClosure g (A x))

Theorem 9.5. Let A be a linear transformation from ℝ^n to ℝ^m, and let g be a proper convex function on ℝ^m such that g ∘ A is not identically +∞. If g is closed, then g ∘ A is closed and (g ∘ A)0^+ = (g0^+) ∘ A. If g is not closed, but A x lies in ri (dom g) for some x, then cl (g ∘ A) = (cl g) ∘ A.

theorem tail_kernel_closure_cone_zero {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∉ C) : have e := EuclideanSpace.equiv (Fin n) ℝ; have C' := ⇑e.symm '' 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, tail v = 0 → v = 0

In the lifted cone, a closure point with zero tail must be the origin.

theorem closure_tail_image_cone_eq_union_recession {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∉ C) : have e := EuclideanSpace.equiv (Fin n) ℝ; have C' := ⇑e.symm '' 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); have A := LinearMap.snd ℝ (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin n)) ∘ₗ ↑(appendAffineEquiv 1 n).symm.linear; closure (⇑A '' K) = ⇑A '' K ∪ C'.recessionCone

The tail image of the lifted cone closes by adjoining recession directions.

theorem convexConeGenerated_union_recession_eq_iUnion_pos {n : ℕ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) {recC : Set (Fin n → ℝ)} (hrec0 : 0 ∈ recC) : have K := convexConeGenerated n C; K ∪ recC = (⋃ (t : ℝ), ⋃ (_ : 0 < t), t • C) ∪ recC

The generated cone equals positive scalings, up to union with a set containing 0.

theorem closure_convexConeGenerated_eq_union_recessionCone {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∉ C) : have e := EuclideanSpace.equiv (Fin n) ℝ; have C' := ⇑e.symm '' C; have recC := ⇑e '' C'.recessionCone; have K := convexConeGenerated n C; closure K = K ∪ recC ∧ K ∪ recC = (⋃ (t : ℝ), ⋃ (_ : 0 < t), t • C) ∪ recC

Theorem 9.6. Let C be a non-empty closed convex set not containing the origin, and let K be the convex cone generated by C. Then closure K = K ∪ 0^+ C, and this set equals ⋃ { λ C | λ > 0 or λ = 0^+ }.

theorem recCone_eq_singleton_zero_of_bounded_image {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hCbdd : Bornology.IsBounded C) : have e := EuclideanSpace.equiv (Fin n) ℝ; have C' := ⇑e.symm '' C; C'.recessionCone = {0}

Boundedness forces the recession cone of the Euclidean image to be {0}.

theorem closed_convexConeGenerated_of_bounded {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCbdd : Bornology.IsBounded C) (hCconv : Convex ℝ C) (hC0 : 0 ∉ C) : IsClosed (convexConeGenerated n C)

Corollary 9.6.1. If C is a non-empty closed bounded convex set not containing the origin, then the convex cone K generated by C is closed.

theorem lineSet_eq_first_coord : {x : Fin 2 → ℝ | ∃ (t : ℝ), x = ![1, 0] + t • ![0, 1]} = {x : Fin 2 → ℝ | x 0 = 1}

The vertical line through ![1, 0] is the set of points with first coordinate 1.

theorem closed_lineSet : IsClosed {x : Fin 2 → ℝ | ∃ (t : ℝ), x = ![1, 0] + t • ![0, 1]}

The vertical line {(1, t)} is closed.

theorem convex_lineSet : Convex ℝ {x : Fin 2 → ℝ | ∃ (t : ℝ), x = ![1, 0] + t • ![0, 1]}

The vertical line {(1, t)} is convex.

theorem cone_line_pos_first {x : Fin 2 → ℝ} (hx : x ∈ convexConeGenerated 2 {x : Fin 2 → ℝ | ∃ (t : ℝ), x = ![1, 0] + t • ![0, 1]}) (hx0 : x ≠ 0) : 0 < x 0

Nonzero points in the cone over the vertical line have positive first coordinate.

theorem pos_first_mem_cone_line {x : Fin 2 → ℝ} (hx : 0 < x 0) : x ∈ convexConeGenerated 2 {x : Fin 2 → ℝ | ∃ (t : ℝ), x = ![1, 0] + t • ![0, 1]}

Points with positive first coordinate lie in the cone over the vertical line.

theorem closure_cone_line_has_point : ![0, 1] ∈ closure (convexConeGenerated 2 {x : Fin 2 → ℝ | ∃ (t : ℝ), x = ![1, 0] + t • ![0, 1]})

The point (0, 1) lies in the closure of the cone over the vertical line.