theorem helperForCorollary_20_0_3_attainment_target_eq_zero_of_empty_index {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) {xStar : Fin n → ℝ} (hAtt : ∃ (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)) : xStar = 0

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.

theorem helperForCorollary_20_0_3_exists_attainmentWitness_iff_target_eq_zero_of_empty_index {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : (∃ (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)) ↔ xStar = 0

Helper for Corollary 20.0.3: for an empty index family, the split-attainment condition is equivalent to the target covector being zero.

theorem helperForCorollary_20_0_3_exists_attainmentWitness_iff_false_of_empty_index_of_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) (hxStar : 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)) ↔ False

Helper for Corollary 20.0.3: with an empty index family, a nonzero target covector makes attainment-witness existence equivalent to False.

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

Helper for Corollary 20.0.3: with an empty index family, a nonzero target cannot admit any split-sum decomposition.

theorem helperForCorollary_20_0_3_no_attainment_witness_of_empty_index_of_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) {xStar : Fin n → ℝ} (hxStar : 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.3: with an empty index family, a nonzero target cannot admit an attainment witness for the conjugate infimal convolution split.

theorem helperForCorollary_20_0_3_universalAttainment_impossible_of_empty_index_of_exists_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hne : ∃ (xStar : Fin n → ℝ), xStar ≠ 0) : ¬∀ (xStar : Fin n → ℝ), ∃ (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.3: if an empty-index model has at least one nonzero covector, then the universal attainment claim is impossible.

theorem helperForCorollary_20_0_3_unitCovector_ne_zero : (fun (x : Fin 1) => 1) ≠ 0

Helper for Corollary 20.0.3: in dimension one, the constant-one covector is nonzero.

theorem helperForCorollary_20_0_3_constOneCovector_ne_zero_of_dim_ne_zero {n : ℕ} (hnZero : n ≠ 0) : (fun (x : Fin n) => 1) ≠ 0

Helper for Corollary 20.0.3: in any nonzero dimension, the constant-one covector is nonzero.

theorem helperForCorollary_20_0_3_exists_nonzero_covector_of_dim_ne_zero {n : ℕ} (hnZero : n ≠ 0) : ∃ (xStar : Fin n → ℝ), xStar ≠ 0

Helper for Corollary 20.0.3: in nonzero dimension there exists a nonzero covector.

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

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.

theorem helperForCorollary_20_0_3_no_attainment_witness_for_constOne_of_empty_index_of_dim_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hnZero : n ≠ 0) : ¬∃ (xStarFamily : Fin 0 → Fin n → ℝ), (∑ i : Fin 0, xStarFamily i = fun (x : Fin n) => 1) ∧ (infimalConvolutionFamily (fun (i : Fin 0) => fenchelConjugate n (f i)) fun (x : Fin n) => 1) = ∑ i : Fin 0, fenchelConjugate n (f i) (xStarFamily i)

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.

theorem helperForCorollary_20_0_3_exists_counterexample_no_attainment_of_empty_index_of_dim_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hnZero : n ≠ 0) : ∃ (xStar : Fin n → ℝ), ¬∃ (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.3: with an empty index family and nonzero dimension, the constant-one covector is an explicit target with no attainment witness.

theorem helperForCorollary_20_0_3_universalAttainment_impossible_of_empty_index_of_dim_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hnZero : n ≠ 0) : ¬∀ (xStar : Fin n → ℝ), ∃ (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.3: with an empty index family and nonzero dimension, the universal attainment claim is impossible.

theorem helperForCorollary_20_0_3_dim_eq_zero_of_empty_index_of_universalAttainment {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hAll : ∀ (xStar : Fin n → ℝ), ∃ (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)) : n = 0

Helper for Corollary 20.0.3: in the empty-index case, if universal attainment holds, then the ambient dimension must be zero.

theorem helperForCorollary_20_0_3_universalAttainment_impossible_of_empty_index (f : Fin 0 → (Fin 1 → ℝ) → EReal) : ¬∀ (xStar : Fin 1 → ℝ), ∃ (xStarFamily : Fin 0 → Fin 1 → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily (fun (i : Fin 0) => fenchelConjugate 1 (f i)) xStar = ∑ i : Fin 0, fenchelConjugate 1 (f i) (xStarFamily i)

Helper for Corollary 20.0.3: with an empty index family, universal attainment fails already for the one-dimensional constant-one target covector.

theorem helperForCorollary_20_0_3_covector_eq_zero_of_dim_zero (xStar : Fin 0 → ℝ) : xStar = 0

Helper for Corollary 20.0.3: in zero dimension, every covector is zero.

theorem helperForCorollary_20_0_3_universalAttainment_iff_dim_zero_of_empty_index {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) : (∀ (xStar : Fin n → ℝ), ∃ (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)) ↔ n = 0

Helper for Corollary 20.0.3: with an empty index family, universal attainment is equivalent to the ambient dimension being zero.

theorem helperForCorollary_20_0_3_refinement_and_universalAttainment_impossible_of_empty_index_of_dim_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hnZero : n ≠ 0) : ¬(((fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin 0, f i x) = infimalConvolutionFamily fun (i : Fin 0) => fenchelConjugate n (f i)) ∧ ∀ (xStar : Fin n → ℝ), ∃ (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.3: with an empty index family and nonzero dimension, the full refinement-plus-universal-attainment conclusion is impossible.

theorem helperForCorollary_20_0_3_exists_hypotheses_without_universalAttainment : ∃ (f : Fin 0 → (Fin 1 → ℝ) → EReal), (∀ (i : Fin 0), IsPolyhedralConvexFunction 1 (f i)) ∧ (∀ (i : Fin 0), ProperConvexFunctionOn Set.univ (f i)) ∧ (⋂ (i : Fin 0), effectiveDomain Set.univ (f i)).Nonempty ∧ ¬∀ (xStar : Fin 1 → ℝ), ∃ (xStarFamily : Fin 0 → Fin 1 → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily (fun (i : Fin 0) => fenchelConjugate 1 (f i)) xStar = ∑ i : Fin 0, fenchelConjugate 1 (f i) (xStarFamily i)

Helper for Corollary 20.0.3: there is explicit empty-index data satisfying all hypotheses while universal attainment fails in dimension one.

theorem helperForCorollary_20_0_3_not_imp_universalAttainment_in_empty_index_dim_one : ¬∀ (f : Fin 0 → (Fin 1 → ℝ) → EReal), (∀ (i : Fin 0), IsPolyhedralConvexFunction 1 (f i)) → (∀ (i : Fin 0), ProperConvexFunctionOn Set.univ (f i)) → (⋂ (i : Fin 0), effectiveDomain Set.univ (f i)).Nonempty → ∀ (xStar : Fin 1 → ℝ), ∃ (xStarFamily : Fin 0 → Fin 1 → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily (fun (i : Fin 0) => fenchelConjugate 1 (f i)) xStar = ∑ i : Fin 0, fenchelConjugate 1 (f i) (xStarFamily i)

Helper for Corollary 20.0.3: in the concrete branch m = 0, n = 1, the standard hypotheses do not imply universal split-attainment.

theorem helperForCorollary_20_0_3_not_imp_full_refinement_and_universalAttainment_in_empty_index_dim_one : ¬∀ (f : Fin 0 → (Fin 1 → ℝ) → EReal), (∀ (i : Fin 0), IsPolyhedralConvexFunction 1 (f i)) → (∀ (i : Fin 0), ProperConvexFunctionOn Set.univ (f i)) → (⋂ (i : Fin 0), effectiveDomain Set.univ (f i)).Nonempty → ((fenchelConjugate 1 fun (x : Fin 1 → ℝ) => ∑ i : Fin 0, f i x) = infimalConvolutionFamily fun (i : Fin 0) => fenchelConjugate 1 (f i)) ∧ ∀ (xStar : Fin 1 → ℝ), ∃ (xStarFamily : Fin 0 → Fin 1 → ℝ), ∑ i : Fin 0, xStarFamily i = xStar ∧ infimalConvolutionFamily (fun (i : Fin 0) => fenchelConjugate 1 (f i)) xStar = ∑ i : Fin 0, fenchelConjugate 1 (f i) (xStarFamily i)

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.

theorem helperForCorollary_20_0_3_not_forall_dimensions_refinement_and_universalAttainment : ¬∀ (n m : ℕ) (f : Fin m → (Fin n → ℝ) → EReal), (∀ (i : Fin m), IsPolyhedralConvexFunction n (f i)) → (∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) → (⋂ (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)) ∧ ∀ (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)

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.

theorem helperForCorollary_20_0_3_no_split_sum_for_unitCovector_of_empty_index : ¬∃ (xStarFamily : Fin 0 → Fin 1 → ℝ), ∑ i : Fin 0, xStarFamily i = fun (x : Fin 1) => 1

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.

theorem helperForCorollary_20_0_3_universalAttainment_impossible_under_hypotheses_of_empty_index_of_dim_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hnZero : n ≠ 0) (_hpoly : ∀ (i : Fin 0), IsPolyhedralConvexFunction n (f i)) (_hproper : ∀ (i : Fin 0), ProperConvexFunctionOn Set.univ (f i)) (_hdom : (⋂ (i : Fin 0), effectiveDomain Set.univ (f i)).Nonempty) : ¬∀ (xStar : Fin n → ℝ), ∃ (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.3: in the branch m = 0 and n ≠ 0, the standard polyhedral/proper/domain hypotheses still do not imply universal split-attainment.

theorem helperForCorollary_20_0_3_refinement_and_universalAttainment_impossible_under_hypotheses_of_empty_index_of_dim_ne_zero {n : ℕ} (f : Fin 0 → (Fin n → ℝ) → EReal) (hnZero : n ≠ 0) (_hpoly : ∀ (i : Fin 0), IsPolyhedralConvexFunction n (f i)) (_hproper : ∀ (i : Fin 0), ProperConvexFunctionOn Set.univ (f i)) (_hdom : (⋂ (i : Fin 0), effectiveDomain Set.univ (f i)).Nonempty) : ¬(((fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin 0, f i x) = infimalConvolutionFamily fun (i : Fin 0) => fenchelConjugate n (f i)) ∧ ∀ (xStar : Fin n → ℝ), ∃ (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.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.

theorem helperForCorollary_20_0_3_attainment_for_each_xStar_of_pos_m {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)

Helper for Corollary 20.0.3: when 0 < m, each covector admits an attaining split for the infimal convolution of conjugates.

theorem helperForCorollary_20_0_3_refinement_and_attainment_of_pos_m {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) : ((fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x) = infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) ∧ ∀ (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)

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.

theorem polyhedral_refinement_fenchelConjugate_sum_eq_infimalConvolutionFamily_and_attainment {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) : ((fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x) = infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) ∧ ∀ (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.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.