small VaR-related comments

Author: marekpetrik

Probability/MDP/Risk.lean

@@ -13,7 +13,6 @@ def rangeOfRV (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
 
 /-- Value-at-Risk of X at level α: VaR_α(X) = min { t ∈ X(Ω) | P[X ≤ t] ≥ α }.
 If we assume 0 ≤ α ∧ α ≤ 1, then the "else 0" branch is never used. -/
-
 def VaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
   let S : Finset ℚ := (rangeOfRV X).filter (fun t => cdf P X t ≥ α)
   if h : S.Nonempty then
@@ -22,6 +21,9 @@ def VaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
     0
 
 notation "VaR[" α "," X "//" P "]" => VaR P X α
+-- TODO (Marek): What do you think about : 
+-- notation "VaR[ X "//" P "," α "]" => VaR P X α
+-- I think that the α goes better with the probability that the variable
 
 theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
   (hXY : ∀ ω, X ω ≤ Y ω) : VaR P X α ≤ VaR P Y α := by
@@ -66,6 +68,10 @@ def CVaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
   else
      num / den
 
+-- NOTE (Marek): The CVaR, as defined above is not convex/concave. 
+-- See Page 14 at https://www.cs.unh.edu/~mpetrik/pub/tutorials/risk2/dlrl2023.pdf
+-- NOTE (Marek): The CVaR above is defined for costs and not rewards 
+
 notation "CVaR[" α "," X "//" P "]" => CVaR P X α
 
 --TODO: prove...
@@ -75,4 +81,5 @@ notation "CVaR[" α "," X "//" P "]" => CVaR P X α
 -- convexity
 -- CVaR ≥ VaR: CVaR[α, X // P] ≥ VaR[α, X // P]
 
+
 end Risk