ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Lyapunov condition for nonidentical summands

Example

Assume AC. Take independent symmetric signs $ϵ_{n, k} \in {- 1, 1}$ , $1 \leq k \leq n$ , and set $X_{n, k} = k ϵ_{n, k}$ . With $s_{n}^{2} = \sum_{k = 1}^{n} k^{2}$ , the Lyapunov condition holds for $δ = 1$ , and $s_{n}^{- 1} \sum_{k = 1}^{n} X_{n, k} \Rightarrow N (0, 1)$ . In every row of length at least two the summand laws are distinct.

Facts & Assumptions

[F1]

The normalized third-moment condition implies the CLT with delta=1. Lyapunov central limit theorem.

[F2]

Under DC and countable choice independent copies of a two-point law exist. Countably many independent copies of a prescribed law exist.

[F3]

AC supplies those choice principles. AC supplies countable selections and prescribed serial paths.

Verification

Given: Assume AC. Take independent symmetric signs $ϵ_{n, k} \in {- 1, 1}$ , $1 \leq k \leq n$ , and set $X_{n, k} = k ϵ_{n, k}$ . With $s_{n}^{2} = \sum_{k = 1}^{n} k^{2}$ , the Lyapunov condition holds for $δ = 1$ , and $s_{n}^{- 1} \sum_{k = 1}^{n} X_{n, k} \Rightarrow N (0, 1)$ . In every row of length at least two the summand laws are distinct.

1.1

Use [F2]–[F3] on the law assigning mass 1/2 to each sign, and index its coordinates by $n (n - 1) / 2 + k$ for $1 \leq k \leq n$ . These indices are distinct across the array and exhaust the positive integers. Thus the required signs exist and are independent. Direct two-point integration gives $E X_{n, k} = (k - k) / 2 = 0$ , $E X_{n, k}^{2} = k^{2}$ and $E ∣ X_{n, k} ∣^{3} = k^{3}$ . Different k have disjoint supports ${- k, k}$ , so their laws differ.

F2F3

2.1

At least n/2 integers k in the row satisfy $k \geq n / 2$ , so $s_{n}^{2} \geq (n / 2) (n / 2)^{2} = n^{3} / 8$ . Also $\sum_{k = 1}^{n} k^{3} \leq n n^{3} = n^{4}$ . Hence $s_{n}^{- 3} \sum_{k} E ∣ X_{n, k} ∣^{3} \leq 8^{3 / 2} / \sqrt{n} \to 0$ . These bounds remain valid for n=1. The rows are centered, independent and have finite moments and positive s_n, so [F1] with delta=1 proves the assertion. AC is used by the copy construction and inherited in [F1].

step 1.1F1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Durrett, Probability: Theory and Examples, exercises after Theorem 3.4.10 (standard reference, not scraped)
Aldous and Chewi, Probability Theory notes, Corollary 6.2 (standard reference, not scraped)