Let $X$ be a random variable with finite variance. I know that this implies a finite mean.
Do I have to prove that or does it follow from the definition of the variance?
The variance is defined as $V[X] =E[(X−E[X])^2]$
If the mean $E[X]$ would not exist, the variance would be undefined. Thus no finite variance without a defined mean.
If the mean $E[X]$ would be infinite, it could still be the case that $E[(X−E[X])^2]$ is finite, I would have to prove that it is not.
Mathematicians, how do you use "infinite" and "does not exist" interchangeably?
Note in this question, comments say "follows from the definition", while answer says "use Cauchy Schwarz", so I am not the only one who is confused.
Infinite mean and mean not existing are not one and the same. $X$ has mean $\infty$ if $EX^{+}=\infty$ and $EX^{-}<\infty$. Mean of $X$ dose not exist if $EX^{+}=\infty$ and $EX^{-}=\infty$ in which case you cannot assign any value, finite of infinite, to $EX$.
We can say the following: if $EX$ exists (finite or infinite) and $E(X-EX)^{2} <\infty$ then $EX$ is finite. [$E(X-EX)^{2} <\infty$ implies $X-EX$ is finite almost surely. Since $X$ has finite values this implies $EX$ is finite]. If $EX$ is not even defined we just cannot talk about variance of $X$.