The worst total is positively homogeneous
ProvedCoherentRisk.worstTotal_homogeneousoperations-researchprobability
Scaling a position by a nonnegative factor scales its worst-total loss by the same factor. A nonnegative factor multiplies every competitor's total without reordering them, so it passes through the maximum. Nonnegativity is essential: a negative factor would reverse the order and turn the maximum into a minimum.
As throughout CoherentRisk, the development counts states and refers to no probability measure, so no confidence level is attached to .
Preamble
import Definitions.Def_ExpectedShortfall open CoherentRisk
Formal statement
namespace CoherentRisk
theorem worstTotal_homogeneous {n : ℕ} (m : Fin (n+1)) (lam : ℝ) (hlam : 0 ≤ lam)
(X : Fin (n+1) → ℝ) :
worstTotal (fun i => lam * X i) m = lam * worstTotal X m := by
sorry
end CoherentRiskSource
C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking and Finance 26 (2002) 1487-1503, Section 3; P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228, Definition 2.4