Helper for Corollary 20.0.3: with an empty index family, any split-sum attainment witness for the conjugate infimal convolution forces the target vector to be zero.
Helper for Corollary 20.0.3: for an empty index family, the split-attainment condition is equivalent to the target covector being zero.
Helper for Corollary 20.0.3: with an empty index family, a nonzero target covector makes attainment-witness existence equivalent to False.
Helper for Corollary 20.0.3: with an empty index family, a nonzero target cannot admit any split-sum decomposition.
Helper for Corollary 20.0.3: with an empty index family, a nonzero target cannot admit an attainment witness for the conjugate infimal convolution split.
Helper for Corollary 20.0.3: if an empty-index model has at least one nonzero covector, then the universal attainment claim is impossible.
Helper for Corollary 20.0.3: in dimension one, the constant-one covector is nonzero.
Helper for Corollary 20.0.3: with an empty index family and nonzero dimension,
one cannot decompose every covector as a Fin 0-indexed split sum.
Helper for Corollary 20.0.3: with an empty index family and nonzero dimension, the constant-one covector admits no attainment witness for the conjugate split.
Helper for Corollary 20.0.3: with an empty index family and nonzero dimension, the constant-one covector is an explicit target with no attainment witness.
Helper for Corollary 20.0.3: with an empty index family and nonzero dimension, the universal attainment claim is impossible.
Helper for Corollary 20.0.3: in the empty-index case, if universal attainment holds, then the ambient dimension must be zero.
Helper for Corollary 20.0.3: with an empty index family, universal attainment fails already for the one-dimensional constant-one target covector.
Helper for Corollary 20.0.3: in zero dimension, every covector is zero.
Helper for Corollary 20.0.3: with an empty index family and nonzero dimension, the full refinement-plus-universal-attainment conclusion is impossible.
Helper for Corollary 20.0.3: there is explicit empty-index data satisfying all hypotheses while universal attainment fails in dimension one.
Helper for Corollary 20.0.3: in the concrete branch m = 0, n = 1,
the standard hypotheses do not imply universal split-attainment.
Helper for Corollary 20.0.3: in the concrete branch m = 0, n = 1,
the full refinement-plus-universal-attainment conclusion cannot follow from the
standard hypotheses.
Helper for Corollary 20.0.3: the hypotheses do not imply the full
refinement-plus-universal-attainment conclusion in all dimensions/index sizes.
The branch n = 1, m = 0 gives a concrete obstruction.
Helper for Corollary 20.0.3: in the branch m = 0, n = 1, the constant-one
target covector cannot be represented as a Fin 0-indexed split sum.
Helper for Corollary 20.0.3: in the branch m = 0 and n ≠ 0,
the standard polyhedral/proper/domain hypotheses still do not imply universal
split-attainment.
Helper for Corollary 20.0.3: in the branch m = 0 and n ≠ 0,
the full refinement-plus-universal-attainment conclusion is incompatible even
under the standard polyhedral/proper/domain hypotheses.
Helper for Corollary 20.0.3: when 0 < m, each covector admits an attaining split
for the infimal convolution of conjugates.
Helper for Corollary 20.0.3: if the index family is nonempty (0 < m), then the
polyhedral sum-conjugate identity and universal attainment conclusion both hold.
Corollary 20.0.3: In the polyhedral case, Theorem 20.0.1 yields the sum-conjugate/infimal-convolution identity without closure, under the simpler condition dom f₁ ∩ ⋯ ∩ dom fₘ ≠ ∅, and the infimum in the infimal convolution is attained.
Helper for Theorem 20.0.4: every summand indexed by Ipoly is closed proper
polyhedral, hence equal to its convex-function closure.
Helper for Theorem 20.0.4: unpack a witness from the mixed
dom/ri-intersection assumption into pointwise membership facts.
Helper for Theorem 20.0.4: mixed dom/ri qualification should identify the
sum-of-closures with the closure of the sum.
Helper for Theorem 20.0.4: rewrite both full sums into Ipoly and Ipolyᶜ
filter blocks, and remove closures on the polyhedral block.
Helper for Theorem 20.0.4: the mixed hypothesis yields nonempty intersection of relative interiors on the nonpolyhedral block.
Helper for Theorem 20.0.4: the mixed qualification provides a common effective-domain point for all nonpolyhedral indices.
Helper for Theorem 20.0.4: the filtered nonpolyhedral block is proper, using the common effective-domain point extracted from the mixed qualification.
Helper for Theorem 20.0.4: the nonpolyhedral filtered block satisfies the
Section 16 closure-of-sum identity under the extracted ri qualification.
Helper for Theorem 20.0.4: the polyhedral filtered block is proper and has a domain witness extracted from the mixed qualification point.
Helper for Theorem 20.0.4: the mixed qualification yields a single witness that lies in the polyhedral filtered-block effective domain and in the relative interior of the nonpolyhedral filtered-block effective domain.
Helper for Theorem 20.0.4: reduced mixed bridge after splitting into poly/nonpoly filter blocks.
Helper for Theorem 20.0.4: reduced mixed bridge after splitting into poly/nonpoly filter blocks.
Theorem 20.0.4: Let f₁, …, fₘ be proper convex functions on ℝⁿ, let
I_poly be the set of indices for which fᵢ is polyhedral, and let
I_gen = I_polyᶜ. If
(⋂_{i ∈ I_poly} dom fᵢ) ∩ (⋂_{i ∈ I_gen} ri (dom fᵢ)) ≠ ∅,
then
(f₁ + ⋯ + fₘ)^* = cl (f₁^* □ ⋯ □ fₘ^*).
Here dom fᵢ is effectiveDomain univ (f i), ri is euclideanRelativeInterior,
^* is fenchelConjugate, □ is infimalConvolutionFamily, and cl is
convexFunctionClosure.
Theorem 20.1: Let f₁, …, fₘ be proper convex functions on ℝⁿ such that f₁, …, f_k are polyhedral. Assume
dom f₁ ∩ ⋯ ∩ dom f_k ∩ ri (dom f_{k+1}) ∩ ⋯ ∩ ri (dom fₘ) ≠ ∅.
Also assume 0 < m.
Then (f₁ + ⋯ + fₘ)^* = f₁^* □ ⋯ □ fₘ^*, and for each x⋆ the infimum in the infimal-convolution formula is attained by a decomposition x⋆ = x⋆₁ + ⋯ + x⋆ₘ.
Corollary 20.1.1: Let f₁, …, fₘ be closed proper convex functions on ℝⁿ such that
f₁, …, f_k are polyhedral. If
dom f₁^* ∩ ⋯ ∩ dom f_k^* ∩ ri (dom f_{k+1}^*) ∩ ⋯ ∩ ri (dom fₘ^*) ≠ ∅,
and 0 < m,
then f₁ □ ⋯ □ fₘ is closed proper convex, and for every x the infimum in the
definition of f₁ □ ⋯ □ fₘ at x is attained.
Theorem 20.2: Let C₁ and C₂ be non-empty convex sets in ℝ^n, with C₁ polyhedral.
There exists a hyperplane that separates C₁ and C₂ properly and does not contain C₂
if and only if C₁ ∩ ri C₂ = ∅ (with ri formalized as intrinsicInterior).
Corollary 20.2.1: Let C₁ and C₂ be non-empty convex sets in ℝ^n with C₁
polyhedral. Then C₁ ∩ ri C₂ is nonempty if and only if every x⋆ satisfying
δ*(x⋆ | C₁) ≤ -δ*(-x⋆ | C₂) also satisfies δ*(x⋆ | C₁) = δ*(x⋆ | C₂)
(formalized with ri = intrinsicInterior and δ* = deltaStar).
Theorem 20.3: Let C₁ and C₂ be non-empty convex sets in ℝ^n, with C₁ polyhedral
and C₂ closed. If every recession direction z of C₁ such that -z is a recession
direction of C₂ is also a recession direction of C₂ (so C₂ is linear in that
direction), then C₁ + C₂ is closed.
Corollary 20.3.1: Let C₁ and C₂ be non-empty convex sets in ℝ^n such that C₁ is
polyhedral, C₂ is closed, and C₁ ∩ C₂ = ∅. Suppose C₁ and C₂ have no common recession
directions except those in which C₂ is linear (formalized as: if z is a recession direction of
both sets, then -z is also a recession direction of C₂). Then there exists a hyperplane
separating C₁ and C₂ strongly.
Theorem 20.4: Let C be a nonempty closed bounded convex set, and let D be a convex
set with C ⊆ interior D. Then there exists a polyhedral convex set P such that
P ⊆ interior D and C ⊆ interior P.
Theorem 20.5: Every polyhedral convex set is locally simplicial. In particular, every polytope is locally simplicial.