theorem helperForTheorem_20_0_1_convexFunctionClosure_eq_self_eachSummand {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (i : Fin m) : convexFunctionClosure (f i) = f i

Helper for Theorem 20.0.1: each polyhedral proper summand equals its convex-function closure.

theorem helperForTheorem_20_0_1_main_rewrite_from_section16 {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : (fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x) = convexFunctionClosure (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i))

Helper for Theorem 20.0.1: Theorem 16.4.2 rewrites to a closure identity after removing closures on each polyhedral summand.

theorem helperForTheorem_20_0_1_infimalConvolutionFamily_fenchelConjugate_ne_bot {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) (xStar : Fin n → ℝ) : infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar ≠ ⊥

Helper for Theorem 20.0.1: a common effective-domain point gives a finite lower bound, hence the infimal convolution of conjugates never takes the value ⊥.

theorem helperForTheorem_20_0_1_convexFunctionClosure_rhs_eq_self {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) : convexFunctionClosure (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) = infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)

Helper for Theorem 20.0.1: closure-removal on the infimal convolution side.

theorem fenchelConjugate_sum_eq_infimalConvolutionFamily_of_polyhedral_of_nonempty_iInter_effectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) : (fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x) = infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)

Theorem 20.0.1: Let f₁, …, fₘ be proper polyhedral convex functions on ℝⁿ with dom f₁ ∩ ⋯ ∩ dom fₘ ≠ ∅ (formalized as nonempty intersection of effective domains on univ). Then the Fenchel conjugate of their pointwise sum equals the infimal convolution of their Fenchel conjugates.

theorem helperForCorollary_20_0_2_sum_eq_zero_of_index_empty {n : ℕ} (xStarFamily : Fin 0 → Fin n → ℝ) : ∑ i : Fin 0, xStarFamily i = 0

Helper for Corollary 20.0.2: for an empty index family, the split sum is the zero vector.

theorem helperForCorollary_20_0_2_no_decomposition_of_nonzero_of_index_empty {n : ℕ} {xStar : Fin n → ℝ} (hxStar : xStar ≠ 0) : ¬∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar

Helper for Corollary 20.0.2: with empty index set, no nonzero vector has a split-sum decomposition.

theorem helperForCorollary_20_0_2_exists_nonzero_vector_of_pos {n : ℕ} (hn : 0 < n) : ∃ (xStar : Fin n → ℝ), xStar ≠ 0

Helper for Corollary 20.0.2: when 0 < n, there exists a nonzero vector in Fin n → ℝ.

theorem helperForCorollary_20_0_2_eq_zero_of_n_eq_zero {n : ℕ} (hn : n = 0) (xStar : Fin n → ℝ) : xStar = 0

Helper for Corollary 20.0.2: when n = 0, every vector in Fin n → ℝ is zero.

theorem helperForCorollary_20_0_2_not_forall_exists_decomposition_of_index_empty_of_pos {n : ℕ} (hn : 0 < n) : ¬∀ (xStar : Fin n → ℝ), ∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar

Helper for Corollary 20.0.2: when m = 0 and 0 < n, it is impossible to decompose every target vector as a split sum indexed by Fin 0.

theorem helperForCorollary_20_0_2_infimalConvolutionFamily_eq_if_of_index_empty {n : ℕ} (g : Fin 0 → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : infimalConvolutionFamily g xStar = if xStar = 0 then 0 else ⊤

Helper for Corollary 20.0.2: for an empty index family, the family infimal convolution is 0 exactly at the zero vector and ⊤ otherwise.

theorem helperForCorollary_20_0_2_infimalConvolutionFamily_eq_top_of_nonzero_of_index_empty {n : ℕ} (g : Fin 0 → (Fin n → ℝ) → EReal) {xStar : Fin n → ℝ} (hxStar : xStar ≠ 0) : infimalConvolutionFamily g xStar = ⊤

Helper for Corollary 20.0.2: for an empty index family, every nonzero target has infimal convolution value ⊤.

theorem helperForCorollary_20_0_2_not_forall_attainment_of_index_empty_of_pos {n : ℕ} (hn : 0 < n) (g : Fin 0 → (Fin n → ℝ) → EReal) : ¬∀ (xStar : Fin n → ℝ), ∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily g xStar = ∑ i : Fin 0, g i (xStarFamily i)

Helper for Corollary 20.0.2: when m = 0 and 0 < n, universal attainment with a split-sum decomposition is impossible (independently of the function family values).

theorem helperForCorollary_20_0_2_no_attainmentWitness_of_nonzero_of_index_empty {n : ℕ} (g : Fin 0 → (Fin n → ℝ) → EReal) {xStar : Fin n → ℝ} (hxStar : xStar ≠ 0) : ¬∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily g xStar = ∑ i : Fin 0, g i (xStarFamily i)

Helper for Corollary 20.0.2: with empty index set, a nonzero target cannot admit an attainment witness in split-sum form.

theorem helperForCorollary_20_0_2_exists_counterexample_attainment_of_index_empty_of_pos {n : ℕ} (hn : 0 < n) (g : Fin 0 → (Fin n → ℝ) → EReal) : ∃ (xStar : Fin n → ℝ), ¬∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily g xStar = ∑ i : Fin 0, g i (xStarFamily i)

Helper for Corollary 20.0.2: when m = 0 and 0 < n, there exists a target vector without a split-sum attainment witness.

theorem helperForCorollary_20_0_2_exists_nonzero_counterexample_for_fenchelFamily_of_index_empty_of_pos {n : ℕ} (hn : 0 < n) (f : Fin 0 → (Fin n → ℝ) → EReal) : ∃ (xStar : Fin n → ℝ), xStar ≠ 0 ∧ ¬∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily (fun (i : Fin 0) => fenchelConjugate n (f i)) xStar = ∑ i : Fin 0, fenchelConjugate n (f i) (xStarFamily i)

Helper for Corollary 20.0.2: when m = 0 and 0 < n, there exists a nonzero target vector that has no split-sum attainment witness for the conjugate family.

theorem helperForCorollary_20_0_2_not_forall_attainment_for_fenchelFamily_of_index_empty_of_pos {n : ℕ} (hn : 0 < n) (f : Fin 0 → (Fin n → ℝ) → EReal) : ¬∀ (yStar : Fin n → ℝ), ∃ (yStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, yStarFamily i = yStar ∧ infimalConvolutionFamily (fun (i : Fin 0) => fenchelConjugate n (f i)) yStar = ∑ i : Fin 0, fenchelConjugate n (f i) (yStarFamily i)

Helper for Corollary 20.0.2: when m = 0 and 0 < n, universal split-sum attainment fails for the conjugate family.

theorem helperForCorollary_20_0_2_attainmentWitness_target_eq_zero_of_index_empty {n : ℕ} (g : Fin 0 → (Fin n → ℝ) → EReal) {xStar : Fin n → ℝ} (hAtt : ∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily g xStar = ∑ i : Fin 0, g i (xStarFamily i)) : xStar = 0

Helper for Corollary 20.0.2: with empty index set, any split-sum attainment witness forces the target vector to be zero.

theorem helperForCorollary_20_0_2_exists_attainmentWitness_of_zero_of_index_empty {n : ℕ} (g : Fin 0 → (Fin n → ℝ) → EReal) : ∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = 0 ∧ infimalConvolutionFamily g 0 = ∑ i : Fin 0, g i (xStarFamily i)

Helper for Corollary 20.0.2: with empty index set and zero target, a split-sum attainment witness exists.

theorem helperForCorollary_20_0_2_exists_attainmentWitness_iff_target_eq_zero_of_index_empty {n : ℕ} (g : Fin 0 → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : (∃ (xStarFamily : Fin 0 → Fin n → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily g xStar = ∑ i : Fin 0, g i (xStarFamily i)) ↔ xStar = 0

Helper for Corollary 20.0.2: with empty index set, a split-sum attainment witness exists exactly at the zero target.

theorem helperForCorollary_20_0_2_exists_attainment_of_ne_top_of_top_or_exists {n m : ℕ} (g : Fin m → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) (hTopOrAttained : infimalConvolutionFamily g xStar = ⊤ ∨ ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, g i (xStarFamily i) = infimalConvolutionFamily g xStar) (htop : infimalConvolutionFamily g xStar ≠ ⊤) : ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ infimalConvolutionFamily g xStar = ∑ i : Fin m, g i (xStarFamily i)

Helper for Corollary 20.0.2: if the infimal-convolution value is not ⊤ and one has the standard ⊤-or-attainment alternative, then an attainment witness exists in the orientation used by the corollary statement.

theorem helperForCorollary_20_0_2_sum_headTail_rewrite {n k : ℕ} (xStarFamily : Fin (k + 1) → Fin n → ℝ) : ∑ i : Fin (k + 1), xStarFamily i = xStarFamily 0 + ∑ j : Fin k, xStarFamily j.succ

Helper for Corollary 20.0.2: rewrite a split sum over Fin (k+1) as head plus tail.

theorem helperForCorollary_20_0_2_liftWitness_from_headTail {n k : ℕ} (g : Fin (k + 1) → (Fin n → ℝ) → EReal) {xStar x0 y : Fin n → ℝ} (tailFamily : Fin k → Fin n → ℝ) (hHeadTail : x0 + y = xStar) (hTailSum : ∑ j : Fin k, tailFamily j = y) : ∃ (xStarFamily : Fin (k + 1) → Fin n → ℝ), ∑ i : Fin (k + 1), xStarFamily i = xStar ∧ ∑ i : Fin (k + 1), g i (xStarFamily i) = g 0 x0 + ∑ j : Fin k, g j.succ (tailFamily j)

Helper for Corollary 20.0.2: from a head point and a tail family summing to y, build a full Fin (k+1) split family and rewrite its value-sum in head-tail form.

theorem helperForCorollary_20_0_2_nonempty_iInter_effectiveDomain_tail {n k : ℕ} (f : Fin (k + 1) → (Fin n → ℝ) → EReal) (hdom : (⋂ (i : Fin (k + 1)), effectiveDomain Set.univ (f i)).Nonempty) : (⋂ (j : Fin k), effectiveDomain Set.univ (f j.succ)).Nonempty

Helper for Corollary 20.0.2: from a common effective-domain point for a Fin (k+1) family, obtain one for its tail Fin k subfamily.

theorem helperForCorollary_20_0_2_properSum_of_commonEffectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x

Helper for Corollary 20.0.2: the pointwise sum x ↦ ∑ i, f i x is proper whenever the summands are proper and their effective domains have a common point.

theorem helperForCorollary_20_0_2_properInfConjFamily_of_polyhedral_nonempty_iInter_effectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) : ProperConvexFunctionOn Set.univ (infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i))

Helper for Corollary 20.0.2: under Theorem 20.0.1 hypotheses, the family infimal convolution of conjugates is proper.

theorem helperForCorollary_20_0_2_infimalConvolution_headTail_le_infimalConvolutionFamily {n k : ℕ} (g : Fin (k + 1) → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : infimalConvolution (g 0) (fun (y : Fin n → ℝ) => infimalConvolutionFamily (fun (j : Fin k) => g j.succ) y) xStar ≤ infimalConvolutionFamily g xStar

Helper for Corollary 20.0.2: the binary head-tail infimal convolution is bounded above by the full family infimal convolution.

@[irreducible]

theorem helperForCorollary_20_0_2_polyhedralSum_of_polyhedral_nonempty_iInter_effectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) (hmPos : 0 < m) : IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x

Helper for Corollary 20.0.2: for a nonempty family of proper polyhedral summands with a common effective-domain point, the pointwise sum is polyhedral.

@[irreducible]

theorem helperForCorollary_20_0_2_topOrAttained_of_polyhedral_nonempty_iInter_effectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) (hmPos : 0 < m) (xStar : Fin n → ℝ) : infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar = ⊤ ∨ ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, fenchelConjugate n (f i) (xStarFamily i) = infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar

Helper for Corollary 20.0.2: under the hypotheses of Theorem 20.0.1 and 0 < m, the family infimal-convolution value is either ⊤ or attained in split-sum form.

theorem infimalConvolutionFamily_fenchelConjugate_attained_of_polyhedral_of_nonempty_iInter_effectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hpoly : ∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hdom : (⋂ (i : Fin m), effectiveDomain Set.univ (f i)).Nonempty) (hmPos : 0 < m) (xStar : Fin n → ℝ) : ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar = ∑ i : Fin m, fenchelConjugate n (f i) (xStarFamily i)

Corollary 20.0.2: Under the hypotheses of Theorem 20.0.1 and 0 < m, for each x⋆ ∈ ℝ^n there exists a decomposition x⋆ = ∑ i, x⋆ᵢ such that (f₁^* ⋄ ⋯ ⋄ fₘ^*)(x⋆) = ∑ i, fᵢ^*(x⋆ᵢ), i.e. the infimum in the definition of the infimal convolution of the conjugates is attained.