theorem closure_posHomogeneousGenerated_infimum_rightScalarMultiple {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} (hfclosed : ClosedConvexFunction f) (hfproper : ProperConvexFunctionOn Set.univ f) (hf0 : f 0 > 0) (hrec : (epigraph Set.univ f).recessionCone = epigraph Set.univ f0_plus) : have k := positivelyHomogeneousConvexFunctionGenerated f; ProperConvexFunctionOn Set.univ k ∧ (∀ (x : Fin n → ℝ), convexFunctionClosure k x = sInf (Set.insert (f0_plus x) {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple f lam x})) ∧ (∀ (x : Fin n → ℝ), ∃ z ∈ Set.insert (f0_plus x) {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple f lam x}, convexFunctionClosure k x = z) ∧ (0 ∈ effectiveDomain Set.univ f → ClosedConvexFunction k ∧ ∀ (x : Fin n → ℝ), k x = sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple f lam x})

Theorem 9.7. Let f be a closed proper convex function on ℝ^n with f(0) > 0, and let k be the positively homogeneous convex function generated by f. Then k is proper and (convexFunctionClosure k)(x) is the infimum of (f λ)(x) over λ > 0 together with λ = 0^+ (encoded here as f0_plus), the infimum being attained for each x. If 0 ∈ dom f, then k is closed and the λ = 0^+ term can be omitted (but the infimum might not be attained).