[affeldt-aist]

Motivation for this change

generalize expectation to extended real-valued RVs

gen finite_form

motivated by PR #2116

Checklist

• appended entries in the relevant sections of CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are likely to be merged as they are into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[hoheinzollern]

I understand the need to generalize expectation to extended real-valued random variables, but shouldn't there be notations for handling the real case, like for the integral? The composition EFin \o f could be automatically handled by the scope.

[Yosuke-Ito-345]

This generalization is fine with me. I added some minor comments.

In step with this generalization, should I change the codomain of X from R to \bar R in the definition of cdf?

Definition cdf d (T : measurableType d) (R : realType) (P : probability T R)
  (X : {RV P >-> R}) (r : R) := distribution P X `]-oo, r].

This is also the case with ccdf, and maybe with pmf, too. I will create an issue if needed.

[affeldt-aist]

I understand the need to generalize expectation to extended real-valued random variables, but shouldn't there be notations for handling the real case, like for the integral? The composition EFin \o f could be automatically handled by the scope.

Note that in the case of the integral there is a new definition (Rintegral) and many lemmas are "duplicated". If you were to use only a notation to hide EFin ¥o f, it could be fragile (unstable because it could reduce upon conversion).

[affeldt-aist]

Thanks for the comments.

Regarding the type of cdf, ccdf, and pmf: we didn't feed the need to generalize yet (in the PR #2116).

[affeldt-aist]

by the way @Yosuke-Ito-345 @hoheinzollern you might be interested in providing input to #2116 in which @lyonel2017 put much effort