Merge branch 'lotus'

Author: marekpetrik

Probability/MDP/Risk.lean

@@ -0,0 +1,78 @@
+import Probability.Probability.Basic
+
+namespace Risk
+
+open Findist FinRV
+
+variable {n : ℕ}
+
+def cdf (P : Findist n) (X : FinRV n ℚ) (t : ℚ) : ℚ := ℙ[X ≤ᵣ t // P]
+
+/-- Finite set of values taken by a random variable X : Fin n → ℚ. -/
+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
+    S.min' h
+  else
+    0
+
+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 X t ≤ cdf P Y t := by
+    intro t
+    have h_ind : (𝕀 ∘ (Y ≤ᵣ t)) ≤ (𝕀 ∘ (X ≤ᵣ t)) := by
+      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]
+    simp [cdf]
+
+    sorry
+  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
+
+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

Probability/Probability/Defs.lean

@@ -3,7 +3,7 @@ import Probability.Probability.Prelude
 import Mathlib.Data.Matrix.Mul  -- dot product definitions and results
 import Mathlib.Algebra.Notation.Pi.Defs -- operations on functions
 import Mathlib.Algebra.Module.PointwisePi -- for smul_pi
-import Mathlib.LinearAlgebra.Matrix.DotProduct -- for monotonicity 
+import Mathlib.LinearAlgebra.Matrix.DotProduct -- for monotonicity
 
 --------------------------- Findist ---------------------------------------------------------------
 
@@ -14,7 +14,7 @@ variable {n : ℕ}
 structure Findist (n : ℕ) : Type where
     p : Fin n → ℚ
     prob : 1 ⬝ᵥ p = 1
-    nneg : 0 ≤ p 
+    nneg : 0 ≤ p
 
 namespace Findist
 
@@ -29,12 +29,12 @@ def singleton : Findist 1 :=
 
 
 @[simp]
-def length (_ : Findist n) := n 
+def length (_ : Findist n) := n
 
-variable {n : ℕ} 
+variable {n : ℕ}
 
-theorem nonempty (P : Findist n) : P.length > 0 := 
-  by cases n 
+theorem nonempty (P : Findist n) : P.length > 0 :=
+  by cases n
      · have := P.prob; simp_all only [Matrix.dotProduct_of_isEmpty, zero_ne_one]
      · simp only [length, gt_iff_lt, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true]
 
@@ -50,7 +50,7 @@ end Findist
 --------------------------- Random Variable -------------------------------------------------------------------
 
 /-!
-Random variables are defined as function. The operations on random variables can be performed 
+Random variables are defined as function. The operations on random variables can be performed
 using the standard notation:
 
 - X + Y is elementwise addition
@@ -60,12 +60,12 @@ using the standard notation:
 
 
 - L =ᵣ i is a boolean indicator random variable
-- L =ᵢ i is a ℚ indicator random variable 
-- L ≤ᵣ i is a bool indicator random variable 
+- L =ᵢ i is a ℚ indicator random variable
+- L ≤ᵣ i is a bool indicator random variable
 
-Main results 
+Main results
 
-- Hadamard product is linear:  Y * (∑ i, Xs i) = ∑ i, Y * (Xs i) 
+- Hadamard product is linear:  Y * (∑ i, Xs i) = ∑ i, Y * (Xs i)
 -/
 
 
@@ -133,6 +133,12 @@ def leq [LE ρ] [DecidableLE ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
 
 infix:50 "≤ᵣ" => FinRV.leq
 
+@[simp]
+def gt [LT ρ] [DecidableLT ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
+  fun ω ↦ Y ω > y
+
+infix:50 ">ᵣ" => FinRV.gt
+
 example (m n : ℕ) : (m < n) ∨ (m = n) ∨ (m > n) :=  Nat.lt_trichotomy m n
 
 /-- Shows equivalence when extending the random variable to another element. -/
@@ -158,16 +164,16 @@ abbrev 𝕀 [OfNat ρ 0] [OfNat ρ 1] : Bool → ρ := indicator
 
 variable {k : ℕ} {L : FinRV n (Fin k)}
 
-theorem indi_eq_indr : ∀i : Fin k, (𝕀 ∘ (L =ᵣ i)) = (L =ᵢ i) := by 
-  intro i 
-  unfold FinRV.eq FinRV.eqi 𝕀 indicator 
-  ext ω 
-  by_cases h: L ω = i 
+theorem indi_eq_indr : ∀i : Fin k, (𝕀 ∘ (L =ᵣ i)) = (L =ᵢ i) := by
+  intro i
+  unfold FinRV.eq FinRV.eqi 𝕀 indicator
+  ext ω
+  by_cases h: L ω = i
   · simp [h]
   · simp [h]
 
 
-variable {B : FinRV n Bool} 
+variable {B : FinRV n Bool}
 /-- Indicator is 0 or 1 -/
 theorem ind_zero_one  :  ∀ ω, (𝕀∘B) ω = 1 ∨ (𝕀∘B) ω = 0 := by
     intro ω
@@ -176,40 +182,40 @@ theorem ind_zero_one  :  ∀ ω, (𝕀∘B) ω = 1 ∨ (𝕀∘B) ω = 0 := by
     · right; simp only [Function.comp_apply, h, indicator]
 
 /-- Indicator is 0 or 1 -/
-theorem ind_nneg : (0 : FinRV n ℚ) ≤ 𝕀∘B := by 
+theorem ind_nneg : (0 : FinRV n ℚ) ≤ 𝕀∘B := by
     intro ω
     simp [𝕀, indicator]
     by_cases h : B ω
-    · simp [h] 
-    · simp [h]   
+    · simp [h]
+    · simp [h]
 
-theorem ind_le_one : 𝕀∘B ≤ (1 : FinRV n ℚ) := 
+theorem ind_le_one : 𝕀∘B ≤ (1 : FinRV n ℚ) :=
     by unfold 𝕀 indicator
        intro ω
        by_cases h : B ω
        · simp [h]
-       · simp [h]  
+       · simp [h]
 
 theorem one_of_true : 𝕀 ∘ (1 : Fin n → Bool) = (1 : Fin n → ℚ) := by ext; simp [𝕀, indicator]
 
-theorem one_of_bool_or_not : B + (¬ᵣ B) = (1 : FinRV n Bool) := by ext ω; unfold FinRV.not; simp 
+theorem one_of_bool_or_not : B + (¬ᵣ B) = (1 : FinRV n Bool) := by ext ω; unfold FinRV.not; simp
 
-theorem one_of_ind_bool_or_not : (𝕀∘B) + (𝕀∘(¬ᵣ B)) = (1 : FinRV n ℚ) := 
+theorem one_of_ind_bool_or_not : (𝕀∘B) + (𝕀∘(¬ᵣ B)) = (1 : FinRV n ℚ) :=
     by ext ω
-       unfold FinRV.not 𝕀 indicator not 
+       unfold FinRV.not 𝕀 indicator not
        by_cases h : B ω
        · simp [h]
-       · simp [h]  
+       · simp [h]
 
-variable {X Y: FinRV n ℚ} 
+variable {X Y: FinRV n ℚ}
 
 theorem rv_le_abs : X ≤ abs ∘ X := by intro i; simp [le_abs_self (X i)]
 
-theorem rv_prod_sum_linear {Xs : Fin k → FinRV n ℚ} : ∑ i, Y * (Xs i) = Y * (∑ i, Xs i) := 
-    by ext ω 
-       simp 
-       rw [Finset.mul_sum] 
-        
+theorem rv_prod_sum_linear {Xs : Fin k → FinRV n ℚ} : ∑ i, Y * (Xs i) = Y * (∑ i, Xs i) :=
+    by ext ω
+       simp
+       rw [Finset.mul_sum]
+
 end RandomVariable
 
 ------------------------------ Probability ---------------------------
@@ -222,7 +228,7 @@ def probability : ℚ :=  P.p ⬝ᵥ (𝕀 ∘ B)
 
 notation "ℙ[" B "//" P "]" => probability P B
 
--- helps to refold is when needed 
+-- helps to refold is when needed
 lemma probability_def : P.p ⬝ᵥ (𝕀 ∘ B) = ℙ[B // P] := rfl
 
 -- TODO: the sorry in the definition has to do with the decidability of the membership
@@ -244,11 +250,11 @@ theorem prob_one_of_true : ℙ[1 // P] = 1 :=
 
 example {a b : ℚ} (h : 0 ≤ a) (h2 : 0 ≤ b) : 0 ≤ a * b :=  Rat.mul_nonneg h h2
 
-variable {P : Findist n} {B : FinRV n Bool} 
+variable {P : Findist n} {B : FinRV n Bool}
+
+theorem prod_zero_of_prob_zero : ℙ[B // P] = 0 → (P.p * (𝕀∘B) = 0) := by
+    intro h; exact prod_eq_zero_of_nneg_dp_zero P.nneg ind_nneg h
 
-theorem prod_zero_of_prob_zero : ℙ[B // P] = 0 → (P.p * (𝕀∘B) = 0) := by 
-    intro h; exact prod_eq_zero_of_nneg_dp_zero P.nneg ind_nneg h 
-  
 
 ------------------------------ PMF ---------------------------
 
@@ -278,7 +284,7 @@ notation "𝔼[" PX "]" => expect PX.1 PX.2
 --theorem exp_eq_correct : 𝔼[X // P] = ∑ v ∈ ((List.finRange P.length).map X).toFinset, v * ℙ[ X =ᵣ v // P]
 
 @[simp]
-theorem prob_eq_exp_ind : ℙ[B // P] = 𝔼[𝕀 ∘ B // P] := 
+theorem prob_eq_exp_ind : ℙ[B // P] = 𝔼[𝕀 ∘ B // P] :=
     by simp only [expect, probability]
 
 
@@ -298,47 +304,47 @@ def expect_cnd_rv : Fin n → ℚ := fun i ↦ 𝔼[ X | L =ᵣ (L i) // P ]
 notation "𝔼[" X "|ᵣ" L "//" P "]" => expect_cnd_rv P X L
 
 end Ex
---- some basic properties 
+--- some basic properties
 
-section Expectation_properties 
+section Expectation_properties
 variable {P : Findist n} {X Y Z: FinRV n ℚ} {B : FinRV n Bool}
 
-theorem exp_congr : (X = Y) → 𝔼[X // P] = 𝔼[Y // P] := 
-  by intro h 
-     unfold Ex.expect dotProduct 
+theorem exp_congr : (X = Y) → 𝔼[X // P] = 𝔼[Y // P] :=
+  by intro h
+     unfold Ex.expect dotProduct
      apply Fintype.sum_congr
-     simp_all 
+     simp_all
 
-theorem exp_dists_add : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := by simp [Ex.expect] 
+theorem exp_dists_add : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := by simp [Ex.expect]
 
 theorem exp_mul_comm : 𝔼[X * Y // P] = 𝔼[Y * X // P] := by unfold Ex.expect; exact dotProd_hadProd_comm
 
 variable {c : ℚ} {p : Fin n → ℚ}
 
-theorem const_fun_to_one : (fun _ ↦ c : FinRV n ℚ)  = c • 1 := by ext; simp; 
+theorem const_fun_to_one : (fun _ ↦ c : FinRV n ℚ)  = c • 1 := by ext; simp;
 
-theorem exp_const : 𝔼[(fun _ ↦ c) // P] = c := 
+theorem exp_const : 𝔼[(fun _ ↦ c) // P] = c :=
     by unfold Ex.expect
-       rw [const_fun_to_one] 
+       rw [const_fun_to_one]
        simp only [dotProduct_smul, smul_eq_mul]
        rw [dotProduct_comm, P.prob]
-       simp 
+       simp
 
-theorem exp_one : 𝔼[ 1 // P] = 1 := 
-    by calc 𝔼[ 1 // P] = 𝔼[ (fun _ ↦ 1) // P] := rfl 
-       _ = 1 := exp_const    
+theorem exp_one : 𝔼[ 1 // P] = 1 :=
+    by calc 𝔼[ 1 // P] = 𝔼[ (fun _ ↦ 1) // P] := rfl
+       _ = 1 := exp_const
 
 theorem exp_prod_const : 𝔼[c • X // P] = c * 𝔼[X // P] := by simp only [Ex.expect, dotProduct_smul, smul_eq_mul]
 
-lemma constant_mul_eq_smul : (fun ω ↦ c * X ω) = c • X := rfl 
+lemma constant_mul_eq_smul : (fun ω ↦ c * X ω) = c • X := rfl
 
-theorem exp_prod_const_fun : 𝔼[(λ _ ↦ c) * X // P] = c * 𝔼[X // P] := 
+theorem exp_prod_const_fun : 𝔼[(λ _ ↦ c) * X // P] = c * 𝔼[X // P] :=
   by simp only [Ex.expect, Pi.mul_def, constant_mul_eq_smul, dotProduct_smul, smul_eq_mul]
 
-theorem exp_indi_eq_exp_indr : ∀i : Fin k, 𝔼[L =ᵢ i // P] = 𝔼[𝕀 ∘ (L =ᵣ i) // P] := by 
-  intro i 
+theorem exp_indi_eq_exp_indr : ∀i : Fin k, 𝔼[L =ᵢ i // P] = 𝔼[𝕀 ∘ (L =ᵣ i) // P] := by
+  intro i
   rw [indi_eq_indr]
 
 theorem exp_monotone (h: X ≤ Y)  : 𝔼[X // P] ≤ 𝔼[Y // P] :=  dotProduct_le_dotProduct_of_nonneg_left h P.nneg
 
-end Expectation_properties 
+end Expectation_properties