Conditional variance

Stream: Is there code for X?

[Yaël Dillies]

I'm looking for the conditional variance of a random variable according to a sigma-subalgebra. Searching through mathlib, I notice that in fact we don't have the usual variance of a non-real-valued random variable. Indeed, docs#ProbabilityTheory.variance only works for X : Ω → ℝ.

[Rémy Degenne]

That's correct: we don't have a specific definition for the conditional variance (but it's not hard to define with existing tools), and we have only variance of real random variables.

[Yaël Dillies]

I'm somewhat confused as to why we only have variance of real-valued random variables. The definition straightforwardly generalises to a normed space-valued random variable. Am I missing something? Was this simplification done for usability? (eg to use X ^ 2 instead of fun ω ↦ ‖X ω‖ ^ 2). Was this an oversight?

[Rémy Degenne]

In R^n the useful object is the covariance matrix and the matrix you get for cov(X,X) is sometimes called variance, and then there are several notions of real valued variance used in different places: trace of the covariance matrix (what you get with your def) or determinant of that matrix.

[Rémy Degenne]

It's not absolutely clear that your generalization should be the one with name variance.

[Yaël Dillies]

Okay I see. Wouldn't it be fine to do this generalisation anyway, since it has the same type as the variance of a real-valued random variable, and add a disclaimer that there are other kinds of variances?

[Kexing Ying]

I think it would be better just to define covariance directly instead of generalizing variance to non-real valued RVs.

[Kexing Ying]

There was a small discussion about this here