cvar_inf_form

SAA CVaR inf-form — the discrete Rockafellar–Uryasev auxiliary form (obligations A1 + A5)

Seal

Rung risk-A1 (the first Lean stone of the risk layer; risk-aware planning proof-obligations map rows A1/A5, also serving B3 by reuse) · Status sealed — all three public theorems axiom-clean (#print axioms verbatim in 6. The machine seal), no sorryAx, no interface hypothesis anywhere. This module is self-contained: it imports only Mathlib, discharges nothing from the ledger, and is the substrate the risk-aware CVaR obligations rest on. Links: consumes only Mathlib convex-analysis + Finset sums · source rockafellar2002conditional (the atomic-case provenance) · rockafellar2000optimization (the inf-form origin) · artzner1999coherent (coherence context) · SymPy pin (/Code/tasks/streams/ctrllib/scratch/pin_cvar_saa.py) · obligations map (/Code/tasks/streams/risk_aware_planning/proof_obligations_risk_phases.md) rows A1/A5, §7 item 2.

What this seals, in one paragraph

A scenario-based risk-aware planner never sees a continuous loss distribution — it sees a finite set of simulated losses $Z_1,\dots ,Z_q$, an empirical distribution that is a step function with probability atoms by construction. Rockafellar–Uryasev give the tractable form of Conditional Value-at-Risk for exactly this case: CVaR is the minimum over one auxiliary scalar $\tau$ of a piecewise-linear convex objective (RU-2000 Thm 1 / RU-2002 Thm 10, sampled form eq. 9 / Thm 16). This module formalizes that discrete inf-form for equal weights $p_k=1/q$ and seals its two load-bearing structural facts — convexity of the objective, and that its minimum over $\tau \in \mathbb{R}$ is attained at a sample point (the piecewise-linear-minimizer characterization, RU-2002 Prop. 8’s VaR breakpoint) — hence the defined CVaR equals the objective evaluated at that sample. The module is (~/Code/vault/lean/CvarInfForm.lean), build copy ~/lean/ctrllib/Ctrllib/CvarInfForm.lean.

⚠ Route deviation — read this first

Route chosen: definition-first (the sanctioned honest fallback), not full equality with a from-first-principles CVaR. Recorded loudly per the house provenance rule.

• Declined (equality route): define CVaR independently as the sorted $\alpha$-tail average (RU-2002 Prop. 8, eq. 25) and prove the inf-form equals it. This needs order statistics — a sort of the sample vector and the index $k_{\alpha }$ — which is real formalization work (a permutation-sorting layer) with little added defense value over what is sealed here. Deferred; it is pinned numerically instead (see 5. The atom subtlety, in plain words).
• Sealed (definition-first route): cvarSAA α Z is defined by the inf-form, ⨅_τ cvarObj α Z τ (RU-2000 Thm 1 / RU-2002 Thm 10 — this is the paper’s operative definition, not a shortcut). We then seal, from that definition, convexity + attainment-at-a-sample + the closed-form value $\text{CVaR}=\text{cvarObj}(\text{VaR})$ (the RU-2002 Prop. 8 shape: CVaR is the objective at a sample breakpoint).
• Why this is honest and sufficient. The two facts a risk-aware planner actually consumes are (i) the objective is convex, so the sampled CVaR constraint is an LP / SOCP-friendly convex program (RU-2000’s whole point), and (ii) the minimizer is a sample, so the CVaR value and the VaR are read off a finite set — both sealed. The sorted closed form is a convenience re-expression of (ii), not an independent obligation.

1. The statement and its objects

Notation follows rockafellar2002conditional (⚠ the 2002 paper’s convention, which swaps the 2000 paper’s letters): $\alpha \in [0,1)$ is the confidence level, $\tau$ is the auxiliary minimization variable. For samples $Z:\text{Fin }q\to \mathbb{R}$ (equal weights $p_k=1/q$), the SAA objective is

$\text{cvarObj}\alpha Z\tau =\tau +\frac{1}{q(1-\alpha )}{\sum }_k(Z_k-\tau {)}^{+},(Z_k-\tau {)}^{+}:=\max (Z_k-\tau ,0)$

(RU-2000 eq. 9 ${\tilde{F}}_{\beta }$; RU-2002 Thm 16, with $\beta \to \alpha$). CVaR is defined by the inf-form

$\text{cvarSAA}\alpha Z={\inf }_{\tau \in \mathbb{R}}\text{cvarObj}\alpha Z\tau \text{(RU-2000 Thm 1 / RU-2002 Thm 10, eq. 28).}$

Atom-safety is built in. Every theorem below is stated for an arbitrary $Z:\text{Fin }q\to \mathbb{R}$ — no distinctness / no-tie hypothesis. So a probability mass sitting exactly at the VaR quantile (obligation A5, the visibility-flip case) is handled by construction; the inf-form never forms the ambiguous conditional expectation that the naive tail averages do.

2. Theorem 1 — convexity (cvarObj_convexOn, sealed)

$0<q,\alpha <1\Rightarrow \text{ConvexOn}\mathbb{R}\text{univ}(\text{cvarObj}\alpha Z)$

Proof. Each summand $\tau \mapsto \max (Z_k-\tau ,0)$ is the pointwise supremum of the affine function $\tau \mapsto Z_k-\tau$ (convex: a convex constant minus a concave identity, convexOn_const.sub concaveOn_id) and the constant $0$, hence convex (ConvexOn.sup). A finite sum of convex functions is convex (Finset.sum_induction over ConvexOn.add, base convexOn_const 0). The weight $\frac{1}{q(1-\alpha )}\ge 0$ (needs $q>0$, $\alpha <1$), so scaling preserves convexity (ConvexOn.smul); adding the identity $\tau \mapsto \tau$ (convexOn_id) gives the objective. $■$

This is the RU-2000 Thm 1 convexity — the property that turns a sampled CVaR bound into a convex program (an LP after the standard epigraph split).

3. Theorem 2 — the minimizer is a sample (cvarObj_min_at_sample, sealed)

$0<q,0\le \alpha <1\Rightarrow \exists k,\forall \tau ,\text{cvarObj}\alpha Z(Z_k)\le \text{cvarObj}\alpha Z\tau$

The global minimum over all $\tau \in \mathbb{R}$ is attained at one of the samples — the piecewise-linear-minimizer characterization (RU-2002 Prop. 8: the argmin’s lower endpoint is $z_{k_{\alpha }}=\text{VaR}$).

Proof. The engine is a separating-sample slope identity (cvarObj_diff_sep, private): if a value $w$ separates the samples $\le \tau$ from those $>\tau$ (i.e. $Z_j\le \tau \Rightarrow Z_j\le w$ and $\tau <Z_j\Rightarrow w\le Z_j$), then

$\text{cvarObj}\alpha Zw-\text{cvarObj}\alpha Z\tau =(w-\tau )(1-\frac{1}{q(1-\alpha )}|\{k:\tau <Z_k\}\left|\right).$

This is the affine-between-breakpoints fact: on the segment reaching $w$ the objective is affine with slope $1-\frac{1}{q(1-\alpha )}|\{k:\tau <Z_k\}|$. It is proved by splitting the sum ${\sum }_k[(Z_k-w{)}^{+}-(Z_k-\tau {)}^{+}]$ over $\{k:\tau <Z_k\}$ and its complement — each above-$\tau$ term collapses to $\tau -w$, each at-or-below term to $0$ — with no tie hypothesis — the statement holds for distributions with atoms, the general-loss setting of rockafellar2002conditional.

Then a two-case per-point lemma: for every $\tau$ some sample dominates it.

• If $\frac{1}{q(1-\alpha )}|\{k:\tau <Z_k\}|\ge 1$ (right slope $\le 0$), the smallest sample strictly above $\tau$ (via Finset.exists_min_image) is a separating $w>\tau$ with slope factor $\le 0$, so $\text{cvarObj}(w)\le \text{cvarObj}(\tau )$.
• Otherwise (right slope $>0$), the set $\{k:Z_k\le \tau \}$ is nonempty — else all $q$ samples exceed $\tau$ and $\frac{1}{q(1-\alpha )}\cdot q=\frac{1}{1-\alpha }\ge 1$ (uses $0\le \alpha$), contradiction — and its largest sample (via Finset.exists_max_image) is a separating $w\le \tau$ with slope factor $\ge 0$, again $\text{cvarObj}(w)\le \text{cvarObj}(\tau )$.

Finally, the finite argmin over the samples (Finset.exists_min_image on univ, nonempty since $q>0$) dominates every $\tau$ through the per-point lemma. $■$

4. Theorem 3 — the inf is attained at a sample (cvarSAA_eq_obj_sample, sealed)

$0<q,0\le \alpha <1\Rightarrow \exists k,\text{cvarSAA}\alpha Z=\text{cvarObj}\alpha Z(Z_k)$

Proof. Theorem 2 gives a sample $Z_k$ with $\text{cvarObj}(Z_k)\le \text{cvarObj}(\tau )$ for all $\tau$, so $\text{cvarObj}(Z_k)$ is a lower bound of the range (BddBelow) and is achieved at $\tau =Z_k$. Antisymmetry of ciInf_le (inf $\le$ value) and le_ciInf (value $\le$ inf) closes it. $■$

This is the RU-2002 Prop. 8 shape: the CVaR value is the objective evaluated at the VaR breakpoint $Z_k$ — a finite, computable expression, no continuum infimum left.

5. The atom subtlety, in plain words

When the loss distribution has a probability mass exactly at the VaR quantile — obligation A5’s “visibility flip”, where invalid views deposit a mass at the failure loss $-r_{\text{fail}}$ — the phrase “expected loss beyond VaR” is genuinely ambiguous: three different numbers (VaR itself, the mean at-or-above VaR = ${\text{CVaR}}^{-}$, the mean strictly above = ${\text{CVaR}}^{+}$) can all differ (rockafellar2002conditional Intro, eq. 17). RU-2002 resolves it by splitting the atom (Def. 3): the single well-defined CVaR is a weighted average of VaR and ${\text{CVaR}}^{+}$, the weight being the fraction of the VaR-level atom folded into the tail (Prop. 6, eq. 21). The inf-form sealed here splits the atom automatically — it never forms a conditional expectation, so it needs no atom bookkeeping at all; that is precisely why Theorems 1–3 carry no distinctness hypothesis.

The SymPy pin (~/Code/tasks/streams/ctrllib/scratch/pin_cvar_saa.py) exhibits this in exact rationals on the atom case $Z=[1,2,3,3,10]$, $\alpha =3/5$ (a mass of $2$ at the value $3=\text{VaR}$):

quantity	value	note
inf-form min $=$ RU-2002 Prop. 8 (eq. 25)	$13/2=6.5$	attained at $\tau =\text{VaR}=3$ — the correct CVaR
naive ${\text{CVaR}}^{-}=\mathbb{E}[Z\mid Z\ge \text{VaR}]$	$16/3\approx 5.33$	too low — under-counts tail risk
naive ${\text{CVaR}}^{+}=\mathbb{E}[Z\mid Z>\text{VaR}]$	$10$	too high

The naive averages straddle the truth (${\text{CVaR}}^{-}\le \text{CVaR}\le {\text{CVaR}}^{+}$, verified); only the inf-form lands on the RU-2002 value. The pin also confirms, on distinct-sample cases, that the inf-form equals the Prop. 8 closed form exactly and that the argmin is the VaR order-statistic $z_{k_{\alpha }}$, and includes the Corollary 9 worst-case collapse ($\alpha$ inside the top scenario’s mass $\Rightarrow$ CVaR $=$ max loss).

What is sealed vs defined (for the defense)

• Defined: $\text{cvarSAA}:={\inf }_{\tau }\text{cvarObj}$ — the RU inf-form is the operative definition (RU-2000 Thm 1 / RU-2002 Thm 10). No independent sorted-tail-average CVaR is formalized; that equality is deferred and covered numerically (§5).
• Sealed (kernel-checked, axiom-clean): convexity (T1), attainment-at-a-sample / piecewise-linear minimizer (T2), and the attained closed-form value $\text{CVaR}=\text{cvarObj}(\text{VaR})$ (T3). Atom-safety is structural — no theorem assumes distinct samples.

6. The machine seal

Single-file elaboration (lake env lean, no sorry, no interface hypotheses); axiom prints verbatim:

'Ctrllib.cvarObj_convexOn' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.cvarObj_min_at_sample' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.cvarSAA_eq_obj_sample' depends on axioms: [propext, Classical.choice, Quot.sound]

All within {propext, Classical.choice, Quot.sound} — no sorryAx. interfaces_assumed: [], interfaces_discharged: []: a fresh foundational stone for the risk layer.