I care to understand the concept behind the Borel-Cantelli Lemma better, hence I would appreciate it if someone could take the time to check if my arguments below are clear and rigorous.
Statement: Let $(X_n)_{n \geq 1}$ be a sequence of non-negative random variables that are identically distributed $X_n \sim X \geq 0 $ with $E(X)< \infty$, show that $ X_n/n \to 0$ almost surely
Proof: Since $X_n \sim X$ for some non negative random variables we can easily compute that for $\epsilon >0$ we have $$ \infty>E(X/\epsilon) = \int_0^\infty P(X/ \epsilon > t) dt = \sum_{n=1}^\infty \int_{n-1}^n P(X/ \epsilon > t ) dt \geq \sum_{n=1}^{\infty} P(X/ \epsilon >n) $$ Thanks to the Borel-Cantelli Lemma we obtain that $$ P ( \limsup_{n \to \infty} \lbrace X_n/n > \epsilon \rbrace ) = 0 \iff P ( \liminf_{n \to \infty} \lbrace X_n/n \leq \epsilon \rbrace) = 1 $$
Question: Does the $\epsilon$ in the above depend on $k$?
I think it does and I would argue as follows $$P( \liminf_{n \to \infty} \lbrace X_n/n \leq \epsilon \rbrace )= P \left( \bigcup_{n=0}^\infty \bigcap_{k=n} \lbrace X_k/k \leq \epsilon (k) \rbrace \right) $$ Now using the chain of inclusions that state that we have for $\epsilon >0$ $$ \lbrace \limsup |X_n-X| < \epsilon \rbrace \subset \liminf \lbrace |X_n-X| < \epsilon \rbrace \subset \lbrace \limsup |X_n-X| \leq \epsilon \rbrace $$ We conclude that $$ P ( \lbrace \limsup_{n \to \infty } X_n/ n \leq \epsilon(k) \rbrace)=1 $$ Where I choose the same $k \in \mathbb{N}$ as above, and then choose $k^*$ large enough such that $\epsilon(k) \leq \frac{1}{k^*}$, define the set $$ \Lambda_{k^*}:= \lbrace \limsup_{n \to \infty} X_n/n \leq 1/k^* \rbrace \implies P(\Lambda_{k^*})=1$$ and also we obtain that $\Lambda:=\bigcap_{j \geq k^*} \Lambda_{k^*}$ is still an almost sure event, i.e. $P(\Lambda)=1$ but for all realizations $\omega \in \Lambda$ we have $\limsup_{n \to \infty} X_n( \omega)/n \leq 0 \implies X_n( \omega)/n \to 0$ for all $\omega \in \Lambda$ that is$X_n/n \to 0$ almost surely $\Box$
Are my arguments given above correct and more importantly complete? Are there steps where you'd use different arguments?