theorem section16_supportFunctionEReal_iInter_eq_infimalConvolutionFamily_of_nonempty_iInter_ri_proof_step {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) (hC : ∀ (i : Fin m), Convex ℝ (C i)) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hri : (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C i)).Nonempty) : (supportFunctionEReal (⋂ (i : Fin m), C i) = infimalConvolutionFamily fun (i : Fin m) => supportFunctionEReal (C i)) ∧ ∀ (xStar : Fin n → ℝ), infimalConvolutionFamily (fun (i : Fin m) => supportFunctionEReal (C i)) xStar = ⊤ ∨ ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, supportFunctionEReal (C i) (xStarFamily i) = infimalConvolutionFamily (fun (i : Fin m) => supportFunctionEReal (C i)) xStar

Specializing Theorem 16.4.3 to indicator functions yields the support-function identity and the usual attainment/⊤ disjunction.

theorem section16_exists_xStarFamily_sum_eq_of_pos {n m : ℕ} (hm : 0 < m) (xStar : Fin n → ℝ) : ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar

When m > 0, any xStar admits a family summing to xStar.

theorem section16_attainment_when_infimalConvolutionFamily_eq_top_of_pos {n m : ℕ} (hm : 0 < m) (g : Fin m → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) (htop : infimalConvolutionFamily g xStar = ⊤) : ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, g i (xStarFamily i) = infimalConvolutionFamily g xStar

If the infimal convolution is ⊤ and m > 0, any fixed decomposition attains ⊤.

theorem section16_supportFunctionEReal_iInter_eq_infimalConvolutionFamily_of_nonempty_iInter_ri {n m : ℕ} (C : Fin m → Set (Fin n → ℝ)) (hC : ∀ (i : Fin m), Convex ℝ (C i)) (hCne : ∀ (i : Fin m), (C i).Nonempty) (hri : (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C i)).Nonempty) (hm : 0 < m) : (supportFunctionEReal (⋂ (i : Fin m), C i) = infimalConvolutionFamily fun (i : Fin m) => supportFunctionEReal (C i)) ∧ ∀ (xStar : Fin n → ℝ), ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, supportFunctionEReal (C i) (xStarFamily i) = infimalConvolutionFamily (fun (i : Fin m) => supportFunctionEReal (C i)) xStar

Corollary 16.4.1.3: Let C₁, …, Cₘ be non-empty convex sets in ℝⁿ. If the sets ri Cᵢ have a point in common, then the closure operation can be omitted from Corollary 16.4.1.2, and

δ^*(· | C₁ ∩ ⋯ ∩ Cₘ) = inf { δ^*(· | C₁) + ⋯ + δ^*(· | Cₘ) | x₁⋆ + ⋯ + xₘ⋆ = x⋆ },

where for each x⋆ the infimum is attained.

In this development, δ^* is supportFunctionEReal, ri is euclideanRelativeInterior, and the right-hand side is modeled by infimalConvolutionFamily.