Strong law of large numbers

DefinitionPartial sums of indicators#✓fully proved

For sets \(A_0, A_1, \dots\) in \(\Omega\) and \(n \in \mathbb{N}\), \(S_n = \sum_{i < n} 1_{A_i}\) is the sum of the indicators of the first \(n\) sets, viewed as a real-valued function on \(\Omega\).

def partialSumIndicators (A : ℕ → Set Ω) (n : ℕ) : Ω → ℝ :=
  fun ω => ∑ i ∈ Finset.range n, (A i).indicator (1 : Ω → ℝ) ω

Used by 19

Used byChebyshev bound along the subsequence · Monotonicity of the expected partial sums · The expected partial sums along the subsequence are positive · Upper bound for the expected partial sums along the subsequence · The expected partial sums grow by at most one per step · Ratios of consecutive subsequence expectations tend to one · Divergent total probability makes the expected partial sums diverge · Expectation of a sum of indicators · Partial sums of indicators are square-integrable · Pairwise-independent strong law for indicator sums · The partial sum as a sum of indicator functions · Partial sums of indicators are nondecreasing · Partial sums of indicators are nonnegative · Quadratic subsequence for the pairwise-independent strong law · Indices of the quadratic subsequence are positive · Lower bound on the expected count along the quadratic subsequence · The quadratic subsequence is strictly increasing · Summable deviation probabilities along the quadratic subsequence · Variance of a sum of pairwise independent indicators is at most its mean

LemmaThe partial sum as a sum of indicator functions#✓fully proved

For sets \(A_0, A_1, \dots\) in \(\Omega\) and every \(n\), the partial sum \(S_n\), defined pointwise by \(S_n(\omega) = \sum_{i < n} 1_{A_i}(\omega)\), equals, as a function on \(\Omega\), the sum \(\sum_{i < n} 1_{A_i}\) of the real-valued indicator functions.

lemma partialSumIndicators_eq (A : ℕ → Set Ω) (n : ℕ) :
    partialSumIndicators A n = ∑ i ∈ Finset.range n, (A i).indicator (1 : Ω → ℝ)

Uses 1 · Used by 2

Statement usesPartial sums of indicators

Used byPartial sums of indicators are square-integrable · Variance of a sum of pairwise independent indicators is at most its mean

LemmaThe σ-algebra generated by an indicator function#✓fully proved

For a set \(s \subseteq \Omega\), the σ-algebra on \(\Omega\) generated by the indicator function \(1_s : \Omega \to \mathbb{R}\) (the preimages of Borel sets of \(\mathbb{R}\)) is contained in the σ-algebra generated by \(s\).

lemma comap_indicator_one_le_generateFrom (s : Set Ω) :
    MeasurableSpace.comap (s.indicator (1 : Ω → ℝ)) Real.measurableSpace ≤
    MeasurableSpace.generateFrom {s}

Used by 1

Used byIndependent events have independent indicators

LemmaIndependent events have independent indicators#✓fully proved

If two sets \(s\) and \(t\) are independent with respect to a probability measure \(\mu\), then their real-valued indicator functions \(1_s\) and \(1_t\) are independent random variables with respect to \(\mu\).

lemma indepFun_indicator_of_indepSet {s t : Set Ω} (h : IndepSet s t μ) :
    IndepFun (s.indicator (1 : Ω → ℝ)) (t.indicator (1 : Ω → ℝ)) μ

Uses 1 · Used by 1

Proof usesThe σ-algebra generated by an indicator function

Used byVariance of a sum of pairwise independent indicators is at most its mean

LemmaIndicators are square-integrable#✓fully proved

If \(\mu\) is a probability measure and \(s\) is a measurable set, then the real-valued indicator function \(1_s\) lies in \(L^2(\mu)\).

lemma memLp_indicator_one {s : Set Ω} (hs : MeasurableSet s) :
    MemLp (s.indicator (1 : Ω → ℝ)) 2 μ

Used by 4

Used byExpectation of a sum of indicators · Partial sums of indicators are square-integrable · Variance of an indicator is at most its probability · Variance of a sum of pairwise independent indicators is at most its mean

LemmaThe square of an indicator is itself#✓fully proved

For every set \(s \subseteq \Omega\), the real-valued indicator function \(1_s\) satisfies \(1_s^2 = 1_s\).

lemma indicator_one_sq (s : Set Ω) :
    s.indicator (1 : Ω → ℝ) ^ 2 = s.indicator 1

Used by 1

Used byVariance of an indicator is at most its probability

LemmaVariance of an indicator is at most its probability#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\) and let \(s \subseteq \Omega\) be measurable. Then the indicator function \(1_s\) satisfies \(\operatorname{Var}_\mu(1_s) \le \mu(s)\).

In fact \(\operatorname{Var}_\mu(1_s) = \mu(s)(1 - \mu(s))\).

lemma variance_indicator_le {s : Set Ω} (hs : MeasurableSet s) :
    variance (s.indicator (1 : Ω → ℝ)) μ ≤ (μ s).toReal

Uses 2 · Used by 1

Proof usesThe square of an indicator is itself · Indicators are square-integrable

Used byVariance of a sum of pairwise independent indicators is at most its mean

TheoremExpectation of a sum of indicators#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\) and let \(A_0, A_1, \dots\) be measurable sets. For every \(n\), the partial sum \(S_n = \sum_{i < n} 1_{A_i}\) has expectation \(E[S_n] = \sum_{i < n} \mu(A_i)\).

theorem integral_partialSumIndicators
    (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i)) (n : ℕ) :
    ∫ ω, partialSumIndicators A n ω ∂μ =
    ∑ i ∈ Finset.range n, (μ (A i)).toReal

Uses 2 · Used by 4

Statement usesPartial sums of indicators

Proof usesIndicators are square-integrable

Used byMonotonicity of the expected partial sums · The expected partial sums grow by at most one per step · Divergent total probability makes the expected partial sums diverge · Pairwise-independent strong law for indicator sums

TheoremVariance of a sum of pairwise independent indicators is at most its mean#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\) and let \(A_0, A_1, \dots\) be pairwise independent measurable subsets of \(\Omega\). Then for every \(n\), the partial sum \(S_n = \sum_{i < n} 1_{A_i}\) satisfies \(\operatorname{Var}(S_n) \le \mathbb{E}[S_n]\), where variance and expectation are taken with respect to \(\mu\).

This follows from \(\operatorname{Var}(1_{A_i}) \le \mu(A_i)\) and the fact that pairwise independence makes covariances vanish.

theorem variance_partialSumIndicators_le
    (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i))
    (hindep : Pairwise fun i j => IndepSet (A i) (A j) μ)
    (n : ℕ) :
    variance (partialSumIndicators A n) μ ≤
    integral μ (partialSumIndicators A n)

Uses 5 · Used by 1

Statement usesPartial sums of indicators

Proof usesIndependent events have independent indicators · Indicators are square-integrable · The partial sum as a sum of indicator functions · Variance of an indicator is at most its probability

Used byChebyshev bound along the subsequence

TheoremDivergent total probability makes the expected partial sums diverge#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots \subseteq \Omega\) be measurable sets with \(\sum_n \mu(A_n) = \infty\), and let \(S_n = \sum_{i\lt n} 1_{A_i}\). Then \(\mathbb{E}[S_n] \to \infty\) as \(n \to \infty\).

Here \(\mathbb{E}[S_n] = \sum_{i\lt n} \mu(A_i)\).

theorem ES_tendsto_atTop
    (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i))
    (hsum : ∑' n, μ (A n) = ⊤) :
    Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop

Uses 2 · Used by 1

Statement usesPartial sums of indicators

Proof usesExpectation of a sum of indicators

Used byPairwise-independent strong law for indicator sums

TheoremMonotonicity of the expected partial sums#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots \subseteq \Omega\) be measurable sets and let \(S_n = \sum_{i\lt n} 1_{A_i}\). Then \(n \mapsto \mathbb{E}[S_n]\) is nondecreasing.

This holds because \(\mathbb{E}[S_n] = \sum_{i\lt n} \mu(A_i)\) and every summand is nonnegative.

theorem ES_mono (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i)) :
    Monotone (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)

Uses 2 · Used by 3

Statement usesPartial sums of indicators

Proof usesExpectation of a sum of indicators

Used byRatios of consecutive subsequence expectations tend to one · Pairwise-independent strong law for indicator sums · The quadratic subsequence is strictly increasing

TheoremThe expected partial sums grow by at most one per step#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots \subseteq \Omega\) be measurable sets and let \(S_n = \sum_{i\lt n} 1_{A_i}\). Then \(\mathbb{E}[S_{n+1}] - \mathbb{E}[S_n] \le 1\) for every \(n \in \mathbb{N}\).

Indeed the difference equals \(\mu(A_n) \le 1\).

theorem ES_step_le_one (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i)) (n : ℕ) :
    ∫ ω, partialSumIndicators A (n + 1) ω ∂μ - ∫ ω, partialSumIndicators A n ω ∂μ ≤ 1

Uses 2 · Used by 2

Statement usesPartial sums of indicators

Proof usesExpectation of a sum of indicators

Used byUpper bound for the expected partial sums along the subsequence · The quadratic subsequence is strictly increasing

DefinitionQuadratic subsequence for the pairwise-independent strong law#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots\) be subsets of \(\Omega\), and write \(S_n = \sum_{i < n} 1_{A_i}\). Assuming \(\mathbb{E}[S_n] = \int S_n \, d\mu \to \infty\) as \(n \to \infty\), this is the sequence \(\varphi : \mathbb{N} \to \mathbb{N}\) for which \(\varphi(k)\) is the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\).

Because the thresholds grow quadratically, the Chebyshev tail bounds for \(S_{\varphi(k)} / \mathbb{E}[S_{\varphi(k)}]\) are summable.

noncomputable def sllnSubseq {A : ℕ → Set Ω}
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop) : ℕ → ℕ :=
  fun k => Nat.find
    ((hES_top.eventually (Filter.eventually_ge_atTop (((k : ℝ) + 1) ^ 2))).exists)

Uses 1 · Used by 9

Statement usesPartial sums of indicators

Used byChebyshev bound along the subsequence · The expected partial sums along the subsequence are positive · Upper bound for the expected partial sums along the subsequence · Ratios of consecutive subsequence expectations tend to one · Pairwise-independent strong law for indicator sums · Indices of the quadratic subsequence are positive · Lower bound on the expected count along the quadratic subsequence · The quadratic subsequence is strictly increasing · Summable deviation probabilities along the quadratic subsequence

LemmaLower bound on the expected count along the quadratic subsequence#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots\) be subsets of \(\Omega\), write \(S_n = \sum_{i < n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] = \int S_n \, d\mu \to \infty\) as \(n \to \infty\). If \(\varphi(k)\) is the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\), then \(\mathbb{E}[S_{\varphi(k)}] \ge (k+1)^2\) for every natural number \(k\).

lemma sllnSubseq_spec {A : ℕ → Set Ω}
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop)
    (k : ℕ) :
    ((k : ℝ) + 1) ^ 2 ≤ ∫ ω, partialSumIndicators A (sllnSubseq hES_top k) ω ∂μ

Uses 2 · Used by 5

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Used byChebyshev bound along the subsequence · The expected partial sums along the subsequence are positive · Ratios of consecutive subsequence expectations tend to one · Indices of the quadratic subsequence are positive · The quadratic subsequence is strictly increasing

LemmaIndices of the quadratic subsequence are positive#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots\) be subsets of \(\Omega\), write \(S_n = \sum_{i < n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] = \int S_n \, d\mu \to \infty\) as \(n \to \infty\). If \(\varphi(k)\) is the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\), then \(\varphi(k) > 0\) for every natural number \(k\).

This holds because \(\mathbb{E}[S_0] = 0 < (k+1)^2\).

lemma sllnSubseq_pos {A : ℕ → Set Ω}
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop)
    (k : ℕ) : 0 < sllnSubseq hES_top k

Uses 3 · Used by 2

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Proof usesLower bound on the expected count along the quadratic subsequence

Used byUpper bound for the expected partial sums along the subsequence · The quadratic subsequence is strictly increasing

LemmaThe quadratic subsequence is strictly increasing#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots\) be measurable subsets of \(\Omega\), write \(S_n = \sum_{i < n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] = \int S_n \, d\mu \to \infty\) as \(n \to \infty\). If \(\varphi(k)\) is the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\), then \(\varphi : \mathbb{N} \to \mathbb{N}\) is strictly increasing.

lemma sllnSubseq_strictMono {A : ℕ → Set Ω}
    (hA : ∀ i, MeasurableSet (A i))
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop) :
    StrictMono (sllnSubseq hES_top)

Uses 6 · Used by 2

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Proof usesMonotonicity of the expected partial sums · The expected partial sums grow by at most one per step · Indices of the quadratic subsequence are positive · Lower bound on the expected count along the quadratic subsequence

Used byRatios of consecutive subsequence expectations tend to one · Pairwise-independent strong law for indicator sums

LemmaThe expected partial sums along the subsequence are positive#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots \subseteq \Omega\), let \(S_n = \sum_{i\lt n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] \to \infty\). For \(k \in \mathbb{N}\) let \(\varphi(k)\) be the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\). Then \(\mathbb{E}[S_{\varphi(k)}] > 0\) for every \(k \in \mathbb{N}\).

Indeed \(\mathbb{E}[S_{\varphi(k)}] \ge (k+1)^2 > 0\).

lemma ES_sllnSubseq_pos {A : ℕ → Set Ω}
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop)
    (k : ℕ) :
    0 < ∫ ω, partialSumIndicators A (sllnSubseq hES_top k) ω ∂μ

Uses 3 · Used by 3

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Proof usesLower bound on the expected count along the quadratic subsequence

Used byChebyshev bound along the subsequence · Ratios of consecutive subsequence expectations tend to one · Pairwise-independent strong law for indicator sums

LemmaPartial sums of indicators are square-integrable#✓fully proved

Let \(\mu\) be a probability measure and let \(A_0, A_1, \dots\) be measurable sets. For every \(n\), the partial sum \(S_n = \sum_{i < n} 1_{A_i}\) lies in \(L^2(\mu)\).

lemma memLp_partialSumIndicators (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i)) (n : ℕ) :
    MemLp (partialSumIndicators A n) 2 μ

Uses 3 · Used by 1

Statement usesPartial sums of indicators

Proof usesIndicators are square-integrable · The partial sum as a sum of indicator functions

Used byChebyshev bound along the subsequence

LemmaAlmost sure convergence from shrinking tail bounds#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(f_k : \Omega \to \mathbb{R}\) for \(k \in \mathbb{N}\), and let \(a \in \mathbb{R}\). Suppose that for every \(m \in \mathbb{N}\), for \(\mu\)-almost every \(\omega\), we have \(|f_k(\omega) - a| < 1/(m+1)\) for all sufficiently large \(k\). Then for \(\mu\)-almost every \(\omega\), \(f_k(\omega) \to a\) as \(k \to \infty\).

lemma ae_tendsto_of_ae_eventually_abs_sub_lt
    {f : ℕ → Ω → ℝ} {a : ℝ}
    (h : ∀ m : ℕ, ∀ᵐ ω ∂μ, ∀ᶠ k in Filter.atTop, |f k ω - a| < 1 / ((m : ℝ) + 1)) :
    ∀ᵐ ω ∂μ, Filter.Tendsto (fun k => f k ω) Filter.atTop (nhds a)

Used by 1

Used byPairwise-independent strong law for indicator sums

LemmaChebyshev bound along the subsequence#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots \subseteq \Omega\) be pairwise independent measurable sets, let \(S_n = \sum_{i\lt n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] \to \infty\). For \(k \in \mathbb{N}\) let \(\varphi(k)\) be the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\). Then for every \(\varepsilon > 0\) and every \(k \in \mathbb{N}\), the probability of the set of \(\omega\) with \(|S_{\varphi(k)}(\omega)/\mathbb{E}[S_{\varphi(k)}] - 1| \ge \varepsilon\) is at most \(1/(\varepsilon^2 (k+1)^2)\).

These bounds are summable in \(k\), which gives almost sure convergence along the subsequence.

lemma chebyshev_subseq_bound
    (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i))
    (hindep : Pairwise fun i j => IndepSet (A i) (A j) μ)
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop)
    (ε : ℝ) (hε : 0 < ε) (k : ℕ) :
    μ {ω | ε ≤ |partialSumIndicators A (sllnSubseq hES_top k) ω /
            (∫ ω', partialSumIndicators A (sllnSubseq hES_top k) ω' ∂μ) - 1|} ≤
    ENNReal.ofReal (1 / (ε ^ 2 * ((k : ℝ) + 1) ^ 2))

Uses 6 · Used by 1

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Proof usesThe expected partial sums along the subsequence are positive · Partial sums of indicators are square-integrable · Lower bound on the expected count along the quadratic subsequence · Variance of a sum of pairwise independent indicators is at most its mean

Used bySummable deviation probabilities along the quadratic subsequence

LemmaSummable deviation probabilities along the quadratic subsequence#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots\) be pairwise independent measurable subsets of \(\Omega\), write \(S_n = \sum_{i < n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] = \int S_n \, d\mu \to \infty\) as \(n \to \infty\). Let \(\varphi(k)\) be the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\). Then for every real \(\varepsilon > 0\), the sum over \(k \in \mathbb{N}\) of the probabilities \(\mu\{\omega : |S_{\varphi(k)}(\omega) / \mathbb{E}[S_{\varphi(k)}] - 1| \ge \varepsilon\}\) is finite.

By Chebyshev's inequality the \(k\)-th term is at most \(1/(\varepsilon^2 (k+1)^2)\); this is the Borel–Cantelli input along the subsequence.

lemma summable_chebyshev_subseq
    (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i))
    (hindep : Pairwise fun i j => IndepSet (A i) (A j) μ)
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop)
    (ε : ℝ) (hε : 0 < ε) :
    ∑' k, μ {ω | ε ≤ |partialSumIndicators A (sllnSubseq hES_top k) ω /
            (∫ ω', partialSumIndicators A (sllnSubseq hES_top k) ω' ∂μ) - 1|} ≠ ⊤

Uses 3 · Used by 1

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Proof usesChebyshev bound along the subsequence

Used byPairwise-independent strong law for indicator sums

LemmaPartial sums of indicators are nondecreasing#✓fully proved

For sets \(A_0, A_1, \dots\) and every \(\omega \in \Omega\), the map \(n \mapsto S_n(\omega)\), where \(S_n = \sum_{i < n} 1_{A_i}\), is nondecreasing.

lemma partialSumIndicators_mono (A : ℕ → Set Ω) (ω : Ω) :
    Monotone (fun n => partialSumIndicators A n ω)

Uses 1 · Used by 1

Statement usesPartial sums of indicators

Used byPairwise-independent strong law for indicator sums

LemmaPartial sums of indicators are nonnegative#✓fully proved

For sets \(A_0, A_1, \dots\), every \(n\) and every \(\omega \in \Omega\), the partial sum \(S_n(\omega) = \sum_{i < n} 1_{A_i}(\omega)\) satisfies \(S_n(\omega) \ge 0\).

lemma partialSumIndicators_nonneg (A : ℕ → Set Ω) (n : ℕ) (ω : Ω) :
    0 ≤ partialSumIndicators A n ω

Uses 1 · Used by 1

Statement usesPartial sums of indicators

Used byPairwise-independent strong law for indicator sums

LemmaBracketing by a strictly increasing sequence#✓fully proved

Let \(\varphi : \mathbb{N} \to \mathbb{N}\) be strictly increasing and let \(n \ge \varphi(0)\). Then there is \(k \in \mathbb{N}\) with \(\varphi(k) \le n < \varphi(k+1)\).

This is used to sandwich a general index \(n\) between two consecutive subsequence indices.

lemma exists_bracket_of_strictMono (φ : ℕ → ℕ) (hφ : StrictMono φ) (n : ℕ) (hn : φ 0 ≤ n) :
    ∃ k, φ k ≤ n ∧ n < φ (k + 1)

Used by 1

Used byPairwise-independent strong law for indicator sums

LemmaUpper bound for the expected partial sums along the subsequence#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots \subseteq \Omega\) be measurable sets, let \(S_n = \sum_{i\lt n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] \to \infty\). For \(k \in \mathbb{N}\) let \(\varphi(k)\) be the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\). Then \(\mathbb{E}[S_{\varphi(k)}] < (k+1)^2 + 1\) for every \(k \in \mathbb{N}\).

This holds because \(\mathbb{E}[S_{\varphi(k)-1}] < (k+1)^2\) and the expectation grows by at most one per step.

lemma ES_sllnSubseq_upper_bound {A : ℕ → Set Ω}
    (hA : ∀ i, MeasurableSet (A i))
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop)
    (k : ℕ) :
    ∫ ω, partialSumIndicators A (sllnSubseq hES_top k) ω ∂μ < ((k : ℝ) + 1) ^ 2 + 1

Uses 4 · Used by 1

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Proof usesThe expected partial sums grow by at most one per step · Indices of the quadratic subsequence are positive

Used byRatios of consecutive subsequence expectations tend to one

LemmaRatios of consecutive subsequence expectations tend to one#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \(A_0, A_1, \dots \subseteq \Omega\) be measurable sets, let \(S_n = \sum_{i\lt n} 1_{A_i}\), and suppose that \(\mathbb{E}[S_n] \to \infty\). For \(k \in \mathbb{N}\) let \(\varphi(k)\) be the least \(n\) with \(\mathbb{E}[S_n] \ge (k+1)^2\). Then \(\mathbb{E}[S_{\varphi(k+1)}] / \mathbb{E}[S_{\varphi(k)}] \to 1\) as \(k \to \infty\).

This slow growth lets the proof of the pairwise-independent strong law pass from the subsequence to the full sequence.

lemma ES_subseq_ratio_tendsto_one {A : ℕ → Set Ω}
    (hA : ∀ i, MeasurableSet (A i))
    (hES_top : Filter.Tendsto (fun n => ∫ ω, partialSumIndicators A n ω ∂μ)
      Filter.atTop Filter.atTop) :
    Filter.Tendsto
      (fun k => (∫ ω, partialSumIndicators A (sllnSubseq hES_top (k + 1)) ω ∂μ) /
                (∫ ω, partialSumIndicators A (sllnSubseq hES_top k) ω ∂μ))
      Filter.atTop (nhds 1)

Uses 7 · Used by 1

Statement usesPartial sums of indicators · Quadratic subsequence for the pairwise-independent strong law

Proof usesMonotonicity of the expected partial sums · The expected partial sums along the subsequence are positive · Upper bound for the expected partial sums along the subsequence · Lower bound on the expected count along the quadratic subsequence · The quadratic subsequence is strictly increasing

Used byPairwise-independent strong law for indicator sums

TheoremPairwise-independent strong law for indicator sums#✓fully proved

Let \(A_1, A_2, \dots\) be pairwise independent events in a probability space with \(\sum_n P(A_n) = \infty\), and write \(S_n = \sum_{i=1}^n 1_{A_i}\). Then almost surely \(S_n / E[S_n] \to 1\) as \(n \to \infty\), where \(E[S_n] = \sum_{i=1}^n P(A_i)\).

theorem pairwise_indep_slln
    {A : ℕ → Set Ω}
    (hA_meas : ∀ n, MeasurableSet (A n))
    (hA_indep : Pairwise fun i j => IndepSet (A i) (A j) μ)
    (hA_sum : ∑' n, μ (A n) = ⊤) :
    ∀ᵐ ω ∂μ, Filter.Tendsto
      (fun n => (∑ i ∈ Finset.range n, (A i).indicator (1 : Ω → ℝ) ω) /
                (∑ i ∈ Finset.range n, (μ (A i)).toReal))
      Filter.atTop (nhds 1)

Sources

• Lecture 9.

Uses 13

Proof usesMonotonicity of the expected partial sums · The expected partial sums along the subsequence are positive · Ratios of consecutive subsequence expectations tend to one · Divergent total probability makes the expected partial sums diverge · Almost sure convergence from shrinking tail bounds · Bracketing by a strictly increasing sequence · Expectation of a sum of indicators · Partial sums of indicators · Partial sums of indicators are nondecreasing · Partial sums of indicators are nonnegative · Quadratic subsequence for the pairwise-independent strong law · The quadratic subsequence is strictly increasing · Summable deviation probabilities along the quadratic subsequence

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.