theorem helperForCorollary_19_3_2_polyhedral_preimage_intersection {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (A₁ A₂ : (Fin (n + n) → ℝ) →ₗ[ℝ] Fin n → ℝ) (hC₁ : IsPolyhedralConvexSet n C₁) (hC₂ : IsPolyhedralConvexSet n C₂) : IsPolyhedralConvexSet (n + n) (⇑A₁ ⁻¹' C₁ ∩ ⇑A₂ ⁻¹' C₂)

Helper for Corollary 19.3.2: the intersection of the two split preimages is polyhedral whenever the two source sets are polyhedral.

theorem helperForCorollary_19_3_2_image_polyhedral_of_polyhedralCarrier {n : ℕ} (B : (Fin (n + n) → ℝ) →ₗ[ℝ] Fin n → ℝ) (P : Set (Fin (n + n) → ℝ)) (hPpoly : IsPolyhedralConvexSet (n + n) P) : IsPolyhedralConvexSet n (⇑B '' P)

Helper for Corollary 19.3.2: a linear image of a polyhedral carrier in Fin (n+n) → ℝ is polyhedral in Fin n → ℝ.

theorem helperForCorollary_19_3_2_append_split_projection_eval {n : ℕ} (u v : Fin n → ℝ) : (LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.castAdd n i)) (Fin.append u v) = u ∧ (LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.natAdd n i)) (Fin.append u v) = v

Helper for Corollary 19.3.2: split projections recover the two components from Fin.append.

theorem helperForCorollary_19_3_2_append_mem_split_preimage_intersection {n : ℕ} (C₁ C₂ : Set (Fin n → ℝ)) (A₁ A₂ : (Fin (n + n) → ℝ) →ₗ[ℝ] Fin n → ℝ) (hA₁ : A₁ = LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.castAdd n i)) (hA₂ : A₂ = LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.natAdd n i)) (u v : Fin n → ℝ) (hu : u ∈ C₁) (hv : v ∈ C₂) : Fin.append u v ∈ ⇑A₁ ⁻¹' C₁ ∩ ⇑A₂ ⁻¹' C₂

Helper for Corollary 19.3.2: appending witnesses from C₁ and C₂ produces a point in the split-preimage intersection carrier.

theorem helperForCorollary_19_3_2_sumMap_image_eq_setAdd {n : ℕ} (C₁ C₂ : Set (Fin n → ℝ)) (A₁ A₂ B : (Fin (n + n) → ℝ) →ₗ[ℝ] Fin n → ℝ) (hA₁ : A₁ = LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.castAdd n i)) (hA₂ : A₂ = LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.natAdd n i)) (hB : B = A₁ + A₂) : ⇑B '' (⇑A₁ ⁻¹' C₁ ∩ ⇑A₂ ⁻¹' C₂) = C₁ + C₂

Helper for Corollary 19.3.2: the split-sum linear image of the split-preimage carrier is exactly the Minkowski sum C₁ + C₂.

theorem polyhedral_convexSet_add (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) : IsPolyhedralConvexSet n C₁ → IsPolyhedralConvexSet n C₂ → IsPolyhedralConvexSet n (C₁ + C₂)

Corollary 19.3.2: If C₁ and C₂ are polyhedral convex sets in ℝ^n, then C₁ + C₂ is polyhedral.

theorem helperForCorollary_19_3_3_polyhedral_implies_convex_pair {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hC₁poly : IsPolyhedralConvexSet n C₁) (hC₂poly : IsPolyhedralConvexSet n C₂) : Convex ℝ C₁ ∧ Convex ℝ C₂

Helper for Corollary 19.3.3: polyhedral convexity of each set implies convexity of both.

theorem helperForCorollary_19_3_3_neg_polyhedral {n : ℕ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolyhedralConvexSet n C) : IsPolyhedralConvexSet n (-C)

Helper for Corollary 19.3.3: negation preserves polyhedral convexity.

theorem helperForCorollary_19_3_3_sub_polyhedral_closed {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hC₁poly : IsPolyhedralConvexSet n C₁) (hC₂poly : IsPolyhedralConvexSet n C₂) : IsPolyhedralConvexSet n (C₁ - C₂) ∧ IsClosed (C₁ - C₂)

Helper for Corollary 19.3.3: the set difference C₁ - C₂ is polyhedral and closed.

theorem helperForCorollary_19_3_3_zero_not_mem_sub_of_disjoint {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hdisj : Disjoint C₁ C₂) : 0 ∉ C₁ - C₂

Helper for Corollary 19.3.3: disjointness excludes 0 from the set difference C₁ - C₂.

theorem helperForCorollary_19_3_3_zero_not_mem_closure_sub {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hdisj : Disjoint C₁ C₂) (hSubClosed : IsClosed (C₁ - C₂)) : 0 ∉ closure (C₁ - C₂)

Helper for Corollary 19.3.3: disjointness and closedness of C₁ - C₂ force 0 ∉ closure (C₁ - C₂).

theorem helperForCorollary_19_3_3_apply_strongSeparation_iff {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) (h0notClosure : 0 ∉ closure (C₁ - C₂)) : ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂

Helper for Corollary 19.3.3: the Theorem 11.4 criterion yields a strongly separating hyperplane from 0 ∉ closure (C₁ - C₂).

theorem exists_hyperplaneSeparatesStrongly_of_disjoint_polyhedralConvex (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) : C₁.Nonempty → C₂.Nonempty → Disjoint C₁ C₂ → IsPolyhedralConvexSet n C₁ → IsPolyhedralConvexSet n C₂ → ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂

Corollary 19.3.3: If C₁ and C₂ are non-empty disjoint polyhedral convex sets, there exists a hyperplane separating C₁ and C₂ strongly.

theorem helperForCorollary_19_3_4_imageUnder_sumMap_eq_infimalConvolution {n : ℕ} (f₁ f₂ : (Fin n → ℝ) → EReal) : have A₁ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.castAdd n i); have A₂ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.natAdd n i); have B := A₁ + A₂; have h := fun (z : Fin (n + n) → ℝ) => f₁ (A₁ z) + f₂ (A₂ z); imageUnderLinearMap B h = infimalConvolution f₁ f₂

Helper for Corollary 19.3.4: infimalConvolution is an image-under-linear-map infimum for the split-coordinate sum map.

theorem helperForCorollary_19_3_4_realSplit_of_sum_le_coe {a b : EReal} {μ : ℝ} (ha_bot : a ≠ ⊥) (hb_bot : b ≠ ⊥) (hab : a + b ≤ ↑μ) : ∃ (μ₁ : ℝ) (μ₂ : ℝ), a ≤ ↑μ₁ ∧ b ≤ ↑μ₂ ∧ μ₁ + μ₂ = μ

Helper for Corollary 19.3.4: split a finite real upper bound on a + b into real upper bounds on each summand, assuming neither summand is ⊥.

theorem helperForCorollary_19_3_4_transformedProjectedEpigraph_eq_sum {n : ℕ} (f₁ f₂ : (Fin n → ℝ) → EReal) (hproper₁ : ProperConvexFunctionOn Set.univ f₁) (hproper₂ : ProperConvexFunctionOn Set.univ f₂) : have A₁ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.castAdd n i); have A₂ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.natAdd n i); have B := A₁ + A₂; have h := fun (z : Fin (n + n) → ℝ) => f₁ (A₁ z) + f₂ (A₂ z); (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' (⇑(linearMap_prod B) '' epigraph Set.univ h) = (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f₁ + (fun (p : (Fin n → ℝ) × ℝ) => prodLinearEquiv_append p) '' epigraph Set.univ f₂

Helper for Corollary 19.3.4: the transformed projected epigraph of the split-sum model equals the Minkowski sum of the transformed epigraphs of f₁ and f₂.

theorem helperForCorollary_19_3_4_transformedProjectedEpigraph_eq_sum_coord {n : ℕ} (f₁ f₂ : (Fin n → ℝ) → EReal) (hproper₁ : ProperConvexFunctionOn Set.univ f₁) (hproper₂ : ProperConvexFunctionOn Set.univ f₂) : have A₁ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.castAdd n i); have A₂ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.natAdd n i); have B := A₁ + A₂; have h := fun (z : Fin (n + n) → ℝ) => f₁ (A₁ z) + f₂ (A₂ z); (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' (⇑(linearMap_prod B) '' epigraph Set.univ h) = (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f₁ + (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f₂

Helper for Corollary 19.3.4: coordinate version of helperForCorollary_19_3_4_transformedProjectedEpigraph_eq_sum.

theorem helperForCorollary_19_3_4_projectedEpigraph_closed {n : ℕ} (f₁ f₂ : (Fin n → ℝ) → EReal) (hf₁poly : IsPolyhedralConvexFunction n f₁) (hf₂poly : IsPolyhedralConvexFunction n f₂) (hproper₁ : ProperConvexFunctionOn Set.univ f₁) (hproper₂ : ProperConvexFunctionOn Set.univ f₂) : have A₁ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.castAdd n i); have A₂ := LinearMap.pi fun (i : Fin n) => LinearMap.proj (Fin.natAdd n i); have B := A₁ + A₂; have h := fun (z : Fin (n + n) → ℝ) => f₁ (A₁ z) + f₂ (A₂ z); IsClosed (⇑(linearMap_prod B) '' epigraph Set.univ h)

Helper for Corollary 19.3.4: the projected epigraph of the split-sum model is closed, via its transformed description as a sum of transformed polyhedral epigraphs.

theorem helperForCorollary_19_3_4_polyhedralEpigraph_infimalConvolution {n : ℕ} (f₁ f₂ : (Fin n → ℝ) → EReal) (hf₁poly : IsPolyhedralConvexFunction n f₁) (hf₂poly : IsPolyhedralConvexFunction n f₂) (hproper₁ : ProperConvexFunctionOn Set.univ f₁) (hproper₂ : ProperConvexFunctionOn Set.univ f₂) : IsPolyhedralConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append p).ofLp) '' epigraph Set.univ (infimalConvolution f₁ f₂))

Helper for Corollary 19.3.4: the transformed epigraph of infimalConvolution f₁ f₂ is polyhedral, obtained from the closed projected-epigraph identity and the transformed sum description.

theorem helperForCorollary_19_3_4_eq_sub_of_add_eq {n : ℕ} {u v x : Fin n → ℝ} (h : u + v = x) : u = x - v

Helper for Corollary 19.3.4: isolate the first summand in an equality u + v = x as u = x - v.

theorem helperForCorollary_19_3_4_attainment_of_finite_value {n : ℕ} (f₁ f₂ : (Fin n → ℝ) → EReal) (hf₁poly : IsPolyhedralConvexFunction n f₁) (hf₂poly : IsPolyhedralConvexFunction n f₂) (hproper₁ : ProperConvexFunctionOn Set.univ f₁) (hproper₂ : ProperConvexFunctionOn Set.univ f₂) (x : Fin n → ℝ) {r : ℝ} (hr : infimalConvolution f₁ f₂ x = ↑r) : ∃ (y : Fin n → ℝ), infimalConvolution f₁ f₂ x = f₁ (x - y) + f₂ y

Helper for Corollary 19.3.4: when the infimal-convolution value at x is finite, the infimum is attained by some y.

theorem helperForCorollary_19_3_4_attainment_of_top_value {n : ℕ} (f₁ f₂ : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) (htop : infimalConvolution f₁ f₂ x = ⊤) : ∃ (y : Fin n → ℝ), infimalConvolution f₁ f₂ x = f₁ (x - y) + f₂ y

Helper for Corollary 19.3.4: if the infimal-convolution value at x is ⊤, the defining infimum is attained by the witness y = 0.

theorem helperForCorollary_19_3_4_eq_coe_toReal_of_ne_top_ne_bot {v : EReal} (hTop : v ≠ ⊤) (hBot : v ≠ ⊥) : v = ↑v.toReal

Helper for Corollary 19.3.4: any EReal value that is neither ⊤ nor ⊥ equals the coercion of its toReal value.

theorem polyhedralConvexFunction_infimalConvolution (n : ℕ) (f₁ f₂ : (Fin n → ℝ) → EReal) : IsPolyhedralConvexFunction n f₁ → IsPolyhedralConvexFunction n f₂ → ProperConvexFunctionOn Set.univ f₁ → ProperConvexFunctionOn Set.univ f₂ → IsPolyhedralConvexFunction n (infimalConvolution f₁ f₂) ∧ (ProperConvexFunctionOn Set.univ (infimalConvolution f₁ f₂) → ∀ (x : Fin n → ℝ), ∃ (y : Fin n → ℝ), infimalConvolution f₁ f₂ x = f₁ (x - y) + f₂ y)

Corollary 19.3.4: If f₁ and f₂ are proper polyhedral convex functions on ℝ^n, then infimalConvolution f₁ f₂ is a polyhedral convex function. Moreover, if infimalConvolution f₁ f₂ is proper, the infimum in the definition of (f₁ \sqcup f₂)(x) is attained for each x.