noncomputable def KolmogorovThreeSeries.truncatedRV {Ω : Type u_1} (X : ℕ → Ω → ℝ) (A : ℝ) (n : ℕ) : Ω → ℝ

The truncation Yₙ = Xₙ · 1_{|Xₙ| ≤ A} of the random variable Xₙ at threshold A, i.e. Yₙ(ω) = Xₙ(ω) when |Xₙ(ω)| ≤ A and 0 otherwise. This is the key construction in the Kolmogorov three-series theorem.

theorem KolmogorovThreeSeries.ae_tendsto_centered_of_indep_summableVar {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX_indep : ProbabilityTheory.iIndepFun X μ) {A : ℝ} (hA : A > 0) (h3 : Summable fun (n : ℕ) => ProbabilityTheory.variance (fun (ω : Ω) => X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω) μ) : ∀ᵐ (ω : Ω) ∂μ, ∃ (c : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (truncatedRV X A i ω - ∫ (ω' : Ω), X i ω' * {ω' : Ω | |X i ω'| ≤ A}.indicator 1 ω' ∂μ)) Filter.atTop (nhds c)

If the truncated variables have summable variances, then almost surely the partial sums of the centered truncations converge: ∑ (Yᵢ - E[Yᵢ]) converges a.s.

theorem KolmogorovThreeSeries.summable_mean_and_variance_of_ae_tendsto_ax {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX_indep : ProbabilityTheory.iIndepFun X μ) {A : ℝ} (hA : A > 0) (hY_tend : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, truncatedRV X A i ω) Filter.atTop (nhds (S ω))) : (Summable fun (n : ℕ) => ∫ (ω : Ω), X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω ∂μ) ∧ Summable fun (n : ℕ) => ProbabilityTheory.variance (fun (ω : Ω) => X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω) μ

(Axiomatic) If the partial sums of the truncations Yₙ = Xₙ · 1_{|Xₙ| ≤ A} converge almost surely, then both ∑ E[Yₙ] and ∑ Var(Yₙ) are summable. This is the harder direction of the three-series theorem; here it is taken as a hypothesis.

theorem KolmogorovThreeSeries.ae_eventually_truncation_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} {A : ℝ} (h1 : ∑' (n : ℕ), μ {ω : Ω | A < |X n ω|} < ⊤) : ∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, X n ω = truncatedRV X A n ω

If ∑ₙ P{|Xₙ| > A} < ∞, then by the first Borel–Cantelli lemma, almost surely the truncation eventually coincides with Xₙ.

theorem KolmogorovThreeSeries.ae_tendsto_of_ae_eventually_eq_and_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f g : ℕ → Ω → ℝ} (hfg : ∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, f n ω = g n ω) (hf : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i ω) Filter.atTop (nhds (S ω))) : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, g i ω) Filter.atTop (nhds (S ω))

If two sequences f, g of random variables agree eventually (almost surely) and the partial sums of f converge almost surely, then the partial sums of g also converge almost surely (to a possibly different limit).

theorem KolmogorovThreeSeries.ae_tendsto_truncated_of_conditions {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX_indep : ProbabilityTheory.iIndepFun X μ) {A : ℝ} (hA : A > 0) (h2 : Summable fun (n : ℕ) => ∫ (ω : Ω), X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω ∂μ) (h3 : Summable fun (n : ℕ) => ProbabilityTheory.variance (fun (ω : Ω) => X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω) μ) : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, truncatedRV X A i ω) Filter.atTop (nhds (S ω))

If the means and variances of the truncations are summable then the partial sums of the truncations ∑ Yᵢ converge almost surely. This combines the centered convergence result with the (deterministic) convergence of the mean series.

theorem KolmogorovThreeSeries.truncatedRV_eq_comp {Ω : Type u_1} [MeasurableSpace Ω] (X : ℕ → Ω → ℝ) (A : ℝ) (n : ℕ) : truncatedRV X A n = (fun (x : ℝ) => x * {x : ℝ | |x| ≤ A}.indicator 1 x) ∘ X n

truncatedRV factors as the composition of Xₙ with the deterministic truncation function x ↦ x · 1_{|x| ≤ A}.

theorem KolmogorovThreeSeries.measurable_truncation_fun (A : ℝ) : Measurable fun (x : ℝ) => x * {x : ℝ | |x| ≤ A}.indicator 1 x

The deterministic truncation function x ↦ x · 1_{|x| ≤ A} is measurable.

theorem KolmogorovThreeSeries.iIndepFun_truncatedRV {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} (hX_indep : ProbabilityTheory.iIndepFun X μ) (A : ℝ) : ProbabilityTheory.iIndepFun (fun (n : ℕ) => truncatedRV X A n) μ

If (Xₙ) is an independent family then so is (truncatedRV X A n), since truncation is a measurable function applied componentwise.

theorem KolmogorovThreeSeries.abs_truncatedRV_le {Ω : Type u_1} [MeasurableSpace Ω] {X : ℕ → Ω → ℝ} {A : ℝ} (hA : A ≥ 0) (n : ℕ) (ω : Ω) : |truncatedRV X A n ω| ≤ A

The truncated random variable is bounded by A in absolute value.

theorem KolmogorovThreeSeries.truncated_indicator_eq_of_bdd {Ω : Type u_1} [MeasurableSpace Ω] {Y : ℕ → Ω → ℝ} {A : ℝ} (hY_bdd : ∀ (n : ℕ) (ω : Ω), |Y n ω| ≤ A) (n : ℕ) : (fun (ω : Ω) => Y n ω * {ω : Ω | |Y n ω| ≤ A}.indicator 1 ω) = Y n

If |Yₙ| ≤ A everywhere, then truncation at level A is the identity, i.e. Yₙ · 1_{|Yₙ| ≤ A} = Yₙ.

theorem KolmogorovThreeSeries.truncatedRV_eq_of_bdd {Ω : Type u_1} [MeasurableSpace Ω] {Y : ℕ → Ω → ℝ} {A : ℝ} (hY_bdd : ∀ (n : ℕ) (ω : Ω), |Y n ω| ≤ A) (n : ℕ) : truncatedRV Y A n = Y n

If |Yₙ| ≤ A everywhere, then truncatedRV Y A n = Yₙ.

theorem KolmogorovThreeSeries.ae_tendsto_truncatedRV_of_bdd {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y : ℕ → Ω → ℝ} {A : ℝ} (hY_bdd : ∀ (n : ℕ) (ω : Ω), |Y n ω| ≤ A) (hY_tend : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, Y i ω) Filter.atTop (nhds (S ω))) : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, truncatedRV Y A i ω) Filter.atTop (nhds (S ω))

If (Yₙ) is uniformly bounded by A and its partial sums converge a.s., then so do the partial sums of truncatedRV Y A n (in fact to the same limit).

theorem KolmogorovThreeSeries.summable_variance_of_bounded_indep_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : ℕ → Ω → ℝ} (hY_meas : ∀ (n : ℕ), Measurable (Y n)) (hY_indep : ProbabilityTheory.iIndepFun Y μ) {A : ℝ} (hA : A > 0) (hY_bdd : ∀ (n : ℕ) (ω : Ω), |Y n ω| ≤ A) (hY_tend : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, Y i ω) Filter.atTop (nhds (S ω))) : Summable fun (n : ℕ) => ProbabilityTheory.variance (Y n) μ

For a uniformly bounded independent sequence Yₙ (|Yₙ| ≤ A), almost-sure convergence of the partial sums implies that the variances ∑ Var(Yₙ) are summable.

theorem KolmogorovThreeSeries.summable_mean_of_variance_summable_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : ℕ → Ω → ℝ} (hY_meas : ∀ (n : ℕ), Measurable (Y n)) (hY_indep : ProbabilityTheory.iIndepFun Y μ) {A : ℝ} (hA : A > 0) (hY_bdd : ∀ (n : ℕ) (ω : Ω), |Y n ω| ≤ A) (hY_tend : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, Y i ω) Filter.atTop (nhds (S ω))) (_hVar : Summable fun (n : ℕ) => ProbabilityTheory.variance (Y n) μ) : Summable fun (n : ℕ) => ∫ (ω : Ω), Y n ω ∂μ

For a uniformly bounded independent sequence Yₙ (|Yₙ| ≤ A) whose partial sums converge a.s. and whose variances are summable, the means ∑ E[Yₙ] are also summable.

theorem KolmogorovThreeSeries.summable_mean_and_variance_of_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX_indep : ProbabilityTheory.iIndepFun X μ) {A : ℝ} (hA : A > 0) (hY_tend : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, truncatedRV X A i ω) Filter.atTop (nhds (S ω))) : (Summable fun (n : ℕ) => ∫ (ω : Ω), X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω ∂μ) ∧ Summable fun (n : ℕ) => ProbabilityTheory.variance (fun (ω : Ω) => X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω) μ

If the partial sums of the truncated variables truncatedRV X A n converge a.s., then both the mean series ∑ E[Yₙ] and the variance series ∑ Var(Yₙ) are summable. This is the forward (necessity) direction of the three-series theorem applied to the truncations.

theorem KolmogorovThreeSeries.summable_tail_prob_of_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX_indep : ProbabilityTheory.iIndepFun X μ) {A : ℝ} (hA : A > 0) (hX_tend : ∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (S ω))) : ∑' (n : ℕ), μ {ω : Ω | A < |X n ω|} < ⊤

If the partial sums of an independent sequence Xₙ converge almost surely, then for every A > 0 the tail probabilities ∑ₙ P(|Xₙ| > A) are finite. Uses the second Borel–Cantelli lemma together with the fact that almost-sure convergence forces Xₙ → 0.

theorem kolmogorov_three_series_theorem {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX_indep : ProbabilityTheory.iIndepFun X μ) (A : ℝ) (hA : A > 0) : (∃ (S : Ω → ℝ), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (S ω))) ↔ ∑' (n : ℕ), μ {ω : Ω | |X n ω| > A} < ⊤ ∧ (Summable fun (n : ℕ) => ∫ (ω : Ω), X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω ∂μ) ∧ Summable fun (n : ℕ) => ProbabilityTheory.variance (fun (ω : Ω) => X n ω * {ω : Ω | |X n ω| ≤ A}.indicator 1 ω) μ

Kolmogorov's three-series theorem. Let X₁, X₂, … be independent random variables and fix A > 0. Write Yᵢ = Xᵢ · 1_{|Xᵢ| ≤ A} for the truncations. Then ∑ Xₙ converges almost surely if and only if all three of the following series converge: (1) ∑ₙ P{|Xₙ| > A}, (2) ∑ₙ E[Yₙ], and (3) ∑ₙ Var(Yₙ).