A convex normalized function is positively superhomogeneous (star-shaped)
ProvedStarShapedRisk.Representation.convex_normalized_superhomogeneousA convex real function with f(0) = 0 is positively superhomogeneous: for every t > 1 and every X, f(tX) >= t f(X). Proof: X = (1/t)(tX) + (1-1/t)0, so convexity and f(0)=0 give f(X) <= (1/t) f(tX). This is the elementary step in Castagnoli et al. (2022) showing every convex risk measure is star-shaped (used in Theorem 2's (ii)=>(i) direction).
Preamble
import Mathlib
Formal statement
namespace StarShapedRisk.Representation
/-- Castagnoli et al. (2022), used in the proof of Theorem 2 (p. 2644): a convex
function with `f 0 = 0` is positively superhomogeneous ("star-shaped"): for
`t > 1`, `t * f X ≤ f (t • X)`. Proof: `X = (1/t) • (t • X) +
(1 - 1/t) • 0`, so convexity and `f 0 = 0` give
`f X ≤ (1/t) * f (t • X)`. This is the step showing every convex
risk measure is star-shaped, feeding Theorem 2's `(ii) ⇒ (i)` via
Theorem 1's infimum case. -/
theorem convex_normalized_superhomogeneous {E : Type*} [AddCommGroup E] [Module ℝ E]
(f : E → ℝ) (hconv : ConvexOn ℝ Set.univ f) (h0 : f 0 = 0)
{t : ℝ} (ht : 1 < t) (X : E) :
t * f X ≤ f (t • X) := by
sorry
end StarShapedRisk.Representation