This is a bit on the elementary side, but I'm having trouble understanding if the following formula is a definition, or a derivation.
Given that $E[X] = \sum\limits_x xp(x)$, and $g(X)$ is some real-valued function, then $E[g(X)] = \sum\limits_xg(x)p(x)$.
From an intuitive standpoint, this makes perfect sense. Finding the expected value of a function of $X$ is fundamentally no different than finding the expectation for $X$ itself, as the expectation is just the theoretical average of all possible values of $g$.
But is this something that
- we define explicitly,
- follows directly from the definition of $E[X]$, or
- something that can be proven to follow from the formula for $E[X]$?
The reason I ask is that I understand $E[X]$ and $E[g(X)]$ in isolation, but I'm having trouble determining if the bridge between them is mathematically provable, or if the latter is just an "obvious" definition.
It also seems that most proofs for properties of expectation (such as linearity; $E[aX + b] = aE[X] +b$) begins with the knowledge that $E[g(X)] = \sum\limits_xg(x)p(x)$ so it's pretty fundamental.