VaR Monotone work -- NOT ready to be merged!

Probability/MDP/Risk.lean

@@ -1,4 +1,6 @@
 import Probability.Probability.Basic
+import Mathlib.Data.EReal.Basic 
+import Mathlib.Data.Set.Operations
 
 namespace Risk
 
@@ -8,80 +10,239 @@ variable {n : ℕ}
 
 def cdf (P : Findist n) (X : FinRV n ℚ) (t : ℚ) : ℚ := ℙ[X ≤ᵣ t // P]
 
+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
+
+
+/-- 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)
+
 /-- 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
+    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
+-- 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
-  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
+  (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
+    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
+
+
+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
+
+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 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
+
+
+
+theorem VaR_caleb_monotone (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ)
+  (hXY : X ≤ Y) : VaR_caleb P X α ≤ VaR_caleb 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 ---------------------------
+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
+    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 ℝ) (α : ℝ) : ℝ :=
+  sInf { t : ℝ | cdfR P X t ≥ α }
+
+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 ≥ α }
+  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
+      unfold cdfR
+      --apply exp_monotone
+
+      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
 
 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 =  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 
+end Risk
 
-notation "CVaR[" α "," X "//" P "]" => CVaR P X α
+--- ************************* Another approach (Marek) ****************************************************
 
---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]
+section Risk2
 
+#check Set.preimage
+#synth SupSet EReal 
+#synth SupSet (WithTop ℝ)
+#check instSupSetEReal
+#check WithTop.instSupSet
 
-end Risk
+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 
+  simp 
+  grind  
+
+
+theorem prob_le_compl_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P]= 1 := by 
+  sorry
+  --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-α
+
+/-- 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 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 
+
+
+-- 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
+
+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 
+    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 
+      have bnd_α : IsRiskLevel α' := by 
+        unfold IsRiskLevel; subst α'; specialize h2 0 
+        constructor 
+        · grw [←h]; simp 
+        · grw [←h2]; simpa using α.2.2 
+      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 
+
+
+def FinVaR (α : RiskLevel) (P : Findist n) (X : FinRV n ℚ) : ℚ := 
+    match n with 
+    | 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 
+
+end Risk2

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 -- for Equiv.Perm and permutation operations
+
+
 /-!
   # 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
 
 
@@ -32,12 +35,27 @@ 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} {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]
+    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] :=
@@ -93,4 +111,47 @@ 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 ℚ} {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 σ)
+
+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_eq_perm : 𝔼[X ∘ σ // P.perm σ] = 𝔼[X // P] := by
+  unfold expect Findist.perm 
+  exact (comp_equiv_dotProduct_comp_equiv P.1 X σ)
+
+theorem prob_eq_perm : ℙ[A ∘ σ // P.perm σ] = ℙ[A // P] := by 
+  have h1 : (𝕀 ∘ A ∘ σ) = (𝕀 ∘ A) ∘ σ := by rfl 
+  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