VaR definition: inf (reals) or min support? --opinions needed

[emily-chandran]

Currently we have this as our VaR definition:
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 --this is illegal i know -- Keith is going to fix it :)

But I'm not sure if we want to keep it like this, or if we want to do this instead:
def VaR (P : Findist n) (X : FinRV n ℝ) (α : ℝ) : ℝ :=
sInf { t : ℝ | cdf P X t ≥ α }

The advantage of the first one is that the r.v.s are in terms of ℚ, but seems more difficult to prove theorems about.

For example, I'm working on the monotonicity proof for VaR and I'm having trouble because the minimization is over the rangeOfRV X, so it’s not always true that VaR Y is in the rangeOfRV X, even if X ≤ Y. I do think I can figure out how to get around this to finish the proof but it would be a lot easier if we were using the inf definition. But then we would need to redefine some things in terms of ℝ which creates other issues.

Before we get too far into the VaR proofs, I wanted to know if anyone had some intuition about which definition might be better for us in the long run!

[marekpetrik]

My thoughts: Lets try to go with both and use the one it is easier to prove things about. Even if we cannot compute it initially, we can then show that the easy-to-prove-with definition is equal to the one that is computable.

However, if we can, it may be easier to avoid definitions that involve inf and sup and use max and min if possible. Proving with Inf and Sup can be quite clunky. At the risk of stating something obvious, inf and sup require R because Q is not complete (https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers#Least_upper_bound_property) and sup and inf may not exist.

Perhaps, it is easier to start with showing the monotonicity property for CDF and then show it for VaR from it. In particular,
[Follmer, H. and Schied, A. (2016) Stochastic finance: introduction in discrete time. 4th ed. De Gruyter Graduate.]
describe VaR as a left/right-continuous inverse of the CDF. Some of these concepts may already be defined in Mathlib.

I will email the relevant parts of Follmer and Schied.