From ece1e1c2d8a84820d5436a1a7d337d779eefefac Mon Sep 17 00:00:00 2001
From: Shane Zarechian <shanezarechian@gmail.com>
Date: Tue, 2 Dec 2025 12:22:18 -0500
Subject: [PATCH] Add VaR_monotone_in_alpha skeleton

---
 Probability/MDP/Risk.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index e50ef37..a831b6b 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -84,4 +84,13 @@ notation "CVaR[" α "," X "//" P "]" => CVaR P X α
 -- CVaR ≥ VaR: CVaR[α, X // P] ≥ VaR[α, X // P]
 
 
+
+theorem VaR_monotone_in_alpha
+  (P : Findist n) (X : FinRV n ℚ)
+  {α₁ α₂ : ℚ} (h0 : 0 ≤ α₁) (h12 : α₁ ≤ α₂) (h1 : α₂ ≤ 1) : VaR P X α₁ ≤ VaR P X α₂ :=
+  by
+    simp [VaR]
+    sorry
+
+
 end Risk