Kolmogorov's three-series theorem

Lemma\(L^1\) norm bounded by the square root of the second moment#✓fully proved

If ∫ ‖f‖² dμ ≤ C for an L² function on a probability space, then ‖f‖₁ ≤ √C.

lemma eLpNorm_one_le_sqrt_integral_sq {f : Ω → ℝ} (hf : MemLp f 2 μ) {C : ℝ}
    (h_int_sq : ∫ x, ‖f x‖ ^ (2 : ℝ) ∂μ ≤ C) [IsProbabilityMeasure μ] :
    eLpNorm f 1 μ ≤ ENNReal.ofReal (Real.sqrt C)

Used by 2

Used byAlmost sure convergence of centered truncated sums · Mean step of three-series necessity

TheoremAlmost-sure convergence of L¹-bounded sums of independent centered variables#✓fully proved

Let \(Z_0, Z_1, \dots\) be independent integrable real random variables on a probability space with \(E[Z_n] = 0\) for every \(n\), and let \(S_n = \sum_{k \le n} Z_k\). If there is a constant \(R \ge 0\) with \(E|S_n| \le R\) for every \(n\), then \(S_n\) converges almost surely to a finite limit.

This is a key step toward the Kolmogorov three-series theorem: \((S_n)\) is a martingale for the natural filtration, so the \(L^1\)-bounded martingale convergence theorem applies.

theorem ae_tendsto_sum_of_indep_centered_L1bdd {Z : ℕ → Ω → ℝ}
    [IsProbabilityMeasure μ]
    (hZ_sm : ∀ n, StronglyMeasurable (Z n))
    (hZ_indep : iIndepFun (m := fun _ => inferInstance) Z μ)
    (hZ_mean : ∀ n, ∫ ω, Z n ω ∂μ = 0)
    (hZ_int : ∀ n, Integrable (Z n) μ)
    {R : NNReal}
    (hZ_L1_bdd : ∀ n, eLpNorm (fun ω => ∑ k ∈ range (n + 1), Z k ω) 1 μ ≤ ↑R) :
    ∀ᵐ ω ∂μ, ∃ c, Tendsto (fun n => ∑ k ∈ range (n + 1), Z k ω) atTop (nhds c)

Used by 2

Used byAlmost sure convergence of centered truncated sums · Mean step of three-series necessity

DefinitionTruncation of a random variable#✓fully proved

For a sequence \(X_0, X_1, \dots\) of real-valued functions on \(\Omega\), a threshold \(A \in \mathbb{R}\) and an index \(n\), the truncation of \(X_n\) at \(A\) is \(Y_n = X_n \mathbf{1}_{\{|X_n| \le A\}}\), that is, \(Y_n(\omega) = X_n(\omega)\) when \(|X_n(\omega)| \le A\) and \(Y_n(\omega) = 0\) otherwise.

This is the key construction in the Kolmogorov three-series theorem.

noncomputable def truncatedRV (X : ℕ → Ω → ℝ) (A : ℝ) (n : ℕ) : Ω → ℝ :=
  fun ω => X n ω * Set.indicator {ω | |X n ω| ≤ A} 1 ω

Used by 23

Used byMean bound for a truncated random variable · Truncation is bounded by a nonnegative cutoff · Truncation is bounded by the absolute cutoff · Truncations eventually agree with the variables · Almost sure convergence of centered truncated sums · Truncated sums converge almost surely · Truncation preserves almost-sure limits of bounded partial sums · Truncation preserves independence · Integrability of truncated random variables · Kolmogorov's three-series theorem (sufficiency direction) · Truncation preserves measurability · Measurability of a truncated random variable · Truncated random variables lie in every Lp space · The Summable-means necessity claim in v1 is false · Kolmogorov three-series necessity, series (2)–(3) · Formula for the truncated random variable · Canonical truncation factors through scalar truncation · Truncation fixes values within the cutoff · Truncation leaves a family bounded by the cutoff unchanged · Truncation vanishes outside the closed band · Canonical truncation preserves nonnegativity · Scalar truncation function · Variance bound for a truncated random variable

TheoremFormula for the truncated random variable#✓fully proved

The canonical truncation is the identity inside the cutoff and zero outside it.

@[simp] theorem truncatedRV_apply (X : ℕ → Ω → ℝ) (A : ℝ) (n : ℕ) (ω : Ω) :
    truncatedRV X A n ω = if |X n ω| ≤ A then X n ω else 0

Uses 1 · Used by 8

Statement usesTruncation of a random variable

Used byTruncation is bounded by a nonnegative cutoff · Truncation is bounded by the absolute cutoff · Almost sure convergence of centered truncated sums · The Summable-means necessity claim in v1 is false · Canonical truncation factors through scalar truncation · Truncation fixes values within the cutoff · Truncation vanishes outside the closed band · Canonical truncation preserves nonnegativity

TheoremTruncation preserves measurability#✓fully proved

The canonical truncation of a measurable random variable is measurable.

theorem measurable_truncatedRV {X : ℕ → Ω → ℝ} (hX : ∀ n, Measurable (X n))
    (A : ℝ) (n : ℕ) : Measurable (truncatedRV X A n)

Uses 1 · Used by 3

Statement usesTruncation of a random variable

Used byMeasurability of a truncated random variable · Measurability of scalar truncation · Kolmogorov three-series necessity, series (2)–(3)

TheoremTruncation preserves independence#✓fully proved

Truncation preserves independence.

theorem iIndepFun_truncatedRV {X : ℕ → Ω → ℝ} (hX : iIndepFun X μ) (A : ℝ) :
    iIndepFun (fun n => truncatedRV X A n) μ

Uses 1 · Used by 1

Statement usesTruncation of a random variable

Used byKolmogorov three-series necessity, series (2)–(3)

TheoremTruncation is bounded by a nonnegative cutoff#✓fully proved

A canonical truncation is bounded by a nonnegative cutoff in absolute value.

theorem abs_truncatedRV_le {X : ℕ → Ω → ℝ} {A : ℝ} (hA : 0 ≤ A) (n : ℕ) (ω : Ω) :
    |truncatedRV X A n ω| ≤ A

Uses 2 · Used by 1

Statement usesTruncation of a random variable

Proof usesFormula for the truncated random variable

Used byKolmogorov three-series necessity, series (2)–(3)

TheoremTruncation is bounded by the absolute cutoff#✓fully proved

A canonical truncation is bounded by the absolute value of any cutoff.

theorem abs_truncatedRV_le_abs {X : ℕ → Ω → ℝ} (A : ℝ) (n : ℕ) (ω : Ω) :
    |truncatedRV X A n ω| ≤ |A|

Uses 2 · Used by 3

Statement usesTruncation of a random variable

Proof usesFormula for the truncated random variable

Used byMean bound for a truncated random variable · Truncated random variables lie in every Lp space · Variance bound for a truncated random variable

TheoremTruncation fixes values within the cutoff#✓fully proved

Truncation fixes points inside or on the cutoff.

theorem truncatedRV_eq_of_abs_le {X : ℕ → Ω → ℝ} {A : ℝ} {n : ℕ} {ω : Ω}
    (h : |X n ω| ≤ A) : truncatedRV X A n ω = X n ω

Uses 2 · Used by 3

Statement usesTruncation of a random variable

Proof usesFormula for the truncated random variable

Used byTruncation preserves almost-sure limits of bounded partial sums · Truncation leaves a family bounded by the cutoff unchanged · Scalar truncation fixes values within the cutoff

TheoremAlmost sure convergence of centered truncated sums#✓fully proved

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 ae_tendsto_centered_of_indep_summableVar [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ} (hX_meas : ∀ n, Measurable (X n))
    (hX_indep : iIndepFun X μ) {A : ℝ} (hA : A > 0)
    (h3 : Summable fun n =>
      variance (fun ω => (X n ω) * Set.indicator {ω | |X n ω| ≤ A} 1 ω) μ) :
    ∀ᵐ ω ∂μ, ∃ c, Tendsto (fun n =>
      ∑ i ∈ Finset.range n, (truncatedRV X A i ω -
        ∫ ω', (X i ω') * Set.indicator {ω' | |X i ω'| ≤ A} 1 ω' ∂μ)) atTop (nhds c)

Uses 4 · Used by 1

Statement usesTruncation of a random variable

Proof usesFormula for the truncated random variable · Almost-sure convergence of L¹-bounded sums of independent centered variables · \(L^1\) norm bounded by the square root of the second moment

Used byTruncated sums converge almost surely

TheoremTruncations eventually agree with the variables#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a probability space \((\Omega, P)\), let \(A\) be a real number, and let \(Y_n = X_n \mathbf{1}_{\{|X_n| \le A\}}\) be the truncation of \(X_n\) at \(A\). If \(\sum_n P(|X_n| > A) < \infty\), then for almost every \(\omega\) we have \(X_n(\omega) = Y_n(\omega)\) for all sufficiently large \(n\).

This follows from the first Borel–Cantelli lemma.

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

Uses 1 · Used by 2

Statement usesTruncation of a random variable

Used byKolmogorov's three-series theorem (sufficiency direction) · Kolmogorov three-series necessity, series (2)–(3)

TheoremEventually equal series inherit almost-everywhere convergence#✓fully proved

Let \(\mu\) be a measure on \(\Omega\) and let \(f_n, g_n : \Omega \to \mathbb{R}\) (\(n \ge 0\)) be functions such that for \(\mu\)-almost every \(\omega\) we have \(f_n(\omega) = g_n(\omega)\) for all sufficiently large \(n\). If there is a function \(S : \Omega \to \mathbb{R}\) with \(\sum_{i < n} f_i(\omega) \to S(\omega)\) as \(n \to \infty\) for \(\mu\)-almost every \(\omega\), then there is a function \(T : \Omega \to \mathbb{R}\) with \(\sum_{i < n} g_i(\omega) \to T(\omega)\) as \(n \to \infty\) for \(\mu\)-almost every \(\omega\).

theorem ae_tendsto_of_ae_eventually_eq_and_ae_tendsto
    {f g : ℕ → Ω → ℝ}
    (hfg : ∀ᵐ ω ∂μ, ∀ᶠ n in atTop, f n ω = g n ω)
    (hf : ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => f i ω)) atTop (nhds (S ω))) :
    ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => g i ω)) atTop (nhds (S ω))

Used by 3

Used byTruncation preserves almost-sure limits of bounded partial sums · Kolmogorov's three-series theorem (sufficiency direction) · Kolmogorov three-series necessity, series (2)–(3)

TheoremTruncated sums converge almost surely#✓fully proved

Let \(X_0, X_1, \dots\) be independent real random variables on a probability space \((\Omega, P)\), let \(A > 0\), and let \(Y_n = X_n \mathbf{1}_{\{|X_n| \le A\}}\) be the truncation of \(X_n\) at \(A\). If the series \(\sum_n E[Y_n]\) converges absolutely and \(\sum_n \operatorname{Var}(Y_n) < \infty\), then there is a function \(S : \Omega \to \mathbb{R}\) with \(\sum_{i < n} Y_i(\omega) \to S(\omega)\) as \(n \to \infty\) for almost every \(\omega\).

This combines the convergence of the centered truncated sums with the convergence of the series of means.

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

Uses 2 · Used by 1

Statement usesTruncation of a random variable

Proof usesAlmost sure convergence of centered truncated sums

Used byKolmogorov's three-series theorem (sufficiency direction)

TheoremKolmogorov's three-series theorem (sufficiency direction)#✓fully proved

Let \(X_0, X_1, \dots\) be independent real random variables on a probability space \((\Omega, P)\), fix \(A > 0\), and write \(Y_n = X_n \mathbf{1}_{\{|X_n| \le A\}}\) for the truncations. If \(\sum_n P(|X_n| > A) < \infty\), the series \(\sum_n E[Y_n]\) converges absolutely, and \(\sum_n \operatorname{Var}(Y_n) < \infty\), then there is a function \(S : \Omega \to \mathbb{R}\) with \(\sum_{i < n} X_i(\omega) \to S(\omega)\) as \(n \to \infty\) for almost every \(\omega\); that is, \(\sum_n X_n\) converges almost surely.

The classical theorem only requires the series \(\sum_n E[Y_n]\) to converge; here it must converge absolutely.

theorem kolmogorov_three_series_sufficiency
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ} (hX_meas : ∀ n, Measurable (X n))
    (hX_indep : iIndepFun (m := fun _ => inferInstance) X μ)
    (A : ℝ) (hA : A > 0)
    (h1 : (∑' n, μ {ω | |X n ω| > A}) < ⊤)
    (h2 : Summable fun n => ∫ ω, (X n ω) * Set.indicator {ω | |X n ω| ≤ A} 1 ω ∂μ)
    (h3 : Summable fun n =>
      variance (fun ω => (X n ω) * Set.indicator {ω | |X n ω| ≤ A} 1 ω) μ) :
    ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Filter.Tendsto (fun n =>
      (Finset.range n).sum (fun i => X i ω))
      Filter.atTop (nhds (S ω))

Uses 4

Proof usesTruncations eventually agree with the variables · Eventually equal series inherit almost-everywhere convergence · Truncated sums converge almost surely · Truncation of a random variable

TheoremKolmogorov three-series theorem, necessity, first series#✓fully proved

Let \((X_n)_{n \ge 0}\) be a sequence of independent measurable real random variables on a probability space \((\Omega, \mu)\) whose partial sums converge almost surely: there is a function \(S : \Omega \to \mathbb{R}\) such that \(\sum_{i < n} X_i(\omega) \to S(\omega)\) as \(n \to \infty\) for \(\mu\)-almost every \(\omega\). Then for every \(A > 0\) the tail probabilities are summable: \(\sum_n \mu(\{\omega : |X_n(\omega)| > A\}) < \infty\).

Proof: argue by contradiction via the second Borel–Cantelli lemma. If the tail probabilities summed to \(\infty\), the events \(\{|X_n| > A\}\) would occur infinitely often with probability one; but almost-sure convergence of the partial sums forces \(X_n \to 0\) almost surely, hence eventually \(|X_n| \le A\).

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

Used by 2

Used byDivergent tail probabilities prevent almost-sure convergence of partial sums · Kolmogorov three-series necessity, series (2)–(3)

TheoremDivergent tail probabilities prevent almost-sure convergence of partial sums#✓fully proved

Let \((X_n)_{n \ge 0}\) be a sequence of independent measurable real random variables on a probability space \((\Omega, \mu)\), and let \(A > 0\). If \(\sum_n \mu(\{\omega : |X_n(\omega)| > A\}) = \infty\), then there is no function \(S : \Omega \to \mathbb{R}\) such that, for \(\mu\)-almost every \(\omega\), the partial sums \(\sum_{i < n} X_i(\omega)\) converge to \(S(\omega)\) as \(n \to \infty\).

theorem not_ae_tendsto_partial_sum_of_tsum_tail_prob_eq_top
    [IsProbabilityMeasure μ]
    {X : ℕ → Ω → ℝ} (hX_meas : ∀ n, Measurable (X n))
    (hX_indep : iIndepFun X μ) {A : ℝ} (hA : A > 0)
    (hdiv : (∑' n, μ {ω | A < |X n ω|}) = ⊤) :
    ¬ ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => X i ω)) atTop (nhds (S ω))

Uses 1

Proof usesKolmogorov three-series theorem, necessity, first series

DefinitionPair of coordinates from two independent copies#✓fully proved

The pair of the n-th coordinates of two independent copies.

def pairRV (Y : ℕ → Ω → ℝ) (n : ℕ) : Ω × Ω → ℝ × ℝ :=
  fun p => (Y n p.1, Y n p.2)

Used by 2

Used byThree-series necessity, second half of the variance step · Symmetrized random variable

DefinitionSymmetrized random variable#✓fully proved

The symmetrized variable Z n (ω, ω') = Y n ω - Y n ω'.

def symmRV (Y : ℕ → Ω → ℝ) (n : ℕ) : Ω × Ω → ℝ :=
  (fun p : ℝ × ℝ => p.1 - p.2) ∘ pairRV Y n

Uses 1 · Used by 1

Statement usesPair of coordinates from two independent copies

Used byThree-series necessity, second half of the variance step

TheoremExpectation of a product of independent functions factors#✓fully proved

If f and g are independent, the expectation of a product of functions of f and g factors.

theorem integral_mul_of_indep_comp {f g : Ω → ℝ} (h : IndepFun f g μ)
    {φ ψ : ℝ → ℝ} (hφ : Measurable φ) (hψ : Measurable ψ)
    (hf : AEStronglyMeasurable (φ ∘ f) μ) (hg : AEStronglyMeasurable (ψ ∘ g) μ) :
    ∫ ω, φ (f ω) * ψ (g ω) ∂μ = (∫ ω, φ (f ω) ∂μ) * (∫ ω, ψ (g ω) ∂μ)

Used by 1

Used byFourth-moment bound for sums of bounded independent variables

TheoremFourth-moment bound for sums of bounded independent variables#✓fully proved

Fourth-moment induction for sums of independent centered bounded random variables: E[S⁴] ≤ 3 E[S²]² + B² E[S²], together with the variance-of-sum identity and E[S] = 0.

theorem integral_pow_four_le {Z : ℕ → Ω → ℝ} (hZmeas : ∀ n, Measurable (Z n))
    (hZindep : iIndepFun Z μ) {B : ℝ} (hB : 0 ≤ B) (hZbdd : ∀ n ω, |Z n ω| ≤ B)
    (hZmean : ∀ n, ∫ ω, Z n ω ∂μ = 0) {m n : ℕ} (hmn : m ≤ n) :
    (∫ ω, (∑ k ∈ Finset.Ico m n, Z k ω) ^ 4 ∂μ ≤
      3 * (∫ ω, (∑ k ∈ Finset.Ico m n, Z k ω) ^ 2 ∂μ) ^ 2 +
        B ^ 2 * (∫ ω, (∑ k ∈ Finset.Ico m n, Z k ω) ^ 2 ∂μ)) ∧
    (∫ ω, (∑ k ∈ Finset.Ico m n, Z k ω) ^ 2 ∂μ =
      ∑ k ∈ Finset.Ico m n, ∫ ω, (Z k ω) ^ 2 ∂μ) ∧
    (∫ ω, (∑ k ∈ Finset.Ico m n, Z k ω) ∂μ = 0)

Uses 1 · Used by 1

Proof usesExpectation of a product of independent functions factors

Used byThree-series necessity, second half of the variance step

TheoremThree-series necessity, second half of the variance step#✓fully proved

For a uniformly bounded independent sequence whose partial sums converge almost surely, the variances are summable. Proved by symmetrization: the symmetrized sums are centered, so Paley–Zygmund gives a uniform lower bound on block-tail probabilities, contradicting convergence in measure unless the variances are summable.

theorem summable_variance_of_bounded_ae_tendsto {Y : ℕ → Ω → ℝ}
    (hYmeas : ∀ n, Measurable (Y n)) (hYindep : iIndepFun Y μ)
    {A : ℝ} (hA : 0 < A) (hYbdd : ∀ n ω, |Y n ω| ≤ A)
    (hYtend : ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => Y i ω)) atTop (nhds (S ω))) :
    Summable (fun n => variance (Y n) μ)

Uses 4 · Used by 1

Proof usesFourth-moment bound for sums of bounded independent variables · Pair of coordinates from two independent copies · Symmetrized random variable · The Paley–Zygmund inequality

Used byKolmogorov three-series necessity, series (2)–(3)

TheoremMean step of three-series necessity#✓fully proved

For a uniformly bounded independent sequence with summable variances whose partial sums converge almost surely, the partial sums of the means converge (to some limit). Proved by centering and applying the canonical centered-sum convergence theorem with an L¹ bound from the total variance. The mean partial sums are the difference of the two convergent series at a single sample point.

theorem tendsto_sum_integral_of_bounded_ae_tendsto {Y : ℕ → Ω → ℝ}
    (hYmeas : ∀ n, Measurable (Y n)) (hYindep : iIndepFun Y μ)
    {A : ℝ} (hYbdd : ∀ n ω, |Y n ω| ≤ A)
    (hVar : Summable (fun n => variance (Y n) μ))
    (hYtend : ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => Y i ω)) atTop (nhds (S ω))) :
    ∃ L : ℝ, Tendsto (fun n => ∑ k ∈ Finset.range n, ∫ ω, Y k ω ∂μ) atTop (nhds L)

Uses 2 · Used by 1

Proof usesAlmost-sure convergence of L¹-bounded sums of independent centered variables · \(L^1\) norm bounded by the square root of the second moment

Used byKolmogorov three-series necessity, series (2)–(3)

TheoremKolmogorov three-series necessity, series (2)–(3)#✓fully proved

If the partial sums of an independent sequence Xₙ converge almost surely, then for every A > 0 the truncations Yₙ = Xₙ · 1_{|Xₙ| ≤ A} have convergent mean partial sums and summable variances. This is the corrected form of v1's summable_mean_and_variance_of_ae_tendsto_ax: v1 claimed the means themselves are Summable, which is false (see summable_mean_necessity_false); only convergence of the mean partial sums holds. Series (1) uses the public theorem from ThreeSeriesTailProb.

theorem three_series_necessity_mean_variance {X : ℕ → Ω → ℝ}
    (hXmeas : ∀ n, Measurable (X n)) (hXindep : iIndepFun X μ)
    {A : ℝ} (hA : 0 < A)
    (hXtend : ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => X i ω)) atTop (nhds (S ω))) :
    (∃ L : ℝ, Tendsto (fun n => ∑ k ∈ Finset.range n,
      ∫ ω, truncatedRV X A k ω ∂μ) atTop (nhds L)) ∧
    Summable (fun n => variance (truncatedRV X A n) μ)

Uses 9

Statement usesTruncation of a random variable

Proof usesThree-series necessity, second half of the variance step · Mean step of three-series necessity · Truncation is bounded by a nonnegative cutoff · Truncations eventually agree with the variables · Eventually equal series inherit almost-everywhere convergence · Truncation preserves independence · Truncation preserves measurability · Kolmogorov three-series theorem, necessity, first series

TheoremThe Summable-means necessity claim in v1 is false#✓fully proved

The deterministic sequence X k ω = (-1)^k / (k + 1) on the one-point probability space (Unit, dirac ()) has converging partial sums, is constant (hence measurable and independent), agrees with its truncations at A = 1, and has all variances 0 — yet its means ∫ truncatedRV X 1 k = (-1)^k / (k + 1) are not Summable, since Summable.abs would force summability of the harmonic series. This is why the ported necessity theorem above states convergence of the mean partial sums rather than Summable of the means. The statement records convergence of both the original and the truncated partial sums: the truncated form is the hypothesis of v1's (false) unproved lemma, and the original form is what the corrected assembly theorem needs.

theorem summable_mean_necessity_false :
    ∃ (X : ℕ → Unit → ℝ) (A : ℝ), 0 < A ∧
      (∀ n, Measurable (X n)) ∧ iIndepFun X (Measure.dirac ()) ∧
      (∃ S : Unit → ℝ, ∀ᵐ ω ∂(Measure.dirac ()),
        Tendsto (fun n => (Finset.range n).sum (fun i => X i ω))
          atTop (nhds (S ω))) ∧
      (∃ S : Unit → ℝ, ∀ᵐ ω ∂(Measure.dirac ()),
        Tendsto (fun n => (Finset.range n).sum (fun i => truncatedRV X A i ω))
          atTop (nhds (S ω))) ∧
      ¬ Summable (fun n => ∫ ω, truncatedRV X A n ω ∂(Measure.dirac ()))

Uses 2

Statement usesTruncation of a random variable

Proof usesFormula for the truncated random variable

AbbreviationScalar truncation function#✓fully proved

Scalar truncation is canonical truncation of the identity sequence.

abbrev truncationFun (A : ℝ) : ℝ → ℝ :=
  truncatedRV (fun _ => id) A 0

Uses 1 · Used by 5

Statement usesTruncation of a random variable

Used byMeasurability of scalar truncation · Canonical truncation factors through scalar truncation · Scalar truncation fixes values within the cutoff · Scalar truncation vanishes beyond the cutoff · Scalar truncation preserves nonnegativity

TheoremTruncation vanishes outside the closed band#✓fully proved

Truncation of a value strictly outside the closed band is zero.

theorem truncatedRV_eq_zero_of_abs_gt {X : ℕ → Ω → ℝ} {A : ℝ} {n : ℕ} {ω : Ω}
    (h : A < |X n ω|) : truncatedRV X A n ω = 0

Uses 2 · Used by 1

Statement usesTruncation of a random variable

Proof usesFormula for the truncated random variable

Used byScalar truncation vanishes beyond the cutoff

TheoremCanonical truncation preserves nonnegativity#✓fully proved

Canonical truncation preserves nonnegativity.

theorem truncatedRV_nonneg_of_nonneg {X : ℕ → Ω → ℝ} {A : ℝ} {n : ℕ} {ω : Ω}
    (h : 0 ≤ X n ω) : 0 ≤ truncatedRV X A n ω

Uses 2 · Used by 1

Statement usesTruncation of a random variable

Proof usesFormula for the truncated random variable

Used byScalar truncation preserves nonnegativity

TheoremScalar truncation fixes values within the cutoff#✓fully proved

Scalar truncation fixes values inside or on the cutoff.

theorem truncationFun_eq_self_of_abs_le {A x : ℝ} (hx : |x| ≤ A) :
    truncationFun A x = x

Uses 2

Statement usesScalar truncation function

Proof usesTruncation fixes values within the cutoff

TheoremScalar truncation vanishes beyond the cutoff#✓fully proved

Scalar truncation kills values strictly outside the cutoff.

theorem truncationFun_eq_zero_of_abs_gt {A x : ℝ} (hx : A < |x|) :
    truncationFun A x = 0

Uses 2

Statement usesScalar truncation function

Proof usesTruncation vanishes outside the closed band

TheoremScalar truncation preserves nonnegativity#✓fully proved

Scalar truncation preserves nonnegativity.

theorem truncationFun_nonneg_of_nonneg {A x : ℝ} (hx : 0 ≤ x) :
    0 ≤ truncationFun A x

Uses 2

Statement usesScalar truncation function

Proof usesCanonical truncation preserves nonnegativity

TheoremCanonical truncation factors through scalar truncation#✓fully proved

Canonical truncation factors through its scalar specialization.

theorem truncatedRV_eq_comp (X : ℕ → Ω → ℝ) (A : ℝ) (n : ℕ) :
    truncatedRV X A n = truncationFun A ∘ X n

Uses 3

Statement usesTruncation of a random variable · Scalar truncation function

Proof usesFormula for the truncated random variable

TheoremMeasurability of scalar truncation#✓fully proved

The scalar specialization of canonical truncation is measurable.

theorem measurable_truncationFun (A : ℝ) : Measurable (truncationFun A)

Uses 2

Statement usesScalar truncation function

Proof usesTruncation preserves measurability

TheoremMeasurability of a truncated random variable#✓fully proved

Canonical truncation needs measurability only of the selected variable.

theorem measurable_truncatedRV_of_measurable {X : ℕ → Ω → ℝ}
    (n : ℕ) (hX : Measurable (X n)) (A : ℝ) :
    Measurable (truncatedRV X A n)

Uses 2 · Used by 2

Statement usesTruncation of a random variable

Proof usesTruncation preserves measurability

Used byTruncated random variables lie in every Lp space · Variance bound for a truncated random variable

TheoremTruncation leaves a family bounded by the cutoff unchanged#✓fully proved

A family bounded by the cutoff is unchanged by canonical truncation.

theorem truncatedRV_eq_of_bdd
    {Y : ℕ → Ω → ℝ} {A : ℝ} (hY : ∀ n ω, |Y n ω| ≤ A) (n : ℕ) :
    truncatedRV Y A n = Y n

Uses 2

Statement usesTruncation of a random variable

Proof usesTruncation fixes values within the cutoff

TheoremTruncation preserves almost-sure limits of bounded partial sums#✓fully proved

A uniformly bounded family keeps its almost-sure partial-sum limit under canonical truncation, on the same measure.

theorem ae_tendsto_truncatedRV_of_bdd
    {Y : ℕ → Ω → ℝ} {A : ℝ} (hY : ∀ n ω, |Y n ω| ≤ A)
    (hY_tend : ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => Y i ω)) atTop (nhds (S ω))) :
    ∃ S : Ω → ℝ, ∀ᵐ ω ∂μ, Tendsto (fun n =>
      (Finset.range n).sum (fun i => truncatedRV Y A i ω)) atTop (nhds (S ω))

Uses 3

Statement usesTruncation of a random variable

Proof usesEventually equal series inherit almost-everywhere convergence · Truncation fixes values within the cutoff

TheoremTruncated random variables lie in every Lp space#✓fully proved

Canonical truncation is in every Lᵖ on a finite measure space.

theorem memLp_truncatedRV [IsFiniteMeasure μ] {X : ℕ → Ω → ℝ}
    (n : ℕ) (hX : Measurable (X n)) (A : ℝ) (p : ℝ≥0∞) :
    MemLp (truncatedRV X A n) p μ

Uses 3 · Used by 1

Statement usesTruncation of a random variable

Proof usesTruncation is bounded by the absolute cutoff · Measurability of a truncated random variable

Used byIntegrability of truncated random variables

TheoremIntegrability of truncated random variables#✓fully proved

Canonical truncation is integrable on a finite measure space.

theorem integrable_truncatedRV [IsFiniteMeasure μ] {X : ℕ → Ω → ℝ}
    (n : ℕ) (hX : Measurable (X n)) (A : ℝ) :
    Integrable (truncatedRV X A n) μ

Uses 2 · Used by 1

Statement usesTruncation of a random variable

Proof usesTruncated random variables lie in every Lp space

Used byMean bound for a truncated random variable

TheoremVariance bound for a truncated random variable#✓fully proved

The variance of canonical truncation is at most A².

theorem variance_truncatedRV_le [IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ}
    (n : ℕ) (hX : Measurable (X n)) (A : ℝ) :
    variance (truncatedRV X A n) μ ≤ A ^ 2

Uses 3

Statement usesTruncation of a random variable

Proof usesTruncation is bounded by the absolute cutoff · Measurability of a truncated random variable

TheoremMean bound for a truncated random variable#✓fully proved

The absolute mean of canonical truncation is at most |A|.

theorem abs_integral_truncatedRV_le [IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ}
    (n : ℕ) (hX : Measurable (X n)) (A : ℝ) :
    |∫ ω, truncatedRV X A n ω ∂μ| ≤ |A|

Uses 3

Statement usesTruncation of a random variable

Proof usesTruncation is bounded by the absolute cutoff · Integrability of truncated random variables

39 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.