Prove2Me

Proof of Theorem 3 — Ank>(2(3+ε)/(6+ε))k−1A_{n_k} > (2(3+\varepsilon)/(6+\varepsilon))^{k-1} from (4.11), (4.12), (4.14)

Proved
AzumaWeightedSums.StrongLaw.block_growth

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1probabilitysequences

Let (an)n≥1(a_n)_{n\ge1} be positive, An=a1+⋯+anA_n=a_1+\dots+a_n, ε>0\varepsilon>0, and let (nk)k≥1(n_k)_{k\ge1} be natural numbers satisfying

  1. (4.11) An1>2(3+ε)/(6+ε)A_{n_1} > 2(3+\varepsilon)/(6+\varepsilon);
  2. (4.12) an/An<ε/(6+ε)a_n/A_n < \varepsilon/(6+\varepsilon) for all n>n1n>n_1;
  3. (4.14) Ank−1<Ank≤(1+ε/3)Ank−1<Ank+1A_{n_{k-1}} < A_{n_k} \le (1+\varepsilon/3)A_{n_{k-1}} < A_{n_k+1} for every k≥2k\ge2.

Then

Ank>(2(3+ε)6+ε)k−1,k=1,2,…A_{n_k} > \Big(\frac{2(3+\varepsilon)}{6+\varepsilon}\Big)^{k-1}, \qquad k=1,2,\dots

Since 2(3+ε)/(6+ε)>12(3+\varepsilon)/(6+\varepsilon)>1, the block totals AnkA_{n_k} grow at least geometrically. Combined with (4.13) and (4.16), this makes the series ∑kP{max⁡nk<n≤nk+1Sˉn>εAnk}\sum_k P\{\max_{n_k<n\le n_{k+1}}\bar S_n>\varepsilon A_{n_k}\} converge, so the Borel–Cantelli lemma applies.

Formalization Note The sequence (nk)(n_k) is indexed by k≥1k\ge1; its value at k=0k=0 is unused. Monotonicity of (nk)(n_k) is not assumed; it follows from (4.14) and the positivity of (an)(a_n).

Preamble
import Mathlib
import Definitions.Def_AzumaWeightedSums_StrongLaw_ReversedSum
Formal statement
namespace AzumaWeightedSums.StrongLaw

/-- Growth of the blocks in the proof of Theorem 3 (Azuma 1967, p. 366): if `(a_n)` is positive,
`ε > 0`, and `(n_k)_{k ≥ 1}` satisfies (4.11) `A_{n_1} > 2(3+ε)/(6+ε)`,
(4.12) `a_n/A_n < ε/(6+ε)` for `n > n_1`, and
(4.14) `A_{n_{k-1}} < A_{n_k} ≤ (1 + ε/3) A_{n_{k-1}} < A_{n_k + 1}` for `k ≥ 2`, then
`A_{n_k} > (2(3+ε)/(6+ε))^{k-1}` for `k = 1, 2, …`. -/
theorem block_growth (a : ℕ → ℝ) (ha_pos : ∀ n : ℕ, 1 ≤ n → 0 < a n)
    (ε : ℝ) (hε : 0 < ε) (nk : ℕ → ℕ)
    (h411 : 2 * (3 + ε) / (6 + ε) < A a (nk 1))
    (h412 : ∀ n : ℕ, nk 1 < n → a n / A a n < ε / (6 + ε))
    (h414 : ∀ k : ℕ, 2 ≤ k →
        A a (nk (k - 1)) < A a (nk k) ∧ A a (nk k) ≤ (1 + ε / 3) * A a (nk (k - 1)) ∧
          (1 + ε / 3) * A a (nk (k - 1)) < A a (nk k + 1)) :
    ∀ k : ℕ, 1 ≤ k → (2 * (3 + ε) / (6 + ε)) ^ (k - 1) < A a (nk k) := by sorry

end AzumaWeightedSums.StrongLaw
Source
Azuma, Weighted sums of certain dependent random variables, Tôhoku Math. J. 19 (1967), p. 366, proof of Theorem 3 (display following (4.16))
Human review

  • Endorsed by Shuze Chen · Oct 5, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 5, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph