noncomputable def partialSumIndicators {Ω : Type u_1} (A : ℕ → Set Ω) (n : ℕ) : Ω → ℝ

The partial sum S_n = ∑_{i < n} 1_{A_i} of indicators of the first n events, viewed as a real-valued random variable on Ω.

theorem partialSumIndicators_eq {Ω : Type u_1} [MeasurableSpace Ω] (A : ℕ → Set Ω) (n : ℕ) : partialSumIndicators A n = ∑ i ∈ Finset.range n, (A i).indicator 1

Rewrite partialSumIndicators A n as the pointwise sum (function-valued sum) of the individual indicator functions.

theorem comap_indicator_one_le_generateFrom {Ω : Type u_1} [MeasurableSpace Ω] (s : Set Ω) : MeasurableSpace.comap (s.indicator 1) Real.measurableSpace ≤ MeasurableSpace.generateFrom {s}

The σ-algebra generated by the indicator 1_s : Ω → ℝ of a set s is contained in the σ-algebra generated by the singleton family {s}.

theorem indepFun_indicator_of_indepSet {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s t : Set Ω} (h : ProbabilityTheory.IndepSet s t μ) : ProbabilityTheory.IndepFun (s.indicator 1) (t.indicator 1) μ

Independence of two sets implies independence of their real-valued indicator functions.

theorem memLp_indicator_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : MeasureTheory.MemLp (s.indicator 1) 2 μ

The indicator function 1_s of a measurable set is in L² for any probability measure.

theorem indicator_one_sq {Ω : Type u_1} [MeasurableSpace Ω] (s : Set Ω) : s.indicator 1 ^ 2 = s.indicator 1

The square of an indicator function equals the indicator function itself: (1_s)² = 1_s.

theorem variance_indicator_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : ProbabilityTheory.variance (s.indicator 1) μ ≤ (μ s).toReal

The variance of the indicator of a measurable set is bounded by its probability: Var(1_s) = P(s)(1 - P(s)) ≤ P(s).

theorem integral_partialSumIndicators {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) (n : ℕ) : ∫ (ω : Ω), partialSumIndicators A n ω ∂μ = ∑ i ∈ Finset.range n, (μ (A i)).toReal

The expected value E[S_n] = ∑_{i < n} P(A_i) of the partial sum of indicators.

theorem variance_partialSumIndicators_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepSet (A i) (A j) μ) (n : ℕ) : ProbabilityTheory.variance (partialSumIndicators A n) μ ≤ MeasureTheory.integral μ (partialSumIndicators A n)

For pairwise independent events A_i, the variance of the partial sum of indicators is bounded by its expectation: Var(S_n) ≤ E[S_n]. This follows from Var(1_{A_i}) ≤ P(A_i) and the fact that pairwise independence makes covariances vanish.

theorem ES_tendsto_atTop {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) (hsum : ∑' (n : ℕ), μ (A n) = ⊤) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), partialSumIndicators A n ω ∂μ) Filter.atTop Filter.atTop

If ∑ P(A_n) = ∞, then the expectations E[S_n] = ∑_{i<n} P(A_i) of the partial sums tend to ∞.

theorem ES_mono {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) : Monotone fun (n : ℕ) => ∫ (ω : Ω), partialSumIndicators A n ω ∂μ

The map n ↦ E[S_n] is monotone since each summand P(A_i) is nonnegative.

theorem ES_step_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) (n : ℕ) : ∫ (ω : Ω), partialSumIndicators A (n + 1) ω ∂μ - ∫ (ω : Ω), partialSumIndicators A n ω ∂μ ≤ 1

Successive expectations differ by at most one: E[S_{n+1}] - E[S_n] = P(A_n) ≤ 1.

noncomputable def sllnSubseq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {A : ℕ → Set Ω} (hES_top : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), partialSumIndicators A n ω ∂μ) Filter.atTop Filter.atTop) : ℕ → ℕ

The subsequence φ(k) used in the proof of the pairwise-independent strong law: it chooses the first index n such that E[S_n] ≥ (k+1)². Because the spacing grows quadratically, the Chebyshev tail bounds for S_{φ(k)}/E[S_{φ(k)}] are summable.

theorem sllnSubseq_spec {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {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) ω ∂μ

Defining property of sllnSubseq: at index φ(k) we have E[S_{φ(k)}] ≥ (k+1)².

theorem sllnSubseq_pos {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {A : ℕ → Set Ω} (hES_top : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), partialSumIndicators A n ω ∂μ) Filter.atTop Filter.atTop) (k : ℕ) : 0 < sllnSubseq hES_top k

Every index φ(k) in the subsequence is strictly positive, because E[S_0] = 0 cannot reach (k+1)² > 0.

theorem sllnSubseq_strictMono {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {A : ℕ → Set Ω} (hA : ∀ (i : ℕ), MeasurableSet (A i)) (hES_top : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), partialSumIndicators A n ω ∂μ) Filter.atTop Filter.atTop) : StrictMono (sllnSubseq hES_top)

The subsequence φ : ℕ → ℕ is strictly monotone.

theorem ES_sllnSubseq_pos {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {A : ℕ → Set Ω} (hES_top : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), partialSumIndicators A n ω ∂μ) Filter.atTop Filter.atTop) (k : ℕ) : 0 < ∫ (ω : Ω), partialSumIndicators A (sllnSubseq hES_top k) ω ∂μ

The expectation E[S_{φ(k)}] along the subsequence is strictly positive (at least (k+1)² > 0).

theorem memLp_partialSumIndicators {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) (n : ℕ) : MeasureTheory.MemLp (partialSumIndicators A n) 2 μ

The partial-sum random variable S_n is in L².

theorem ae_tendsto_of_ae_eventually_abs_sub_lt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : ℕ → Ω → ℝ} {a : ℝ} (h : ∀ (m : ℕ), ∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (k : ℕ) in Filter.atTop, |f k ω - a| < 1 / (↑m + 1)) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => f k ω) Filter.atTop (nhds a)

Almost sure convergence from quantitative tail bounds: if for every m, almost surely |f_k(ω) - a| < 1/(m+1) eventually as k → ∞, then almost surely f_k(ω) → a.

theorem chebyshev_subseq_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.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))

Chebyshev tail bound along the subsequence: the probability that |S_{φ(k)}/E[S_{φ(k)}] - 1| ≥ ε is bounded by 1/(ε² (k+1)²). This is the summable estimate used to conclude a.s. convergence along the subsequence.

theorem summable_chebyshev_subseq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (A : ℕ → Set Ω) (hA : ∀ (i : ℕ), MeasurableSet (A i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.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|} ≠ ⊤

Summing the Chebyshev bounds along the subsequence gives a finite total measure, since ∑ 1/(k+1)² < ∞. This is the Borel-Cantelli input for the subsequence.

theorem partialSumIndicators_mono {Ω : Type u_1} [MeasurableSpace Ω] (A : ℕ → Set Ω) (ω : Ω) : Monotone fun (n : ℕ) => partialSumIndicators A n ω

Pointwise monotonicity of the partial sum process: for each ω, the map n ↦ S_n(ω) is nondecreasing.

theorem partialSumIndicators_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (A : ℕ → Set Ω) (n : ℕ) (ω : Ω) : 0 ≤ partialSumIndicators A n ω

The partial sum S_n(ω) ≥ 0 since it is a sum of nonnegative indicators.

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

For a strictly monotone sequence φ : ℕ → ℕ and any n ≥ φ 0, there exists k such that φ k ≤ n < φ (k+1). This "bracketing" is used to sandwich a general n between two consecutive subsequence indices.

theorem ES_sllnSubseq_upper_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {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

Upper bound on E[S_{φ(k)}] by (k+1)² + 1, since the previous index φ(k) - 1 fails the threshold (k+1)² and the expectation grows by at most one per step.

theorem ES_subseq_ratio_tendsto_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {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)

The ratio E[S_{φ(k+1)}] / E[S_{φ(k)}] tends to 1 as k → ∞. This "slow growth" property allows interpolation between the subsequence and the full sequence in the SLLN proof.

theorem pairwise_indep_slln {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {A : ℕ → Set Ω} (hA_meas : ∀ (n : ℕ), MeasurableSet (A n)) (hA_indep : Pairwise fun (i j : ℕ) => ProbabilityTheory.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)

Pairwise-independent strong law for indicator sums (Lecture 9): suppose A₁, A₂, … are pairwise independent events with ∑ P(A_n) = ∞, and write S_n = ∑_{i=1}^n 1_{A_i}. Then the ratio S_n / E[S_n] tends almost surely to 1.