theorem helperForCorollary_19_2_1_indicatorPolyhedral_of_polyhedralSet {n : ℕ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolyhedralConvexSet n C) : IsPolyhedralConvexFunction n (indicatorFunction C)

Helper for Corollary 19.2.1: a polyhedral set yields a polyhedral indicator function via the max-affine-plus-indicator representation with k = 0.

theorem helperForCorollary_19_2_1_indicatorRepresentation_forces_setEquality {n k m : ℕ} {C D : Set (Fin n → ℝ)} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ} (hrepr : indicatorFunction C = fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin m), ↑i < k ∧ r = ∑ j : Fin n, x j * b i j - β i}) + indicatorFunction D x) : C = D

Helper for Corollary 19.2.1: an equality between an indicator and a max-affine-plus- indicator representation forces equality of the underlying sets.

theorem helperForCorollary_19_2_1_polyhedralSet_of_indicatorPolyhedral {n : ℕ} {C : Set (Fin n → ℝ)} (hIndicatorPoly : IsPolyhedralConvexFunction n (indicatorFunction C)) : IsPolyhedralConvexSet n C

Helper for Corollary 19.2.1: if the indicator function is polyhedral, then the set is polyhedral.

theorem helperForCorollary_19_2_1_supportFunctionPolyhedral_of_polyhedralSet {n : ℕ} {C : Set (Fin n → ℝ)} (hClosed : IsClosed C) (hConv : Convex ℝ C) (hCpoly : IsPolyhedralConvexSet n C) : IsPolyhedralConvexFunction n (supportFunctionEReal C)

Helper for Corollary 19.2.1: a closed convex polyhedral set has a polyhedral support function.

theorem helperForCorollary_19_2_1_polyhedralSet_of_supportFunctionPolyhedral {n : ℕ} {C : Set (Fin n → ℝ)} (hClosed : IsClosed C) (hConv : Convex ℝ C) (hSupportPoly : IsPolyhedralConvexFunction n (supportFunctionEReal C)) : IsPolyhedralConvexSet n C

Helper for Corollary 19.2.1: if the support function is polyhedral, then the closed convex set is polyhedral.

theorem helperForCorollary_19_2_1_polyhedralSet_iff_supportFunctionPolyhedral_of_closed_convex {n : ℕ} {C : Set (Fin n → ℝ)} (hClosed : IsClosed C) (hConv : Convex ℝ C) : IsPolyhedralConvexSet n C ↔ IsPolyhedralConvexFunction n (supportFunctionEReal C)

Helper for Corollary 19.2.1: under closedness and convexity, polyhedrality of C is equivalent to polyhedrality of its support function.

theorem polyhedral_convexSet_iff_supportFunction_polyhedral (n : ℕ) (C : Set (Fin n → ℝ)) : IsClosed C → Convex ℝ C → (IsPolyhedralConvexSet n C ↔ IsPolyhedralConvexFunction n (supportFunctionEReal C))

Corollary 19.2.1: A closed convex set C is polyhedral iff its support function δ^*(· | C) is polyhedral.

theorem helperForCorollary_19_2_2_supportFunction_polyhedral_of_polyhedralSet {n : ℕ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolyhedralConvexSet n C) : IsPolyhedralConvexFunction n (supportFunctionEReal C)

Helper for Corollary 19.2.2: a polyhedral convex set has a polyhedral support function.

theorem helperForCorollary_19_2_2_one_ne_top : 1 ≠ ⊤

Helper for Corollary 19.2.2: the element (1 : EReal) is not top.

theorem helperForCorollary_19_2_2_emptyCase_univ_polyhedral (n : ℕ) : IsPolyhedralConvexSet n {xStar : Fin n → ℝ | supportFunctionEReal ∅ xStar ≤ 1}

Helper for Corollary 19.2.2: when C = ∅, the polar sublevel set at level 1 is all of ℝ^n, hence polyhedral.

theorem helperForCorollary_19_2_2_piecewiseBounds_polyhedral {n k m : ℕ} {b : Fin m → Fin n → ℝ} {β : Fin m → ℝ} : IsPolyhedralConvexSet n {x : Fin n → ℝ | ∀ (i : Fin m), ∑ j : Fin n, x j * b i j ≤ if ↑i < k then β i + 1 else β i}

Helper for Corollary 19.2.2: finitely many affine upper bounds of the form (∑ j, x j * b i j) ≤ (if i < k then β i + 1 else β i) define a polyhedral convex set.

theorem polyhedral_convexSet_polar_polyhedral (n : ℕ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → IsPolyhedralConvexSet n {xStar : Fin n → ℝ | supportFunctionEReal C xStar ≤ 1}

Corollary 19.2.2: The polar of a polyhedral convex set is polyhedral.

theorem helperForTheorem_19_3_image_finitelyGenerated_of_polyhedral {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolyhedralConvexSet n C) : IsFinitelyGeneratedConvexSet m (⇑A '' C)

Helper for Theorem 19.3: linear images of polyhedral convex sets are finitely generated.

theorem helperForTheorem_19_3_image_polyhedral_of_polyhedral {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolyhedralConvexSet n C) : IsPolyhedralConvexSet m (⇑A '' C)

Helper for Theorem 19.3: linear images of polyhedral convex sets are polyhedral.

theorem helperForTheorem_19_3_preimage_closedHalfSpaceLE_eq {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (b : Fin m → ℝ) (β : ℝ) : ⇑A ⁻¹' closedHalfSpaceLE m b β = closedHalfSpaceLE n (((LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))) A).transpose.mulVec b) β

Helper for Theorem 19.3: the preimage of one closed half-space under A is the corresponding closed half-space with normal transformed by the transpose matrix of A.

theorem helperForTheorem_19_3_preimage_polyhedral_of_polyhedral {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {D : Set (Fin m → ℝ)} (hDpoly : IsPolyhedralConvexSet m D) : IsPolyhedralConvexSet n (⇑A ⁻¹' D)

Helper for Theorem 19.3: linear preimages of polyhedral convex sets are polyhedral.

theorem helperForTheorem_19_3_image_branch {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (C : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C → IsPolyhedralConvexSet m (⇑A '' C)

Helper for Theorem 19.3: for fixed A, the image-preservation branch holds pointwise in the set variable.

theorem helperForTheorem_19_3_preimage_branch {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (D : Set (Fin m → ℝ)) : IsPolyhedralConvexSet m D → IsPolyhedralConvexSet n (⇑A ⁻¹' D)

Helper for Theorem 19.3: for fixed A, the preimage-preservation branch holds pointwise in the set variable.

theorem helperForTheorem_19_3_image_and_preimage_polyhedral {n m : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : (∀ (C : Set (Fin n → ℝ)), IsPolyhedralConvexSet n C → IsPolyhedralConvexSet m (⇑A '' C)) ∧ ∀ (D : Set (Fin m → ℝ)), IsPolyhedralConvexSet m D → IsPolyhedralConvexSet n (⇑A ⁻¹' D)

Helper for Theorem 19.3: for a fixed linear map, both the image-preservation and preimage-preservation polyhedrality statements hold together.

theorem polyhedralConvexSet_image_preimage_linear (n m : ℕ) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : (∀ (C : Set (Fin n → ℝ)), IsPolyhedralConvexSet n C → IsPolyhedralConvexSet m (⇑A '' C)) ∧ ∀ (D : Set (Fin m → ℝ)), IsPolyhedralConvexSet m D → IsPolyhedralConvexSet n (⇑A ⁻¹' D)

Theorem 19.3: Let A be a linear transformation from ℝ^n to ℝ^m. Then A '' C is a polyhedral convex set in ℝ^m for each polyhedral convex set C in ℝ^n, and A ⁻¹' D is a polyhedral convex set in ℝ^n for each polyhedral convex set D in ℝ^m.

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

Helper for Corollary 19.3.1: coordinate conjugate of linearMap_prod A between Fin-function models of product spaces.

Equations

• helperForCorollary_19_3_1_linearMapProdCoord A = ↑(prodLinearEquiv_append_coord m) ∘ₗ linearMap_prod A ∘ₗ ↑(prodLinearEquiv_append_coord n).symm

theorem helperForCorollary_19_3_1_image_linearMapProdCoord {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {S : Set ((Fin n → ℝ) × ℝ)} : (fun (p : (Fin m → ℝ) × ℝ) => (prodLinearEquiv_append_coord m) p) '' (⇑(linearMap_prod A) '' S) = ⇑(helperForCorollary_19_3_1_linearMapProdCoord A) '' ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' S)

Helper for Corollary 19.3.1: after converting product points to Fin coordinates, the image under linearMap_prod A is exactly the image under the conjugated map.

theorem helperForCorollary_19_3_1_transformedEpigraphCoord_inverseImage_eq_preimage {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {g : (Fin m → ℝ) → EReal} : (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ (inverseImageUnderLinearMap A g) = ⇑(helperForCorollary_19_3_1_linearMapProdCoord A) ⁻¹' ((fun (p : (Fin m → ℝ) × ℝ) => (prodLinearEquiv_append_coord m) p) '' epigraph Set.univ g)

Helper for Corollary 19.3.1: in Fin coordinates, the epigraph of inverseImageUnderLinearMap A g is the preimage of the transformed epigraph of g under the conjugated product map.

theorem helperForCorollary_19_3_1_closedProjectedEpigraph_of_polyhedralFunction {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) : IsClosed (⇑(linearMap_prod A) '' epigraph Set.univ f)

Helper for Corollary 19.3.1: the projected epigraph of a polyhedral convex function under linearMap_prod A is closed.

theorem helperForCorollary_19_3_1_transformedEpigraphCoord_imageUnderLinearMap_eq_image {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) : (fun (p : (Fin m → ℝ) × ℝ) => (prodLinearEquiv_append_coord m) p) '' epigraph Set.univ (imageUnderLinearMap A f) = ⇑(helperForCorollary_19_3_1_linearMapProdCoord A) '' ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f)

Helper for Corollary 19.3.1: in Fin coordinates, the epigraph of imageUnderLinearMap A f is exactly the image of the transformed epigraph of f under the conjugated product map.

theorem helperForCorollary_19_3_1_transformedEpigraph_imageUnderLinearMap_eq_embeddedImage {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) : (fun (p : (Fin m → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ (imageUnderLinearMap A f) = (fun (z : EuclideanSpace ℝ (Fin (n + 1))) => (linearMap_prod_embedded A) z) '' ((fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f)

Helper for Corollary 19.3.1: in embedded coordinates, the epigraph of imageUnderLinearMap is exactly the linear image of the embedded epigraph.

theorem helperForCorollary_19_3_1_attainment_of_finite_imageValue {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) (y : Fin m → ℝ) : (∃ (r : ℝ), imageUnderLinearMap A f y = ↑r) → ∃ (x : Fin n → ℝ), A x = y ∧ imageUnderLinearMap A f y = f x

Helper for Corollary 19.3.1: if imageUnderLinearMap A f y is finite, then the infimum is attained at some x with A x = y.

theorem helperForCorollary_19_3_1_transformedEpigraph_inverseImage_eq_embeddedPreimage {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {g : (Fin m → ℝ) → EReal} : (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ (inverseImageUnderLinearMap A g) = (fun (z : EuclideanSpace ℝ (Fin (n + 1))) => (linearMap_prod_embedded A) z) ⁻¹' ((fun (p : (Fin m → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ g)

Helper for Corollary 19.3.1: in embedded coordinates, the epigraph of inverseImageUnderLinearMap is the preimage of the embedded epigraph under linearMap_prod_embedded.

theorem helperForCorollary_19_3_1_polyhedral_imageUnderLinearMap {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) : IsPolyhedralConvexFunction m (imageUnderLinearMap A f)

Helper for Corollary 19.3.1: polyhedral convexity is preserved by imageUnderLinearMap for polyhedral convex functions.

theorem helperForCorollary_19_3_1_polyhedral_inverseImageUnderLinearMap {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {g : (Fin m → ℝ) → EReal} (hgpoly : IsPolyhedralConvexFunction m g) : IsPolyhedralConvexFunction n (inverseImageUnderLinearMap A g)

Helper for Corollary 19.3.1: polyhedral convexity is preserved by inverseImageUnderLinearMap for polyhedral convex functions.

theorem helperForCorollary_19_3_1_imageUnderLinearMap_polyhedral_and_attainment {n m : ℕ} {A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) : IsPolyhedralConvexFunction m (imageUnderLinearMap A f) ∧ ∀ (y : Fin m → ℝ), (∃ (r : ℝ), imageUnderLinearMap A f y = ↑r) → ∃ (x : Fin n → ℝ), A x = y ∧ imageUnderLinearMap A f y = f x

Helper for Corollary 19.3.1: polyhedrality of imageUnderLinearMap together with attainment of finite image values.

theorem polyhedralConvexFunction_image_preimage_linear (n m : ℕ) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) : (∀ (f : (Fin n → ℝ) → EReal), IsPolyhedralConvexFunction n f → IsPolyhedralConvexFunction m (imageUnderLinearMap A f) ∧ ∀ (y : Fin m → ℝ), (∃ (r : ℝ), imageUnderLinearMap A f y = ↑r) → ∃ (x : Fin n → ℝ), A x = y ∧ imageUnderLinearMap A f y = f x) ∧ ∀ (g : (Fin m → ℝ) → EReal), IsPolyhedralConvexFunction m g → IsPolyhedralConvexFunction n (inverseImageUnderLinearMap A g)

Corollary 19.3.1: Let A be a linear transformation from ℝ^n to ℝ^m. For each polyhedral convex function f on ℝ^n, the convex function Af is polyhedral on ℝ^m, and the infimum in its definition, if finite, is attained. For each polyhedral convex function g on ℝ^m, gA is polyhedral on ℝ^n.