Processing math: 100%
ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1234 on D1158: Measure space
Borel-Cantelli lemma
Formulation 0
Let M=(X,F,μ) be a D1158: Measure space such that
(i) E0,E1,E2,F are each a D1109: Measurable set in M
(ii) nNμ(En)<
Then
(1) μ(n=1m=nEm)=0
(2) μ({xX:#{nN:xEn}=})=0
Subresults
R1338: Probabilistic Borel-Cantelli lemma
Proofs
Proof 0
Let M=(X,F,μ) be a D1158: Measure space such that
(i) E0,E1,E2,F are each a D1109: Measurable set in M
(ii) nNμ(En)<
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 X#{nN:xEn}μ(dx)=XnNIEn(x)μ(dx)=nNXIEn(x)μ(dx)=nNμ(En) Since the function x#{nN:xEn} is thus integrable on M, then result R1237: Unsigned basic Borel function almost everywhere finite if integral is finite states that #{nN:xEn}< for almost every xX. That is, the set {nN:xEn} is finite for almost every xX. Conversely, the set {nN:xEn} is nonfinite only on a set of measure zero so that we have μ({xX:#{nN:xEn}=})=0 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 μ(n=1m=nEm)=μ({xX:#{nN:xEn}=})=0
Proof 1
Let M=(X,F,μ) be a D1158: Measure space such that
(i) E0,E1,E2,F are each a D1109: Measurable set in M
(ii) nNμ(En)<
Fix NN. Result R1130: Intersection is largest lower bound yields the inclusion n=0m=nEmm=NEm 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 μ(n=0m=nEm)μ(m=NEm)m=Nμ(Em)m=0μ(Em)< Since m=0μ(Em)<, then we can apply result R4488: Tails of convergent unsigned basic real series converge to zero to establish the limit limNm=Nμ(Em)=0 Since μ0 then this, the above bound, and result R1096: Squeeze theorem for basic sequences imply μ(n=0m=nEm)=0 Finally, we can use R2371: Equivalent characterisations of membership in a limit superior for sequences of sets to connect the two claims as follows μ(n=1m=nEm)=μ({xX:#{nN:xEn}=})=0