theorem recessionCone_epigraph_sum_block {n m : ℕ} {f f0_plus : Fin m → (Fin n → ℝ) → EReal} (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) (hnotbot0 : ∀ (i : Fin m) (x : Fin n → ℝ), f0_plus i x ≠ ⊥) (hconv_i : ∀ (i : Fin m), Convex ℝ (epigraph Set.univ (f i))) (hrec_i : ∀ (i : Fin m), (epigraph Set.univ (f i)).recessionCone = epigraph Set.univ (f0_plus i)) : have e := blockEquivFun; have h := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i (e x i); have h0_plus := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f0_plus i (e x i); (epigraph Set.univ h).recessionCone = epigraph Set.univ h0_plus

The recession cone of the block-sum epigraph is the epigraph of the block-sum recession.

theorem h0_plus_sum_posHom_proper {n m : ℕ} {f0_plus : Fin m → (Fin n → ℝ) → EReal} (hpos_i : ∀ (i : Fin m), PositivelyHomogeneous (f0_plus i)) (hproper_i : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f0_plus i)) : have e := blockEquivFun; have h0_plus := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f0_plus i (e x i); PositivelyHomogeneous h0_plus ∧ ProperConvexFunctionOn Set.univ h0_plus

The block-sum h0_plus is positively homogeneous and proper under componentwise assumptions.

theorem attainment_top_case_infimalConvolutionFamily {n m : ℕ} (hm : 0 < m) {f : Fin m → (Fin n → ℝ) → EReal} : have fInf := infimalConvolutionFamily f; ∀ (x : Fin n → ℝ), fInf x = ⊤ → ∃ (x' : Fin m → Fin n → ℝ), ∑ i : Fin m, x' i = x ∧ fInf x = ∑ i : Fin m, f i (x' i)

Attainment in the ⊤ case for infimal convolution families when m > 0.

theorem infimalConvolutionFamily_closed_proper_convex_recession {n m : ℕ} {f f0_plus : Fin m → (Fin n → ℝ) → EReal} (hclosed : ∀ (i : Fin m), ClosedConvexFunction (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hrec_i : ∀ (i : Fin m), (epigraph Set.univ (f i)).recessionCone = epigraph Set.univ (f0_plus i)) (hpos_i : ∀ (i : Fin m), PositivelyHomogeneous (f0_plus i)) (hproper0_i : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f0_plus i)) (hzero : ∀ (z : Fin m → Fin n → ℝ), ∑ i : Fin m, f0_plus i (z i) ≤ 0 → ∑ i : Fin m, f0_plus i (-z i) > 0 → ∑ i : Fin m, z i ≠ 0) (hm : 0 < m) : have fInf := infimalConvolutionFamily f; have fInf0_plus := infimalConvolutionFamily f0_plus; ClosedConvexFunction fInf ∧ ProperConvexFunctionOn Set.univ fInf ∧ (∀ (x : Fin n → ℝ), ∃ (x' : Fin m → Fin n → ℝ), ∑ i : Fin m, x' i = x ∧ fInf x = ∑ i : Fin m, f i (x' i)) ∧ fInf0_plus = infimalConvolutionFamily f0_plus

Corollary 9.2.1. Let f₁, …, fₘ be closed proper convex functions on ℝ^n. Assume that z₁ + … + zₘ ≠ 0 for every choice of vectors z₁, …, zₘ such that (f₁ 0+)(z₁) + … + (fₘ 0+)(zₘ) ≤ 0 and (f₁ 0+)(-z₁) + … + (fₘ 0+)(-zₘ) > 0. Then the infimal convolute f₁ □ … □ fₘ is a closed proper convex function on ℝ^n, and the infimum in the definition of (f₁ □ … □ fₘ)(x) is attained for each x. Moreover, (f₁ □ … □ fₘ)0+ = f₁ 0+ □ … □ fₘ 0+.