LOTUS needlessly assumes function is differentiable for proof

[Tokarak]

https://statproofbook.github.io/P/mean-lotus

• the proof unnecessary regularity conditions on g(x): differentiability and monotonicity. g can be an arbitrary real-valued measurable function. Surely this also mean that the current proof is more complex than it needs to be?
• The proof needlessly assume that X is a real random variable that is either discrete or continuous. X can be any measurable random variable taking values in an arbitrary measurable space.

[JoramSoch]

Dear @Tokarak, thanks for your comments! I think there are two points:

1. differentiability and monotonicity: The monotonicity condition is actually used in the proof for the discrete case (see after eq. 4) and the differentiability condition is used in the proof for the continuous case (see eq. 6). One could be more precise here and say that the discrete case requires monotonicity while the continuous case requires differentiability (and invertibility?). Or simply say that g(X) should be invertible and differentiable. Actually, these conditions should rather go into the Theorem.

2. measurable random variable: This probably points to a much bigger problem, namely that there is currently no satisfying treatment of measure theory in the StatProofBook. For example, a random variable is formally defined as "as a measurable function defined on a probability space that maps from a sample space to the real numbers"; but throughout e.g. Chapter I, this term is used informally in the sense of a "real number whose value is the outcome of a random experiment". So yes, we can use the terminology of "measurable RV", "measurable space" and "measurable function" (all of which are currently undefined!), but this would need a new section on "Measure theory" (which would be the new first section of Chapter I).

What do you think?

[JoramSoch]

One could be more precise here and say that the discrete case requires monotonicity while the continuous case requires differentiability (and invertibility?). Or simply say that g(X) should be invertible and differentiable. Actually, these conditions should rather go into the Theorem.

resolved with commit 2c35dbf