def Risk.IsRiskLevel (α : ℚ) : Prop

Equations

• Risk.IsRiskLevel α = (0 ≤ α ∧ α < 1)

def Risk.RiskLevel : Type

Equations

• Risk.RiskLevel = { α : ℚ // Risk.IsRiskLevel α }

def Risk.FinVaR1 {n : ℕ} (P : Findist n) (X : FinRV n ℚ) (α : RiskLevel) : ℚ

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.

Equations

• VaR[X//P, α] = {t ∈ Finset.image X Finset.univ | ℙ[X<ᵣt//P] ≤ ↑α}.max' ⋯

theorem Risk.var1_prob_lt_var_le_alpha {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : ℙ[X<ᵣVaR[X//P, α]//P] ≤ ↑α

theorem Risk.var1_prob_le_var_gt_alpha {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : ℙ[X≤ᵣVaR[X//P, α]//P] > ↑α

def Risk.«termVaR[_//_,_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Risk.IsVaR {n : ℕ} (P : Findist n) (X : FinRV n ℚ) (α : RiskLevel) (v : ℚ) : Prop

Value v is the Value at Risk at α of X and probability P

Equations

• Risk.IsVaR P X α v = IsGreatest (Statistic.Quantile P X ↑α) v

def Risk.IsVaR2 {n : ℕ} (P : Findist n) (X : FinRV n ℚ) (α : RiskLevel) (v : ℚ) : Prop

A simpler, equivalent definition of Value at Risk

Equations

• Risk.IsVaR2 P X α v = IsGreatest (Statistic.QuantileLower P X ↑α) v

theorem Risk.var2_prob_cond {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR2 P X α v ↔ ℙ[X<ᵣv//P] ≤ ↑α ∧ ↑α < ℙ[X≤ᵣv//P]

theorem Risk.finvar1_correct {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : IsVaR2 P X α VaR[X//P, α]

theorem Risk.var_is_quantile {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR P X α v → Statistic.IsQuantile P X (↑α) v

theorem Risk.var_is_quantilelower {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR P X α v → Statistic.IsQuantileLower P X (↑α) v

theorem Risk.var2_is_quantilelower {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR2 P X α v → Statistic.IsQuantileLower P X (↑α) v

theorem Risk.var2_is_quantile {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR2 P X α v → Statistic.IsQuantile P X (↑α) v

theorem Risk.quantile_nonempty {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : (Statistic.Quantile P X ↑α).Nonempty

theorem Risk.isquantilelower_le_isquantile {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : IsCofinalFor (Statistic.QuantileLower P X ↑α) (Statistic.Quantile P X ↑α)

theorem Risk.isquantile_le_isquantilelower {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : IsCofinalFor (Statistic.Quantile P X ↑α) (Statistic.QuantileLower P X ↑α)

theorem Risk.var_eq_var2 {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR P X α v ↔ IsVaR2 P X α v

theorem Risk.var_prob_cond {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR P X α v ↔ ℙ[X<ᵣv//P] ≤ ↑α ∧ ↑α < ℙ[X≤ᵣv//P]

theorem Risk.tail_monotone {n : ℕ} (X : Fin n.succ → ℚ) (h : Monotone X) : Monotone (Fin.tail X)

def Risk.quantile_srt (n : ℕ) (α : RiskLevel) (p x : Fin n.succ → ℚ) (h1 : Monotone x) (h2 : ∀ (ω : Fin n.succ), 0 ≤ p ω) (h3 : ↑α < 1 ⬝ᵥ p) (h4 : 0 < 1 ⬝ᵥ p) : Fin n.succ

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 α

Equations

• One or more equations did not get rendered due to their size.
• Risk.quantile_srt Nat.zero α p_2 x_2 h1_2 h2_2 h3_2 h4_2 = 0

theorem Risk.quant_less (n : ℕ) {k : Fin n.succ} (α : RiskLevel) (p x : Fin n.succ → ℚ) (h1 : Monotone x) (h2 : ∀ (ω : Fin n.succ), 0 ≤ p ω) (h3 : ↑α < 1 ⬝ᵥ p) (h4 : 0 < 1 ⬝ᵥ p) (h5 : k = quantile_srt n α p x h1 h2 h3 h4) : ∑ i ∈ Finset.Ico 0 k, p i ≤ ↑α ∧ ∑ i ∈ Finset.Icc 0 k, p i > ↑α

def Risk.FinVaR {n : ℕ} {P : Findist n} {X Y : FinRV n ℚ} (α : RiskLevel) : Findist n → FinRV n ℚ → ℚ

Equations

• Risk.FinVaR α P_4 X_4 = 0
• Risk.FinVaR α P_4 X_4 = X_4 (Risk.quantile_srt n' α (P_4.p ∘ ⇑(Tuple.sort X_4)) (X_4 ∘ ⇑(Tuple.sort X_4)) ⋯ ⋯ ⋯ ⋯)

theorem Risk.var2_monotone {n : ℕ} {P : Findist n} {X Y : FinRV n ℚ} {v₁ v₂ : ℚ} {α : RiskLevel} : X ≤ Y → IsVaR2 P X α v₁ → IsVaR2 P Y α v₂ → v₁ ≤ v₂

theorem Risk.const_monotone_univ {c : ℚ} : Monotone fun (x : ℚ) => x + c

theorem Risk.VaR2_translation_invariant {n : ℕ} {v : ℚ} {P : Findist n} {X : FinRV n ℚ} {c : ℚ} {α : RiskLevel} : IsVaR2 P X α v → IsVaR2 P (X + c • 1) α (v + c)

theorem Risk.VaR_translation_invariant {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {c : ℚ} {α : RiskLevel} : VaR[X + c • 1//P, α] = VaR[X + c • 1//P, α] + c

theorem Risk.VaR_positive_homog {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {c : ℚ} {α : RiskLevel} (hc : c > 0) : VaR[fun (ω : Fin n) => c * X ω//P, α] = c * VaR[X//P, α]