ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1234 on D1158: Measure space
Borel-Cantelli lemma
Formulation 0
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $E_0, E_1, E_2, \ldots \in \mathcal{F}$ are each a D1109: Measurable set in $M$
(ii) \begin{equation} \sum_{n \in \mathbb{N}} \mu(E_n) < \infty \end{equation}
Then
(1) \begin{equation} \mu \left( \bigcap_{n = 1}^{\infty} \bigcup_{m = n}^{\infty} E_m \right) = 0 \end{equation}
(2) \begin{equation} \mu(\{ x \in X : \# \{ n \in \mathbb{N} : x \in E_n \} = \infty \}) = 0 \end{equation}
Subresults
R1338: Probabilistic Borel-Cantelli lemma
Proofs
Proof 0
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $E_0, E_1, E_2, \ldots \in \mathcal{F}$ are each a D1109: Measurable set in $M$
(ii) \begin{equation} \sum_{n \in \mathbb{N}} \mu(E_n) < \infty \end{equation}
Applying results
(i) R2369: Expressing a countably infinite pointwise sum of indicator functions in terms of set cardinality
(ii) R1242: Unsigned basic integral is compatible with measure
(iii) R1232: Tonelli's theorem for sums and integrals

we have \begin{equation} \begin{split} \int_X \# \{ n \in \mathbb{N} : x \in E_n \} \, \mu(d x) & = \int_X \sum_{n \in \mathbb{N}} I_{E_n}(x) \, \mu(d x) \\ & = \sum_{n \in \mathbb{N}} \int_X I_{E_n}(x) \, \mu(d x) = \sum_{n \in \mathbb{N}} \mu(E_n) \end{split} \end{equation} Since the function $x \mapsto \# \{ n \in \mathbb{N} : x \in E_n \}$ is thus integrable on $M$, then result R1237: Unsigned basic Borel function almost everywhere finite if integral is finite states that $\# \{ n \in \mathbb{N} : x \in E_n \} < \infty$ for almost every $x \in X$. That is, the set $\{ n \in \mathbb{N} : x \in E_n \}$ is finite for almost every $x \in X$. Conversely, the set $\{ n \in \mathbb{N} : x \in E_n \}$ is nonfinite only on a set of measure zero so that we have \begin{equation} \mu(\{ x \in X : \# \{ n \in \mathbb{N} : x \in E_n \} = \infty \}) = 0 \end{equation} We can now use R2371: Equivalent characterisations of membership in a limit superior for sequences of sets to connect the two claims so that we have \begin{equation} \mu \left( \bigcap_{n = 1}^{\infty} \bigcup_{m = n}^{\infty} E_m \right) = \mu(\{ x \in X : \# \{ n \in \mathbb{N} : x \in E_n \} = \infty \}) = 0 \end{equation} $\square$
Proof 1
Let $M = (X, \mathcal{F}, \mu)$ be a D1158: Measure space such that
(i) $E_0, E_1, E_2, \ldots \in \mathcal{F}$ are each a D1109: Measurable set in $M$
(ii) \begin{equation} \sum_{n \in \mathbb{N}} \mu(E_n) < \infty \end{equation}
Fix $N \in \mathbb{N}$. Result R1130: Intersection is largest lower bound yields the inclusion \begin{equation} \bigcap_{n = 0}^{\infty} \bigcup_{m = n}^{\infty} E_m \subseteq \bigcup_{m = N}^{\infty} E_m \end{equation} Applying now the results
(i) R975: Isotonicity of unsigned basic measure
(ii) R979: Countable subadditivity of measure
(iii) R2933: Isotonicity of countably infinite real summation

we have the inequalities \begin{equation} \mu \left( \bigcap_{n = 0}^{\infty} \bigcup_{m = n}^{\infty} E_m \right) \leq \mu \left( \bigcup_{m = N}^{\infty} E_m \right) \leq \sum_{m = N}^{\infty} \mu(E_m) \leq \sum_{m = 0}^{\infty} \mu(E_m) < \infty \end{equation} Since $\sum_{m = 0}^{\infty} \mu(E_m) < \infty$, then we can apply result R4488: Tails of convergent unsigned basic real series converge to zero to establish the limit \begin{equation} \lim_{N \to \infty} \sum_{m = N}^{\infty} \mu(E_m) = 0 \end{equation} Since $\mu \geq 0$ then this, the above bound, and result R1096: Squeeze theorem for basic sequences imply \begin{equation} \mu \left( \bigcap_{n = 0}^{\infty} \bigcup_{m = n}^{\infty} E_m \right) = 0 \end{equation} Finally, we can use R2371: Equivalent characterisations of membership in a limit superior for sequences of sets to connect the two claims as follows \begin{equation} \mu \left( \bigcap_{n = 1}^{\infty} \bigcup_{m = n}^{\infty} E_m \right) = \mu(\{ x \in X : \# \{ n \in \mathbb{N} : x \in E_n \} = \infty \}) = 0 \end{equation} $\square$