def Risk.IsRiskLevel (α : ℚ) : Prop

Equations

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

def Risk.RiskLevel : Type

Equations

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

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

Equations

• Risk.FinVaRSet P X α = {t ∈ Finset.image X Finset.univ | ℙ[X<ᵣt//P] ≤ ↑α}

theorem Risk.FinVarSet_nonempty {n : ℕ} (P : Findist n) (X : FinRV n ℚ) (α : RiskLevel) : (FinVaRSet P X α).Nonempty

def Risk.FinVaR {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.finvar_prob_lt_var_le_alpha {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : ℙ[X<ᵣVaR[X//P, α]//P] ≤ ↑α

theorem Risk.finvar_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_Q {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_Q P X α v = IsGreatest (Statistic.Quantile P X ↑α) v

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

A simpler, equivalent definition of Value at Risk

Equations

• Risk.IsVaR P X α v = IsGreatest (Statistic.QuantileLower 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.finvar_correct {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} : IsVaR P X α VaR[X//P, α]

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

theorem Risk.varq_is_quantilelower {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR_Q P X α v → Statistic.IsQuantileLower 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.var_is_quantile {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR 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.varq_eq_var {n : ℕ} {P : Findist n} {X : FinRV n ℚ} {α : RiskLevel} {v : ℚ} : IsVaR_Q P X α v ↔ IsVaR P X α v

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

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

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

theorem Risk.isvar_translation_invariant {n : ℕ} {v : ℚ} {P : Findist n} {X : FinRV n ℚ} {c : ℚ} {α : RiskLevel} : IsVaR P X α v → IsVaR 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, α]