From 9e6882afda4de9fa450a37d3f3b9bacc983d3eb7 Mon Sep 17 00:00:00 2001
From: Emily Chandran <emily.chandran@unh.edu>
Date: Fri, 28 Nov 2025 12:14:10 -0500
Subject: [PATCH 01/16] proved cdf monotonicity

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

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index a36fe3f..0481c16 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -8,6 +8,23 @@ variable {n : ℕ}
 
 def cdf (P : Findist n) (X : FinRV n ℚ) (t : ℚ) : ℚ := ℙ[X ≤ᵣ t // P]
 
+theorem cdf_monotone (P : Findist n) (X : FinRV n ℚ) (t1 t2 : ℚ)
+  (ht : t1 ≤ t2) : cdf P X t1 ≤ cdf P X t2 := by
+  simp [cdf]
+  apply exp_monotone
+  intro ω
+  by_cases h1 : X ω ≤ t1
+  · have h2 : X ω ≤ t2 := le_trans h1 ht
+    simp [FinRV.leq, 𝕀, indicator, h1, h2]
+  · simp [𝕀, indicator, FinRV.leq, h1]
+    by_cases h2 : X ω ≤ t2
+    · simp [h2]
+    · simp [h2] ---these lines seem really unnecessary but idk how to fix it
+
+
+
+
+
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
 def rangeOfRV (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
 
@@ -19,7 +36,7 @@ def VaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
   if h : S.Nonempty then
     S.min' h
   else
-    0
+    0 --this is illegal i know -- Keith can fix it :)
 
 notation "VaR[" α "," X "//" P "]" => VaR P X α
 

From 70fc210d9bb13a16f2bacc91059d02483f95318d Mon Sep 17 00:00:00 2001
From: Emily Chandran <emily.chandran@unh.edu>
Date: Mon, 1 Dec 2025 16:29:50 -0500
Subject: [PATCH 02/16] changed var notation

---
 Probability/MDP/Risk.lean | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 564d0d1..3180bc7 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -37,10 +37,7 @@ def VaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
   else
     0 --this is illegal i know -- Keith can fix it :)
 
-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
+notation "VaR[" X "//" P ", " α "]" => VaR P X α
 
 theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
   (hXY : ∀ ω, X ω ≤ Y ω) : VaR P X α ≤ VaR P Y α := by
@@ -74,7 +71,7 @@ def tailInd (X : FinRV n ℚ) (t : ℚ) : FinRV n ℚ :=
   fun ω => if X ω > t then 1 else 0
 
 /-- Conditional Value-at-Risk (CVaR) of X at level α under P.
-CVaR =  E[X * I[X > VaR] ] / P[X > VaR]
+CVaR_α(X) =  E[X * I[X > VaR] ] / P[X > VaR]
 If the tail probability is zero, CVaR is defined to be 0.
 -/
 def CVaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
@@ -87,11 +84,11 @@ def CVaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
   else
      num / den
 
--- NOTE (Marek): The CVaR, as defined above is not convex/concave. 
+-- 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 
+-- NOTE (Marek): The CVaR above is defined for costs and not rewards
 
-notation "CVaR[" α "," X "//" P "]" => CVaR P X α
+notation "CVaR[" X "//" P ", " α "]" => CVaR P X α
 
 --TODO: prove...
 -- monotonicity: (∀ ω, X ω ≤ Y ω) → CVaR[α, X // P] ≤ CVaR[α, Y // P]

From 73d0884d65493500e43c429410d2861c4a726f5d Mon Sep 17 00:00:00 2001
From: Emily Chandran <emily.chandran@unh.edu>
Date: Wed, 3 Dec 2025 12:22:07 -0500
Subject: [PATCH 03/16] current work on var monotone

---
 Probability/MDP/Risk.lean | 64 +++++++++++++++++++++++++--------------
 1 file changed, 41 insertions(+), 23 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 3180bc7..349966a 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -22,9 +22,6 @@ theorem cdf_monotone (P : Findist n) (X : FinRV n ℚ) (t1 t2 : ℚ)
     · simp [h2] ---these lines seem really unnecessary but idk how to fix it
 
 
-
-
-
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
 def rangeOfRV (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
 
@@ -39,31 +36,52 @@ def VaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
 
 notation "VaR[" X "//" P ", " α "]" => VaR P X α
 
-theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
-  (hXY : ∀ ω, X ω ≤ Y ω) : VaR P X α ≤ VaR P Y α := by
-  have hcdf : ∀ t : ℚ, cdf P Y t ≤ cdf P X t := by
-    intro t
-    simp [cdf]
-    apply exp_monotone
-    intro ω
-    have h1 : Y ω ≤ t → X ω ≤ t := by
-      intro hY
-      exact le_trans (hXY ω) hY
-    by_cases hY : Y ω ≤ t
-    · have hX : X ω ≤ t := by exact h1 hY
-      simp [𝕀, indicator, FinRV.leq, hY, hX]
-    · simp [𝕀, indicator, FinRV.leq, hY]
-      by_cases hx2 : X ω ≤ t
-      · simp [hx2]
-      · simp [hx2] ---these lines seem really unnecessary but idk how to fix it
+--(Emily) I am now thinking of just trying to keep it in Q
+--so I wouln't use anything between these lines!
+------------------- defined over the reals to prove monotonicity ---------------------------
+noncomputable def cdfR (P : Findist n) (X : FinRV n ℝ) (t : ℝ) : ℝ := ℙ[X ≤ᵣ t // P]
+
+theorem cdfR_monotone (P : Findist n) (X : FinRV n ℝ) (t1 t2 : ℝ)
+  (ht : t1 ≤ t2) : cdfR P X t1 ≤ cdfR P X t2 := by
+  simp [cdfR]
+  apply exp_monotone
+  intro ω
+  by_cases h1 : X ω ≤ t1
+  · have h2 : X ω ≤ t2 := le_trans h1 ht
+    simp [FinRV.leq, 𝕀, indicator, h1, h2]
+  · simp [𝕀, indicator, FinRV.leq, h1]
+    by_cases h2 : X ω ≤ t2
+    · simp [h2]
+    · simp [h2]
 
+/-- Value-at-Risk of X at level α: VaR_α(X) = inf {t:ℝ | P[X ≤ t] ≥ α } -/
+noncomputable def VaR_R (P : Findist n) (X : FinRV n ℝ) (α : ℝ) : ℝ :=
+  sInf { t : ℝ | cdfR P X t ≥ α }
+
+theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℝ) (α : ℝ)
+  (hXY : ∀ ω, X ω ≤ Y ω) : VaR_R P X α ≤ VaR_R P Y α := by
+  let Sx : Set ℝ := { t : ℝ | cdfR P X t ≥ α }
+  let Sy : Set ℝ := { t : ℝ | cdfR P Y t ≥ α }
+  have hx : VaR_R P X α = sInf Sx := rfl
+  have hy : VaR_R P Y α = sInf Sy := rfl
+  have hsubset : Sy ⊆ Sx := by
+    unfold Sy Sx
+    intro t ht
+    have h_cdf : ∀ t, cdfR P X t ≥ cdfR P Y t := by
+      intro t
+
+      sorry
+    sorry
+  rw [hx, hy]
   sorry
 
+-------------------------------------------------------------------
+
 theorem VaR_translation_invariant (P : Findist n) (X : FinRV n ℚ) (α c : ℚ) :
-  VaR P (fun ω => X ω + c) α = VaR P X α + c := sorry
+  VaR_Q P (fun ω => X ω + c) α = VaR_Q P X α + c := sorry
 
 theorem VaR_positive_homog (P : Findist n) (X : FinRV n ℚ) (α c : ℚ)
-  (hc : c > 0) : VaR P (fun ω => c * X ω) α = c * VaR P X α := sorry
+  (hc : c > 0) : VaR_Q P (fun ω => c * X ω) α = c * VaR_Q P X α := sorry
 
 
 /-- Tail indicator: 1 if X(ω) > t, else 0. -/
@@ -75,7 +93,7 @@ CVaR_α(X) =  E[X * I[X > VaR] ] / P[X > VaR]
 If the tail probability is zero, CVaR is defined to be 0.
 -/
 def CVaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
-  let v := VaR P X α
+  let v := VaR_Q P X α
   let B : FinRV n ℚ := tailInd X v
   let num := 𝔼[X * B // P]
   let den := ℙ[X >ᵣ v // P]

From 2828564eb533a5d8ff2efacf80ae38ce9ea059ef Mon Sep 17 00:00:00 2001
From: Emily Chandran <emily.chandran@unh.edu>
Date: Thu, 4 Dec 2025 10:20:02 -0500
Subject: [PATCH 04/16] fixed small errors

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

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 349966a..c9250f6 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -78,10 +78,10 @@ theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℝ) (α : ℝ)
 -------------------------------------------------------------------
 
 theorem VaR_translation_invariant (P : Findist n) (X : FinRV n ℚ) (α c : ℚ) :
-  VaR_Q P (fun ω => X ω + c) α = VaR_Q P X α + c := sorry
+  VaR P (fun ω => X ω + c) α = VaR P X α + c := sorry
 
 theorem VaR_positive_homog (P : Findist n) (X : FinRV n ℚ) (α c : ℚ)
-  (hc : c > 0) : VaR_Q P (fun ω => c * X ω) α = c * VaR_Q P X α := sorry
+  (hc : c > 0) : VaR P (fun ω => c * X ω) α = c * VaR P X α := sorry
 
 
 /-- Tail indicator: 1 if X(ω) > t, else 0. -/
@@ -93,7 +93,7 @@ CVaR_α(X) =  E[X * I[X > VaR] ] / P[X > VaR]
 If the tail probability is zero, CVaR is defined to be 0.
 -/
 def CVaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
-  let v := VaR_Q P X α
+  let v := VaR P X α
   let B : FinRV n ℚ := tailInd X v
   let num := 𝔼[X * B // P]
   let den := ℙ[X >ᵣ v // P]

From eee99a9c0a23b90e0f0410df7abc3d6d40bfae34 Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Fri, 5 Dec 2025 10:18:05 -0500
Subject: [PATCH 05/16] small tweak

---
 Probability/MDP/Risk.lean          | 8 +++-----
 Probability/Probability/Basic.lean | 3 ++-
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index c9250f6..10a3c7c 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -10,7 +10,7 @@ def cdf (P : Findist n) (X : FinRV n ℚ) (t : ℚ) : ℚ := ℙ[X ≤ᵣ t // P
 
 theorem cdf_monotone (P : Findist n) (X : FinRV n ℚ) (t1 t2 : ℚ)
   (ht : t1 ≤ t2) : cdf P X t1 ≤ cdf P X t2 := by
-  simp [cdf]
+  unfold cdf
   apply exp_monotone
   intro ω
   by_cases h1 : X ω ≤ t1
@@ -18,8 +18,7 @@ theorem cdf_monotone (P : Findist n) (X : FinRV n ℚ) (t1 t2 : ℚ)
     simp [FinRV.leq, 𝕀, indicator, h1, h2]
   · simp [𝕀, indicator, FinRV.leq, h1]
     by_cases h2 : X ω ≤ t2
-    · simp [h2]
-    · simp [h2] ---these lines seem really unnecessary but idk how to fix it
+    repeat simp [h2]
 
 
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
@@ -51,8 +50,7 @@ theorem cdfR_monotone (P : Findist n) (X : FinRV n ℝ) (t1 t2 : ℝ)
     simp [FinRV.leq, 𝕀, indicator, h1, h2]
   · simp [𝕀, indicator, FinRV.leq, h1]
     by_cases h2 : X ω ≤ t2
-    · simp [h2]
-    · simp [h2]
+    repeat simp [h2]
 
 /-- Value-at-Risk of X at level α: VaR_α(X) = inf {t:ℝ | P[X ≤ t] ≥ α } -/
 noncomputable def VaR_R (P : Findist n) (X : FinRV n ℝ) (α : ℝ) : ℝ :=
diff --git a/Probability/Probability/Basic.lean b/Probability/Probability/Basic.lean
index 62ed81e..751b013 100644
--- a/Probability/Probability/Basic.lean
+++ b/Probability/Probability/Basic.lean
@@ -34,7 +34,7 @@ end Findist
 
 ------------------------------ Probability ---------------------------
 
-variable {n : ℕ} {P : Findist n} {B C : FinRV n Bool}
+variable {n : ℕ} {P : Findist n} {A B C : FinRV n Bool}
 
 theorem prob_compl_sums_to_one : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 := 
     by rw [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_dists_add, one_of_ind_bool_or_not]
@@ -44,6 +44,7 @@ theorem prob_compl_one_minus : ℙ[¬ᵣB // P] = 1 - ℙ[B // P] :=
     by rw [←prob_compl_sums_to_one (P:=P) (B:=B)]; ring 
 
 
+
 ------------------------------ Expectation ---------------------------
 
 section Expectation 

From 6ebc6e32b05c068f755a08d60b0798db94c6e63c Mon Sep 17 00:00:00 2001
From: Emily Chandran <emily.chandran@unh.edu>
Date: Fri, 5 Dec 2025 10:32:15 -0500
Subject: [PATCH 06/16] cdf monotonicity x y

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

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index c9250f6..5eb5f72 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -21,6 +21,20 @@ theorem cdf_monotone (P : Findist n) (X : FinRV n ℚ) (t1 t2 : ℚ)
     · simp [h2]
     · simp [h2] ---these lines seem really unnecessary but idk how to fix it
 
+theorem cdf_monotone_xy (P : Findist n) (X Y : FinRV n ℚ) (t : ℚ)
+  (h : X ≤ Y) : cdf P X t ≥ cdf P Y t := by
+  simp [cdf]
+  apply exp_monotone
+  intro ω
+  have h2 := h ω
+  by_cases h1 : Y ω ≤ t
+  · have h3 : X ω ≤ t := le_trans h2 h1
+    simp [FinRV.leq, 𝕀, indicator, h3, h1]
+  · simp [𝕀, indicator, FinRV.leq, h1]
+    by_cases h4 : X ω ≤ t
+    · simp [h4]
+    · simp [h4]
+
 
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
 def rangeOfRV (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
@@ -36,6 +50,11 @@ def VaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
 
 notation "VaR[" X "//" P ", " α "]" => VaR P X α
 
+theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
+  (hXY : ∀ ω, X ω ≤ Y ω) : VaR P X α ≤ VaR P Y α := by
+
+  sorry
+
 --(Emily) I am now thinking of just trying to keep it in Q
 --so I wouln't use anything between these lines!
 ------------------- defined over the reals to prove monotonicity ---------------------------
@@ -58,7 +77,7 @@ theorem cdfR_monotone (P : Findist n) (X : FinRV n ℝ) (t1 t2 : ℝ)
 noncomputable def VaR_R (P : Findist n) (X : FinRV n ℝ) (α : ℝ) : ℝ :=
   sInf { t : ℝ | cdfR P X t ≥ α }
 
-theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℝ) (α : ℝ)
+theorem VaR_R_monotone (P : Findist n) (X Y : FinRV n ℝ) (α : ℝ)
   (hXY : ∀ ω, X ω ≤ Y ω) : VaR_R P X α ≤ VaR_R P Y α := by
   let Sx : Set ℝ := { t : ℝ | cdfR P X t ≥ α }
   let Sy : Set ℝ := { t : ℝ | cdfR P Y t ≥ α }
@@ -69,6 +88,8 @@ theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℝ) (α : ℝ)
     intro t ht
     have h_cdf : ∀ t, cdfR P X t ≥ cdfR P Y t := by
       intro t
+      unfold cdfR
+      --apply exp_monotone
 
       sorry
     sorry

From 61fe5a19ffaa4852c2b84834851820b0cbe372be Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Mon, 8 Dec 2025 14:36:41 -0500
Subject: [PATCH 07/16] small tweaks and another definition of var

---
 Probability/MDP/Risk.lean         | 39 ++++++++++++++++++++++---------
 Probability/Probability/Defs.lean |  7 ++++++
 2 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index e353ba8..a749bea 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -8,31 +8,32 @@ variable {n : ℕ}
 
 def cdf (P : Findist n) (X : FinRV n ℚ) (t : ℚ) : ℚ := ℙ[X ≤ᵣ t // P]
 
-theorem cdf_monotone (P : Findist n) (X : FinRV n ℚ) (t1 t2 : ℚ)
-  (ht : t1 ≤ t2) : cdf P X t1 ≤ cdf P X t2 := by
+variable {P : Findist n} {X : FinRV n ℚ} {t t₁ t₂ : ℚ}
+/-- shows CDF is non-decreasing -/
+theorem cdf_nondecreasing : t₁ ≤ t₂ → cdf P X t₁ ≤ cdf P X t₂ := by
+  intro ht 
   unfold cdf
   apply exp_monotone
   intro ω
-  by_cases h1 : X ω ≤ t1
-  · have h2 : X ω ≤ t2 := le_trans h1 ht
+  by_cases h1 : X ω ≤ t₁
+  · have h2 : X ω ≤ t₂ := le_trans h1 ht
     simp [FinRV.leq, 𝕀, indicator, h1, h2]
   · simp [𝕀, indicator, FinRV.leq, h1]
-    by_cases h2 : X ω ≤ t2
+    by_cases h2 : X ω ≤ t₂
     repeat simp [h2]
 
-theorem cdf_monotone_xy (P : Findist n) (X Y : FinRV n ℚ) (t : ℚ)
-  (h : X ≤ Y) : cdf P X t ≥ cdf P Y t := by
+/-- Shows CDF is monotone in random variable  -/
+theorem cdf_monotone_xy : X ≤ Y → cdf P X t ≥ cdf P Y t := by
+  intro h
   simp [cdf]
   apply exp_monotone
   intro ω
-  have h2 := h ω
   by_cases h1 : Y ω ≤ t
-  · have h3 : X ω ≤ t := le_trans h2 h1
+  · have h3 : X ω ≤ t := le_trans (h ω) h1
     simp [FinRV.leq, 𝕀, indicator, h3, h1]
   · simp [𝕀, indicator, FinRV.leq, h1]
     by_cases h4 : X ω ≤ t
-    · simp [h4]
-    · simp [h4]
+    repeat simp [h4]
 
 
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
@@ -136,3 +137,19 @@ notation "CVaR[" X "//" P ", " α "]" => CVaR P X α
 
 
 end Risk
+
+--- ************************* Another approach (Marek) ****************************************************
+
+section Risk2
+
+variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q : ℚ)
+
+/-- Checks if the function is a quantile --/
+def is_𝕢  : Prop := ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] ≥ 1-α  
+
+/-- Set of quantiles at a level α  --/
+def 𝕢Set : Set ℚ := { q | is_𝕢 P X α q} 
+
+
+
+end Risk2
diff --git a/Probability/Probability/Defs.lean b/Probability/Probability/Defs.lean
index 061b067..5ed4f07 100644
--- a/Probability/Probability/Defs.lean
+++ b/Probability/Probability/Defs.lean
@@ -127,6 +127,13 @@ infix:50 "=ᵢ" => FinRV.eqi
 /-- Boolean random variable represening Y ≤ y inequality -/
 infix:50 "≤ᵣ" => FinRV.leq
 
+/-- Boolean random variable represening Y ≤ y inequality -/
+@[simp] def geq [LE ρ] [DecidableLE ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
+  (fun ω ↦ Y ω ≥ y)
+
+/-- Boolean random variable represening Y ≤ y inequality -/
+infix:50 "≥ᵣ" => FinRV.geq
+
 /-- Boolean random variable represening Y > y inequality -/
 @[simp] def gt [LT ρ] [DecidableLT ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
   fun ω ↦ Y ω > y

From 03d8836283a91050be94ea0018376589117728a2 Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Mon, 8 Dec 2025 15:50:15 -0500
Subject: [PATCH 08/16] small simplifications; refactored a result from two
 proofs

---
 Probability/MDP/Risk.lean          | 29 ++++++++---------------------
 Probability/Probability/Basic.lean | 18 ++++++++++++++++++
 Probability/Probability/Defs.lean  |  4 ++--
 3 files changed, 28 insertions(+), 23 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index a749bea..5bc429b 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -8,32 +8,19 @@ variable {n : ℕ}
 
 def cdf (P : Findist n) (X : FinRV n ℚ) (t : ℚ) : ℚ := ℙ[X ≤ᵣ t // P]
 
-variable {P : Findist n} {X : FinRV n ℚ} {t t₁ t₂ : ℚ}
+variable {P : Findist n} {X Y : FinRV n ℚ} {t t₁ t₂ : ℚ}
+
+
 /-- shows CDF is non-decreasing -/
 theorem cdf_nondecreasing : t₁ ≤ t₂ → cdf P X t₁ ≤ cdf P X t₂ := by
-  intro ht 
-  unfold cdf
-  apply exp_monotone
-  intro ω
-  by_cases h1 : X ω ≤ t₁
-  · have h2 : X ω ≤ t₂ := le_trans h1 ht
-    simp [FinRV.leq, 𝕀, indicator, h1, h2]
-  · simp [𝕀, indicator, FinRV.leq, h1]
-    by_cases h2 : X ω ≤ t₂
-    repeat simp [h2]
+  intro ht; unfold cdf
+  exact exp_monotone <| rvle_monotone (le_refl X) ht 
+  
 
 /-- Shows CDF is monotone in random variable  -/
 theorem cdf_monotone_xy : X ≤ Y → cdf P X t ≥ cdf P Y t := by
-  intro h
-  simp [cdf]
-  apply exp_monotone
-  intro ω
-  by_cases h1 : Y ω ≤ t
-  · have h3 : X ω ≤ t := le_trans (h ω) h1
-    simp [FinRV.leq, 𝕀, indicator, h3, h1]
-  · simp [𝕀, indicator, FinRV.leq, h1]
-    by_cases h4 : X ω ≤ t
-    repeat simp [h4]
+  intro h; unfold cdf
+  exact exp_monotone <| rvle_monotone h (le_refl t) 
 
 
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
diff --git a/Probability/Probability/Basic.lean b/Probability/Probability/Basic.lean
index 751b013..3a07434 100644
--- a/Probability/Probability/Basic.lean
+++ b/Probability/Probability/Basic.lean
@@ -32,6 +32,23 @@ theorem in_prob (P : Findist n) : Prob ℙ[B // P] := ⟨ge_zero, le_one⟩
 
 end Findist
 
+
+section RandomVariables
+
+variable {n : ℕ} {P : Findist n} {A B : FinRV n Bool} {X Y : FinRV n ℚ} {t t₁ t₂ : ℚ}
+
+theorem rvle_monotone (h1 : X ≤ Y) (h2: t₁ ≤ t₂) : 𝕀 ∘ (Y ≤ᵣ t₁) ≤ 𝕀 ∘ (X ≤ᵣ t₂) := by 
+    intro ω   
+    by_cases h3 : Y ω ≤ t₁
+    · have h4 : X ω ≤ t₂ := le_trans (le_trans (h1 ω) h3) h2
+      simp [FinRV.leq, 𝕀, indicator, h3, h4] 
+    · by_cases h5 : X ω ≤ t₂
+      repeat simp [h3, h5, 𝕀, indicator] 
+      
+ 
+
+end RandomVariables
+
 ------------------------------ Probability ---------------------------
 
 variable {n : ℕ} {P : Findist n} {A B C : FinRV n Bool}
@@ -45,6 +62,7 @@ theorem prob_compl_one_minus : ℙ[¬ᵣB // P] = 1 - ℙ[B // P] :=
 
 
 
+
 ------------------------------ Expectation ---------------------------
 
 section Expectation 
diff --git a/Probability/Probability/Defs.lean b/Probability/Probability/Defs.lean
index 5ed4f07..f8ed4ed 100644
--- a/Probability/Probability/Defs.lean
+++ b/Probability/Probability/Defs.lean
@@ -156,10 +156,10 @@ def preimage (f : FinRV n ρ) : ρ → Set (Fin n) :=
 end FinRV
 
 /-- Boolean indicator function -/
-def indicator  [OfNat ρ 0] [OfNat ρ 1] (cond : Bool) : ρ := cond.rec 0 1
+def indicator  [OfNat ℚ 0] [OfNat ℚ 1] (cond : Bool) : ℚ := cond.rec 0 1
 
 /-- Boolean indicator function -/
-abbrev 𝕀 [OfNat ρ 0] [OfNat ρ 1] : Bool → ρ := indicator
+abbrev 𝕀 [OfNat ℚ 0] [OfNat ℚ 1] : Bool → ℚ := indicator
 
 
 variable {k : ℕ} {L : FinRV n (Fin k)}

From 5725b2f3b8aa6e3169ad5b956924c8e56de3b9ed Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Fri, 12 Dec 2025 17:31:46 -0500
Subject: [PATCH 09/16] another var definition

---
 Probability/MDP/Risk.lean          | 18 +++++++++++++-----
 Probability/Probability/Basic.lean |  2 --
 Probability/Probability/Defs.lean  |  8 ++++++++
 3 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 5bc429b..ba63cfa 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -22,23 +22,29 @@ theorem cdf_monotone_xy : X ≤ Y → cdf P X t ≥ cdf P Y t := by
   intro h; unfold cdf
   exact exp_monotone <| rvle_monotone h (le_refl t) 
 
-
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
-def rangeOfRV (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
+def range (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
+
+--def FinQuantile (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ := 
 
+-- TODO: consider also this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Stieltjes.html#StieltjesFunction.toFun 
+
+-- TODO: should we call this FinVaR? and show it is equal to a more standard definition of VaR
 /-- 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 ≥ α)
+  let S : Finset ℚ := (range X).filter (fun t => cdf P X t ≥ α)
   if h : S.Nonempty then
     S.min' h
   else
     0 --this is illegal i know -- Keith can fix it :)
 
+-- TODO: Show that VaR is a left (or right?) inverse for CDF
+
 notation "VaR[" X "//" P ", " α "]" => VaR P X α
 
 theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
-  (hXY : ∀ ω, X ω ≤ Y ω) : VaR P X α ≤ VaR P Y α := by
+  (hXY : X ≤ Y) : VaR P X α ≤ VaR P Y α := by
 
   sorry
 
@@ -129,7 +135,7 @@ end Risk
 
 section Risk2
 
-variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q : ℚ)
+variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q v : ℚ)
 
 /-- Checks if the function is a quantile --/
 def is_𝕢  : Prop := ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] ≥ 1-α  
@@ -137,6 +143,8 @@ def is_𝕢  : Prop := ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] 
 /-- Set of quantiles at a level α  --/
 def 𝕢Set : Set ℚ := { q | is_𝕢 P X α q} 
 
+def is_VaR : Prop := (v ∈ 𝕢Set P X α) ∧ ∀u ∈ 𝕢Set P X α, v ≥ u 
 
+theorem var_def : is_VaR P X α v ↔ (α ≥ ℙ[X <ᵣ v // P] ∧ α < ℙ[ X ≤ᵣ v // P]  ) := sorry 
 
 end Risk2
diff --git a/Probability/Probability/Basic.lean b/Probability/Probability/Basic.lean
index 3a07434..137a5a9 100644
--- a/Probability/Probability/Basic.lean
+++ b/Probability/Probability/Basic.lean
@@ -45,8 +45,6 @@ theorem rvle_monotone (h1 : X ≤ Y) (h2: t₁ ≤ t₂) : 𝕀 ∘ (Y ≤ᵣ t
     · by_cases h5 : X ω ≤ t₂
       repeat simp [h3, h5, 𝕀, indicator] 
       
- 
-
 end RandomVariables
 
 ------------------------------ Probability ---------------------------
diff --git a/Probability/Probability/Defs.lean b/Probability/Probability/Defs.lean
index f8ed4ed..47b4dfd 100644
--- a/Probability/Probability/Defs.lean
+++ b/Probability/Probability/Defs.lean
@@ -127,6 +127,14 @@ infix:50 "=ᵢ" => FinRV.eqi
 /-- Boolean random variable represening Y ≤ y inequality -/
 infix:50 "≤ᵣ" => FinRV.leq
 
+
+/-- Boolean random variable represening Y ≤ y inequality -/
+@[simp] def lt [LT ρ] [DecidableLT ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
+  (fun ω ↦ Y ω < y)
+
+/-- Boolean random variable represening Y ≤ y inequality -/
+infix:50 "<ᵣ" => FinRV.lt
+
 /-- Boolean random variable represening Y ≤ y inequality -/
 @[simp] def geq [LE ρ] [DecidableLE ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
   (fun ω ↦ Y ω ≥ y)

From d0f5c7c225abf4e4da937a7a133bdb3c5b99ebcd Mon Sep 17 00:00:00 2001
From: Emily Chandran <emily.chandran@unh.edu>
Date: Fri, 12 Dec 2025 17:34:25 -0500
Subject: [PATCH 10/16] start of Caleb's ideas

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

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index ba63cfa..7c46fb7 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -14,20 +14,20 @@ variable {P : Findist n} {X Y : FinRV n ℚ} {t t₁ t₂ : ℚ}
 /-- shows CDF is non-decreasing -/
 theorem cdf_nondecreasing : t₁ ≤ t₂ → cdf P X t₁ ≤ cdf P X t₂ := by
   intro ht; unfold cdf
-  exact exp_monotone <| rvle_monotone (le_refl X) ht 
-  
+  exact exp_monotone <| rvle_monotone (le_refl X) ht
+
 
 /-- Shows CDF is monotone in random variable  -/
 theorem cdf_monotone_xy : X ≤ Y → cdf P X t ≥ cdf P Y t := by
   intro h; unfold cdf
-  exact exp_monotone <| rvle_monotone h (le_refl t) 
+  exact exp_monotone <| rvle_monotone h (le_refl t)
 
 /-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
 def range (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
 
---def FinQuantile (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ := 
+--def FinQuantile (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
 
--- TODO: consider also this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Stieltjes.html#StieltjesFunction.toFun 
+-- TODO: consider also this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Stieltjes.html#StieltjesFunction.toFun
 
 -- TODO: should we call this FinVaR? and show it is equal to a more standard definition of VaR
 /-- Value-at-Risk of X at level α: VaR_α(X) = min { t ∈ X(Ω) | P[X ≤ t] ≥ α }.
@@ -48,6 +48,38 @@ theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
 
   sorry
 
+
+------------------Caleb's definition of VaR------------------------
+theorem min_subset (A B : Finset ℕ) (h : B ⊆ A) (hA : A.Nonempty) (hB : B.Nonempty)  : A.min' hA ≤ B.min' hB :=
+  by
+    have hminB : B.min' hB ∈ B := Finset.min'_mem B hB
+    have hminA : B.min' hB ∈ A := h hminB
+    exact Finset.min'_le A (B.min' hB) hminA
+
+def prodDenomRV (X : FinRV n ℚ) : ℕ := ∏ q ∈ range X, q.den
+
+theorem RV_QtoZ (X : FinRV n ℚ) (ω : Fin n) :
+  ∃ z : ℤ, X ω * (prodDenomRV X : ℚ) = z := sorry
+
+theorem Lx_nonempty (P : Findist n) (X : FinRV n ℚ) (α : ℚ) :
+  let Lx : Finset ℚ := (range X).filter (fun t => cdf P X t ≤ 1-α)
+  Lx.Nonempty := sorry
+
+-- def min_Lx (P : Findist n) (X : FinRV n ℚ) (α : ℚ) :
+--   let Lx : Finset ℚ := (range X).filter (fun t => cdf P X t ≤ 1-α)
+--   Lx.min' (Lx_nonempty P X α) := sorry
+
+
+
+
+
+def VaR_caleb (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ := sorry
+
+------------------------------------------------------------------------
+
+
+
+
 --(Emily) I am now thinking of just trying to keep it in Q
 --so I wouln't use anything between these lines!
 ------------------- defined over the reals to prove monotonicity ---------------------------
@@ -138,13 +170,13 @@ section Risk2
 variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q v : ℚ)
 
 /-- Checks if the function is a quantile --/
-def is_𝕢  : Prop := ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] ≥ 1-α  
+def is_𝕢  : Prop := ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] ≥ 1-α
 
 /-- Set of quantiles at a level α  --/
-def 𝕢Set : Set ℚ := { q | is_𝕢 P X α q} 
+def 𝕢Set : Set ℚ := { q | is_𝕢 P X α q}
 
-def is_VaR : Prop := (v ∈ 𝕢Set P X α) ∧ ∀u ∈ 𝕢Set P X α, v ≥ u 
+def is_VaR : Prop := (v ∈ 𝕢Set P X α) ∧ ∀u ∈ 𝕢Set P X α, v ≥ u
 
-theorem var_def : is_VaR P X α v ↔ (α ≥ ℙ[X <ᵣ v // P] ∧ α < ℙ[ X ≤ᵣ v // P]  ) := sorry 
+theorem var_def : is_VaR P X α v ↔ (α ≥ ℙ[X <ᵣ v // P] ∧ α < ℙ[ X ≤ᵣ v // P]  ) := sorry
 
 end Risk2

From 3aed0507381692bad25b162958f57c8977224a8f Mon Sep 17 00:00:00 2001
From: Emily Chandran <emily.chandran@unh.edu>
Date: Fri, 19 Dec 2025 08:26:41 -0500
Subject: [PATCH 11/16] work on caleb's var

---
 Probability/MDP/Risk.lean | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 7c46fb7..aab7606 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -58,22 +58,38 @@ theorem min_subset (A B : Finset ℕ) (h : B ⊆ A) (hA : A.Nonempty) (hB : B.No
 
 def prodDenomRV (X : FinRV n ℚ) : ℕ := ∏ q ∈ range X, q.den
 
+
+def X' (X : FinRV n ℚ) : FinRV n ℚ :=
+  fun ω => X ω * (prodDenomRV X : ℚ)
+
 theorem RV_QtoZ (X : FinRV n ℚ) (ω : Fin n) :
-  ∃ z : ℤ, X ω * (prodDenomRV X : ℚ) = z := sorry
+  ∃ z : ℤ, X ω * (prodDenomRV X : ℚ) = (z : ℚ) := sorry
 
-theorem Lx_nonempty (P : Findist n) (X : FinRV n ℚ) (α : ℚ) :
-  let Lx : Finset ℚ := (range X).filter (fun t => cdf P X t ≤ 1-α)
-  Lx.Nonempty := sorry
+def X'_num (X : FinRV n ℚ) : FinRV n ℤ :=
+  fun ω => (X ω * (prodDenomRV X : ℚ)).num
+
+theorem X'_num_inQ (X : FinRV n ℚ) (ω : Fin n) :
+  X ω * (prodDenomRV X : ℚ) = (X'_num X ω : ℚ) := sorry
 
--- def min_Lx (P : Findist n) (X : FinRV n ℚ) (α : ℚ) :
---   let Lx : Finset ℚ := (range X).filter (fun t => cdf P X t ≤ 1-α)
---   Lx.min' (Lx_nonempty P X α) := sorry
 
+def Lx (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : Finset ℚ :=
+  (range X).filter (fun t => cdf P X t ≤ (1 : ℚ) - α)
 
+theorem Lx_nonempty (P : Findist n) (X : FinRV n ℚ) (α : ℚ) :
+  (Lx P X α).Nonempty := sorry
+
+def min_Lx (P : Findist n) (X : FinRV n ℚ) (α : ℚ) :=
+  (Lx P X α).min' (Lx_nonempty P X α)
 
+--Caleb has a handwritten proof showing this definition is equivalent
+def VaR_caleb (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
+  (min_Lx P X α) / prodDenomRV X
 
 
-def VaR_caleb (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ := sorry
+
+theorem VaR_caleb_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
+  (hXY : X ≤ Y) : VaR_caleb P X α ≤ VaR_caleb P Y α := by
+  sorry
 
 ------------------------------------------------------------------------
 

From f2f54d951a6dbf0a452ad1b4476014751f0f6429 Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Fri, 19 Dec 2025 09:17:44 -0500
Subject: [PATCH 12/16] some var

---
 Probability/MDP/Risk.lean         | 19 +++++++++++++++++--
 Probability/Probability/Defs.lean |  6 +++++-
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 7c46fb7..85e5e66 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -27,7 +27,8 @@ def range (X : FinRV n ℚ) : Finset ℚ := Finset.univ.image X
 
 --def FinQuantile (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
 
--- TODO: consider also this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Stieltjes.html#StieltjesFunction.toFun
+-- TODO: consider also this: 
+-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Stieltjes.html#StieltjesFunction.toFun
 
 -- TODO: should we call this FinVaR? and show it is equal to a more standard definition of VaR
 /-- Value-at-Risk of X at level α: VaR_α(X) = min { t ∈ X(Ω) | P[X ≤ t] ≥ α }.
@@ -167,7 +168,21 @@ end Risk
 
 section Risk2
 
-variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q v : ℚ)
+variable {n : ℕ} {P : Findist n} {X Y : FinRV n ℚ} {t : ℚ} 
+
+theorem rv_le_compl_gt : (X ≤ᵣ t) + (X >ᵣ t) = 1 := by 
+  ext ω
+  unfold FinRV.leq FinRV.gt 
+  simp 
+  grind  
+
+
+theorem prob_le_compl_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P]= 1 := by 
+  rewrite [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_additive]
+
+variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q v : ℚ) 
+
+  
 
 /-- Checks if the function is a quantile --/
 def is_𝕢  : Prop := ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] ≥ 1-α
diff --git a/Probability/Probability/Defs.lean b/Probability/Probability/Defs.lean
index 47b4dfd..6996fda 100644
--- a/Probability/Probability/Defs.lean
+++ b/Probability/Probability/Defs.lean
@@ -225,7 +225,6 @@ end RandomVariable
 
 ------------------------------ Probability ---------------------------
 
-
 variable {n : ℕ} (P : Findist n) (B C : FinRV n Bool)
 
 /-- Probability of B -/
@@ -370,6 +369,11 @@ theorem exp_dists_add : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := by sim
 theorem exp_additive {m : ℕ} (Xs : Fin m → FinRV n ℚ) : 𝔼[∑ i : Fin m, Xs i // P] = ∑ i : Fin m, 𝔼[Xs i // P] := 
   by unfold expect; exact dotProduct_sum P.p Finset.univ Xs
 
+theorem exp_additive_two : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := 
+  by unfold expect; 
+     sorry 
+     --exact dotProduct_sum P.p Finset.univ Xs
+
 /-- Expectation is monotone  -/
 theorem exp_monotone (h: X ≤ Y)  : 𝔼[X // P] ≤ 𝔼[Y // P] :=  dotProduct_le_dotProduct_of_nonneg_left h P.nneg
 

From a5810818db521448b4460ffeb651d8584346a20b Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Mon, 29 Dec 2025 19:03:22 +0000
Subject: [PATCH 13/16] added invariance to permutation

---
 Probability/MDP/Risk.lean          | 56 ++++++++++++------------------
 Probability/Probability/Basic.lean | 40 ++++++++++++++++++---
 Probability/Probability/Defs.lean  | 31 +++++++++++------
 3 files changed, 79 insertions(+), 48 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 1dfb135..6339d19 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -1,4 +1,6 @@
 import Probability.Probability.Basic
+import Mathlib.Data.EReal.Basic 
+import Mathlib.Data.Set.Operations
 
 namespace Risk
 
@@ -46,10 +48,11 @@ notation "VaR[" X "//" P ", " α "]" => VaR P X α
 
 theorem VaR_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
   (hXY : X ≤ Y) : VaR P X α ≤ VaR P Y α := by
-
   sorry
 
 
+example (A B : Set EReal) (h : A ⊆ B) : sSup A ≤ sSup B := sSup_le_sSup h
+
 ------------------Caleb's definition of VaR------------------------
 theorem min_subset (A B : Finset ℕ) (h : B ⊆ A) (hA : A.Nonempty) (hB : B.Nonempty)  : A.min' hA ≤ B.min' hB :=
   by
@@ -146,37 +149,6 @@ theorem VaR_positive_homog (P : Findist n) (X : FinRV n ℚ) (α c : ℚ)
   (hc : c > 0) : VaR P (fun ω => c * X ω) α = c * VaR P X α := sorry
 
 
-/-- Tail indicator: 1 if X(ω) > t, else 0. -/
-def tailInd (X : FinRV n ℚ) (t : ℚ) : FinRV n ℚ :=
-  fun ω => if X ω > t then 1 else 0
-
-/-- Conditional Value-at-Risk (CVaR) of X at level α under P.
-CVaR_α(X) =  E[X * I[X > VaR] ] / P[X > VaR]
-If the tail probability is zero, CVaR is defined to be 0.
--/
-def CVaR (P : Findist n) (X : FinRV n ℚ) (α : ℚ) : ℚ :=
-  let v := VaR P X α
-  let B : FinRV n ℚ := tailInd X v
-  let num := 𝔼[X * B // P]
-  let den := ℙ[X >ᵣ v // P]
-  if _ : den = 0 then
-     0
-  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...
--- monotonicity: (∀ ω, X ω ≤ Y ω) → CVaR[α, X // P] ≤ CVaR[α, Y // P]
--- translation: CVaR[α, (fun ω => X ω + c) // P] = CVaR[α, X // P] + c
--- positive homogeneity: c > 0 → CVaR[α, (fun ω => c * X ω) // P] = c * CVaR[α, X // P]
--- convexity
--- CVaR ≥ VaR: CVaR[α, X // P] ≥ VaR[α, X // P]
-
 
 end Risk
 
@@ -184,6 +156,12 @@ end Risk
 
 section Risk2
 
+#check Set.preimage
+#synth SupSet EReal 
+#synth SupSet (WithTop ℝ)
+#check instSupSetEReal
+#check WithTop.instSupSet
+
 variable {n : ℕ} {P : Findist n} {X Y : FinRV n ℚ} {t : ℚ} 
 
 theorem rv_le_compl_gt : (X ≤ᵣ t) + (X >ᵣ t) = 1 := by 
@@ -194,7 +172,8 @@ theorem rv_le_compl_gt : (X ≤ᵣ t) + (X >ᵣ t) = 1 := by
 
 
 theorem prob_le_compl_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P]= 1 := by 
-  rewrite [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_additive]
+  sorry
+  --rewrite [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_additive]
 
 variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q v : ℚ) 
 
@@ -208,6 +187,17 @@ def 𝕢Set : Set ℚ := { q | is_𝕢 P X α q}
 
 def is_VaR : Prop := (v ∈ 𝕢Set P X α) ∧ ∀u ∈ 𝕢Set P X α, v ≥ u
 
+
+-- theorem prob_monotone_sharp {t₁ t₂ : ℚ} : t₁ < t₂ → ℙ[X ≥ᵣ t₂ // P] ≤ ℙ[X >ᵣ t₁ // P] := 
+
+theorem rv_monotone_sharp {t₁ t₂ : ℚ} : t₁ < t₂ → ∀ ω, (X ≥ᵣ t₂) ω →(X >ᵣ t₁) ω   := 
+    by intro h ω pre
+       simp [FinRV.gt, FinRV.geq] at pre ⊢ 
+       linarith 
+       
+
 theorem var_def : is_VaR P X α v ↔ (α ≥ ℙ[X <ᵣ v // P] ∧ α < ℙ[ X ≤ᵣ v // P]  ) := sorry
 
+
+
 end Risk2
diff --git a/Probability/Probability/Basic.lean b/Probability/Probability/Basic.lean
index 137a5a9..1cc5dd3 100644
--- a/Probability/Probability/Basic.lean
+++ b/Probability/Probability/Basic.lean
@@ -4,6 +4,9 @@ import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Data.Fintype.BigOperators
 
+import Mathlib.Data.Fin.Tuple.Sort 
+
+
 /-!
   # Basic properties for probability spaces and expectations
 
@@ -19,7 +22,7 @@ variable {n : ℕ} {P : Findist n} {B : FinRV n Bool}
 
 theorem ge_zero : 0 ≤ ℙ[B // P] := 
     by rw [prob_eq_exp_ind]
-       calc 0 = 𝔼[0 // P] := exp_const.symm 
+       calc 0 = 𝔼[0 //P] := exp_const.symm 
             _ ≤ 𝔼[𝕀 ∘ B//P] := exp_monotone ind_nneg
        
 
@@ -52,15 +55,13 @@ end RandomVariables
 variable {n : ℕ} {P : Findist n} {A B C : FinRV n Bool}
 
 theorem prob_compl_sums_to_one : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 := 
-    by rw [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_dists_add, one_of_ind_bool_or_not]
+    by rw [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_additive_two, one_of_ind_bool_or_not]
        exact exp_one 
 
 theorem prob_compl_one_minus : ℙ[¬ᵣB // P] = 1 - ℙ[B // P] :=
     by rw [←prob_compl_sums_to_one (P:=P) (B:=B)]; ring 
 
 
-
-
 ------------------------------ Expectation ---------------------------
 
 section Expectation 
@@ -110,4 +111,33 @@ theorem law_of_total_probs : ℙ[B // P] =  ∑ i, ℙ[B * (L =ᵣ i) // P]  :=
 
 end Probability 
 
-#lint 
+section Probability_Permutation
+
+variable {n : ℕ} {P : Findist n} {A B : FinRV n Bool} {X Y : FinRV n ℚ}
+
+example (σ : Equiv.Perm (Fin n)) (f g : Fin n → ℚ) : f ⬝ᵥ g = (f ∘ σ) ⬝ᵥ (g ∘ σ) := 
+  by exact Eq.symm (comp_equiv_dotProduct_comp_equiv f g σ)
+
+example (σ : Equiv.Perm (Fin n)) : (1 : Fin n → ℚ) = (1 : Fin n → ℚ) ∘ σ := rfl
+
+def Findist.perm (P : Findist n) (σ : Equiv.Perm (Fin n)) : Findist n where 
+  p :=  P.p ∘ σ
+  prob := by 
+    have h1 : 1 = (1 : Fin n → ℚ) ∘ σ := rfl 
+    rw [h1, comp_equiv_dotProduct_comp_equiv 1 P.p σ]
+    exact P.prob
+  nneg := fun ω => P.nneg (σ ω)
+
+variable (σ : Equiv.Perm (Fin n))
+
+theorem exp_equiv_perm : 𝔼[X ∘ σ // P.perm σ] = 𝔼[X // P] := by
+  unfold expect Findist.perm 
+  exact (comp_equiv_dotProduct_comp_equiv P.1 X σ)
+
+example : (𝕀 ∘ A ∘ σ) = (𝕀 ∘ A) ∘ σ := by rfl 
+
+theorem prob_equiv_perm : ℙ[A ∘ σ // P.perm σ] = ℙ[A // P] := by 
+  have h1 : (𝕀 ∘ A ∘ σ) = (𝕀 ∘ A) ∘ σ := by rfl 
+  rw [prob_eq_exp_ind, h1, exp_equiv_perm, ←prob_eq_exp_ind] 
+  
+end Probability_Permutation 
diff --git a/Probability/Probability/Defs.lean b/Probability/Probability/Defs.lean
index 6996fda..8f979ab 100644
--- a/Probability/Probability/Defs.lean
+++ b/Probability/Probability/Defs.lean
@@ -363,19 +363,14 @@ theorem exp_indi_eq_exp_indr : ∀i : Fin k, 𝔼[L =ᵢ i // P] = 𝔼[𝕀 ∘
 /-- Expectation is homogeneous under product -/
 theorem exp_homogenous : 𝔼[c • X // P] = c * 𝔼[X // P] := by simp only [expect, dotProduct_smul, smul_eq_mul]
 
-theorem exp_dists_add : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := by simp [expect]
-
 /-- Additivity of expectation --/
 theorem exp_additive {m : ℕ} (Xs : Fin m → FinRV n ℚ) : 𝔼[∑ i : Fin m, Xs i // P] = ∑ i : Fin m, 𝔼[Xs i // P] := 
   by unfold expect; exact dotProduct_sum P.p Finset.univ Xs
-
-theorem exp_additive_two : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := 
-  by unfold expect; 
-     sorry 
-     --exact dotProduct_sum P.p Finset.univ Xs
+     
+theorem exp_additive_two : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := by simp [expect]
 
 /-- Expectation is monotone  -/
-theorem exp_monotone (h: X ≤ Y)  : 𝔼[X // P] ≤ 𝔼[Y // P] :=  dotProduct_le_dotProduct_of_nonneg_left h P.nneg
+theorem exp_monotone (h: X ≤ Y)  : 𝔼[X // P] ≤ 𝔼[Y // P] := dotProduct_le_dotProduct_of_nonneg_left h P.nneg
 
 ---- ** conditional expectation -----
 
@@ -386,7 +381,6 @@ theorem exp_decompose : 𝔼[X // P] = ∑ i, 𝔼[X * (L =ᵢ i) // P] :=
      rewrite [exp_additive]
      simp 
 
-
 /-- Expectation of a conditional constant. Only when probability is positive.  -/
 theorem exp_cond_const : ∀ i, ℙ[L =ᵣ i //   P] ≠ 0 → 𝔼[g ∘ L | L =ᵣ i // P] = g i := 
     by intro i h 
@@ -397,4 +391,21 @@ theorem exp_cond_const : ∀ i, ℙ[L =ᵣ i //   P] ≠ 0 → 𝔼[g ∘ L | L
 
 end Expectation_properties
 
-#lint 
+
+-- Derived properties from the properties of expectation
+section Probability_properties
+
+variable {n : ℕ} {P : Findist n} {A B : FinRV n Bool}
+
+theorem ind_monotone : (∀ ω, A ω → B ω) → (𝕀∘A) ≤ (𝕀∘B) := by
+  intro h ω
+  specialize h ω
+  by_cases h1 : A ω
+  · simp_all [indicator] 
+  · by_cases h2 : B ω
+    repeat simp_all [indicator]
+
+
+
+
+end Probability_properties 

From 924d9fc65cfb60da5cb12add9d569b0721193342 Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Mon, 29 Dec 2025 22:29:12 +0000
Subject: [PATCH 14/16] partial var definition

---
 Probability/MDP/Risk.lean          | 37 ++++++++++++++++++++++++++++--
 Probability/Probability/Basic.lean | 28 ++++++++++++++++------
 2 files changed, 56 insertions(+), 9 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 6339d19..d2f6dbb 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -177,7 +177,6 @@ theorem prob_le_compl_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P]= 1 := by
 
 variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q v : ℚ) 
 
-  
 
 /-- Checks if the function is a quantile --/
 def is_𝕢  : Prop := ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] ≥ 1-α
@@ -198,6 +197,40 @@ theorem rv_monotone_sharp {t₁ t₂ : ℚ} : t₁ < t₂ → ∀ ω, (X ≥ᵣ
 
 theorem var_def : is_VaR P X α v ↔ (α ≥ ℙ[X <ᵣ v // P] ∧ α < ℙ[ X ≤ᵣ v // P]  ) := sorry
 
-
+def IsRiskLevel (α : ℚ) : Prop := 0 ≤ α ∧ α < 1
+
+def RiskLevel := { α : ℚ // IsRiskLevel α}
+
+
+/-- compute a quantile for a partial sorted random variable and a partial probability 
+    used in the induction to eliminate points until we find one that has 
+    probability greater than α -/
+def quantile_srt (n : ℕ) (α : RiskLevel) (p : Fin n.succ → ℚ) (x : Fin n.succ → ℚ) 
+                 (h1 : Monotone x) (h2 : ∀ω, 0 ≤ p ω) (h3 : α.val < 1 ⬝ᵥ p) : ℚ := 
+  match n with 
+  | Nat.zero => x 0 
+  | Nat.succ n' =>
+    if h : p 0 < α.val then 
+      let α':= α.val - p 0 
+      let bnd_α : IsRiskLevel α' := by 
+        unfold IsRiskLevel  
+        subst α' 
+        specialize h2 0 
+        constructor 
+        · grw [←h]; simp 
+        · grw [←h2]; simpa using α.2.2 
+
+      quantile_srt n' ⟨α', bnd_α⟩ (Fin.tail p) (Fin.tail x) sorry sorry sorry 
+    else 
+      x 0 
+
+example (X : Fin (n.succ) → ℚ) (h : Monotone X) : Monotone (Fin.tail X) := sorry
+
+def FinVaR (α : RiskLevel) (P : Findist n) (X : FinRV n ℚ) : ℚ := 
+    match n with 
+    | Nat.zero => 0 -- this case is not possible because of the probability distribution
+    | Nat.succ n' =>
+      let σ := Tuple.sort X 
+      quantile_srt n' α (P.p ∘ σ) (X ∘ σ) sorry sorry sorry 
 
 end Risk2
diff --git a/Probability/Probability/Basic.lean b/Probability/Probability/Basic.lean
index 1cc5dd3..4bdeea3 100644
--- a/Probability/Probability/Basic.lean
+++ b/Probability/Probability/Basic.lean
@@ -4,7 +4,7 @@ import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Data.Fintype.BigOperators
 
-import Mathlib.Data.Fin.Tuple.Sort 
+import Mathlib.Data.Fin.Tuple.Sort -- for Equiv.Perm and permutation operations
 
 
 /-!
@@ -113,7 +113,7 @@ end Probability
 
 section Probability_Permutation
 
-variable {n : ℕ} {P : Findist n} {A B : FinRV n Bool} {X Y : FinRV n ℚ}
+variable {n : ℕ} {P : Findist n} {A B : FinRV n Bool} {X Y : FinRV n ℚ} {t : ℚ}
 
 example (σ : Equiv.Perm (Fin n)) (f g : Fin n → ℚ) : f ⬝ᵥ g = (f ∘ σ) ⬝ᵥ (g ∘ σ) := 
   by exact Eq.symm (comp_equiv_dotProduct_comp_equiv f g σ)
@@ -130,14 +130,28 @@ def Findist.perm (P : Findist n) (σ : Equiv.Perm (Fin n)) : Findist n where
 
 variable (σ : Equiv.Perm (Fin n))
 
-theorem exp_equiv_perm : 𝔼[X ∘ σ // P.perm σ] = 𝔼[X // P] := by
+theorem exp_eq_perm : 𝔼[X ∘ σ // P.perm σ] = 𝔼[X // P] := by
   unfold expect Findist.perm 
   exact (comp_equiv_dotProduct_comp_equiv P.1 X σ)
 
-example : (𝕀 ∘ A ∘ σ) = (𝕀 ∘ A) ∘ σ := by rfl 
-
-theorem prob_equiv_perm : ℙ[A ∘ σ // P.perm σ] = ℙ[A // P] := by 
+theorem prob_eq_perm : ℙ[A ∘ σ // P.perm σ] = ℙ[A // P] := by 
   have h1 : (𝕀 ∘ A ∘ σ) = (𝕀 ∘ A) ∘ σ := by rfl 
-  rw [prob_eq_exp_ind, h1, exp_equiv_perm, ←prob_eq_exp_ind] 
+  rw [prob_eq_exp_ind, h1, exp_eq_perm, ←prob_eq_exp_ind] 
   
+theorem rv_le_perm : (X ∘ σ ≤ᵣ t) = (X ≤ᵣ t) ∘ σ := by unfold FinRV.leq; grind only 
+
+theorem rv_lt_perm : (X ∘ σ <ᵣ t) = (X <ᵣ t) ∘ σ := by unfold FinRV.lt; grind only 
+
+theorem rv_ge_perm : (X ∘ σ ≥ᵣ t) = (X ≥ᵣ t) ∘ σ := by unfold FinRV.geq; grind only 
+
+theorem rv_gt_perm : (X ∘ σ >ᵣ t) = (X >ᵣ t) ∘ σ := by unfold FinRV.gt; grind only 
+
+theorem prob_le_eq_perm : ℙ[X ∘ σ ≤ᵣ t // P.perm σ] = ℙ[X ≤ᵣ t // P] := by rw [rv_le_perm, prob_eq_perm]
+
+theorem prob_lt_eq_perm : ℙ[X ∘ σ <ᵣ t // P.perm σ] = ℙ[X <ᵣ t // P] := by rw [rv_lt_perm, prob_eq_perm]
+
+theorem prob_ge_eq_perm : ℙ[X ∘ σ ≥ᵣ t // P.perm σ] = ℙ[X ≥ᵣ t // P] := by rw [rv_ge_perm, prob_eq_perm]
+
+theorem prob_gt_eq_perm : ℙ[X ∘ σ >ᵣ t // P.perm σ] = ℙ[X >ᵣ t // P] := by rw [rv_gt_perm, prob_eq_perm]
+
 end Probability_Permutation 

From edf064d0b750bb1070f263f9850629e00284ddc4 Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Mon, 29 Dec 2025 22:43:01 +0000
Subject: [PATCH 15/16] removed some sorrys

---
 Probability/MDP/Risk.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index d2f6dbb..76d7426 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -201,6 +201,12 @@ def IsRiskLevel (α : ℚ) : Prop := 0 ≤ α ∧ α < 1
 
 def RiskLevel := { α : ℚ // IsRiskLevel α}
 
+theorem tail_monotone (X : Fin (n.succ) → ℚ) (h : Monotone X) : Monotone (Fin.tail X) := 
+    by unfold Monotone at h ⊢ 
+       unfold Fin.tail 
+       intro a b h2 
+       exact h (Fin.succ_le_succ_iff.mpr h2)
+      
 
 /-- compute a quantile for a partial sorted random variable and a partial probability 
     used in the induction to eliminate points until we find one that has 
@@ -219,16 +225,14 @@ def quantile_srt (n : ℕ) (α : RiskLevel) (p : Fin n.succ → ℚ) (x : Fin n.
         constructor 
         · grw [←h]; simp 
         · grw [←h2]; simpa using α.2.2 
-
-      quantile_srt n' ⟨α', bnd_α⟩ (Fin.tail p) (Fin.tail x) sorry sorry sorry 
+      quantile_srt n' ⟨α', bnd_α⟩ (Fin.tail p) (Fin.tail x) (tail_monotone x h1) (fun ω ↦ h2 ω.succ) sorry 
     else 
       x 0 
 
-example (X : Fin (n.succ) → ℚ) (h : Monotone X) : Monotone (Fin.tail X) := sorry
 
 def FinVaR (α : RiskLevel) (P : Findist n) (X : FinRV n ℚ) : ℚ := 
     match n with 
-    | Nat.zero => 0 -- this case is not possible because of the probability distribution
+    | Nat.zero => 0 -- this case is impossible because n > 0 for Findist 
     | Nat.succ n' =>
       let σ := Tuple.sort X 
       quantile_srt n' α (P.p ∘ σ) (X ∘ σ) sorry sorry sorry 

From c5d110e915f6990fe37f927aba0a03e598b00f7b Mon Sep 17 00:00:00 2001
From: Marek Petrik <mpetrik@cs.unh.edu>
Date: Tue, 6 Jan 2026 15:16:18 -0500
Subject: [PATCH 16/16] completed definition of quantile+

---
 Probability/MDP/Risk.lean | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/Probability/MDP/Risk.lean b/Probability/MDP/Risk.lean
index 76d7426..403a02c 100644
--- a/Probability/MDP/Risk.lean
+++ b/Probability/MDP/Risk.lean
@@ -164,6 +164,8 @@ section Risk2
 
 variable {n : ℕ} {P : Findist n} {X Y : FinRV n ℚ} {t : ℚ} 
 
+--TODO: can we use isLUB
+
 theorem rv_le_compl_gt : (X ≤ᵣ t) + (X >ᵣ t) = 1 := by 
   ext ω
   unfold FinRV.leq FinRV.gt 
@@ -195,7 +197,9 @@ theorem rv_monotone_sharp {t₁ t₂ : ℚ} : t₁ < t₂ → ∀ ω, (X ≥ᵣ
        linarith 
        
 
-theorem var_def : is_VaR P X α v ↔ (α ≥ ℙ[X <ᵣ v // P] ∧ α < ℙ[ X ≤ᵣ v // P]  ) := sorry
+-- this proves that if we have the property we also have the VaR; then all remains is 
+-- to show existence which we can shows constructively by actually computing the value
+theorem var_def : is_VaR P X α v ↔ (α ≥ ℙ[X <ᵣ v // P] ∧ α < ℙ[ X ≤ᵣ v // P]) := sorry
 
 def IsRiskLevel (α : ℚ) : Prop := 0 ≤ α ∧ α < 1
 
@@ -208,7 +212,7 @@ theorem tail_monotone (X : Fin (n.succ) → ℚ) (h : Monotone X) : Monotone (Fi
        exact h (Fin.succ_le_succ_iff.mpr h2)
       
 
-/-- compute a quantile for a partial sorted random variable and a partial probability 
+/-- compute a quantile for a (partial) sorted random variable and a partial probability 
     used in the induction to eliminate points until we find one that has 
     probability greater than α -/
 def quantile_srt (n : ℕ) (α : RiskLevel) (p : Fin n.succ → ℚ) (x : Fin n.succ → ℚ) 
@@ -218,14 +222,18 @@ def quantile_srt (n : ℕ) (α : RiskLevel) (p : Fin n.succ → ℚ) (x : Fin n.
   | Nat.succ n' =>
     if h : p 0 < α.val then 
       let α':= α.val - p 0 
-      let bnd_α : IsRiskLevel α' := by 
-        unfold IsRiskLevel  
-        subst α' 
-        specialize h2 0 
+      have bnd_α : IsRiskLevel α' := by 
+        unfold IsRiskLevel; subst α'; specialize h2 0 
         constructor 
         · grw [←h]; simp 
         · grw [←h2]; simpa using α.2.2 
-      quantile_srt n' ⟨α', bnd_α⟩ (Fin.tail p) (Fin.tail x) (tail_monotone x h1) (fun ω ↦ h2 ω.succ) sorry 
+      have h': α' < 1 ⬝ᵥ (Fin.tail p) := by 
+        unfold Fin.tail; subst α'
+        rw [one_dotProduct] at ⊢ h3
+        calc α.val - p 0 < ∑ i, p i - p 0 := by linarith  
+        _  =  (p 0 + ∑ i : Fin n'.succ, p i.succ) - p 0 := by rw [Fin.sum_univ_succAbove p 0]; simp
+          _ = ∑ i : Fin n'.succ, p i.succ := by ring
+      quantile_srt n' ⟨α', bnd_α⟩ (Fin.tail p) (Fin.tail x) (tail_monotone x h1) (fun ω ↦ h2 ω.succ) h'
     else 
       x 0