theorem recessionFunction_properties {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} {f0_plus : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn C fun (x : Fin n → ℝ) => ↑(f x)) (hC : C = Set.univ) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) : PositivelyHomogeneous f0_plus ∧ ProperConvexFunctionOn Set.univ f0_plus ∧ (∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ C, r = ↑(f (x + y) - f x)}) ∧ ((ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f x)) → ClosedConvexFunction f0_plus ∧ ∀ x ∈ C, ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ (t : ℝ), 0 < t ∧ r = ↑((f (x + t • y) - f x) / t)} ∧ Filter.Tendsto (fun (t : ℝ) => ↑((f (x + t • y) - f x) / t)) Filter.atTop (nhds (f0_plus y)))

Theorem 8.5. Let f be a proper convex function. The recession function f0^+ of f is a positively homogeneous proper convex function. For every vector y, one has (f0^+)(y) = sup { f(x + y) - f(x) | x ∈ dom f }. If f is closed, f0^+ is closed too, and for any x ∈ dom f, (f0^+)(y) = sup_{λ > 0} (f(x + λ y) - f(x)) / λ = lim_{λ → ∞} (f(x + λ y) - f(x)) / λ.