Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
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.

Under square summability, the signed product of (1+p_n) converges iff the series of p_n converges

Statement

Let (pn)(p_n) be a real sequence such that ∑npn2\sum_n p_n^2 converges. Then ∏n(1+pn) converges⟺∑npn converges.\prod_n(1+p_n)\text{ converges}\quad\Longleftrightarrow\quad\sum_n p_n\text{ converges}. The product uses the tail convention of Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors, so finitely many zero factors are allowed.

Facts & Assumptions

Given: A real sequence (pn)(p_n) with ∑npn2\sum_n p_n^2 convergent.

[L1]

A convergent series has terms tending to zero (If a series converges then its terms tend to 00).

[L2]

log⁡(1+t)=t+∑k≥2(−1)k+1tk/k\log(1+t)=t+\sum_{k\ge2}(-1)^{k+1}t^k/k for ∣t∣<1|t|<1 ([The power series for log(1+x) on (-1,1], including the Abel endpoint](/item/thm-log-one-plus-x-power-series)).

[L3]

Direct comparison and absolute convergence give convergence of a series dominated by a convergent nonnegative series (If 0≤ak≤bk0 \le a_k \le b_k eventually, convergence of ∑bk\sum b_k gives convergence of ∑ak\sum a_k, and divergence of ∑ak\sum a_k gives divergence of ∑bk\sum b_k, If ∑∣ak∣\sum |a_k| converges then ∑ak\sum a_k converges).

[L4]

Convergent series are closed under termwise addition and subtraction, and deleting a finite initial segment preserves convergence (Convergent series add and scale termwise, A series converges iff each of its tail series converges, and the sum splits as sNs_N plus the NN-th tail, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L5]

exp⁡(u+v)=exp⁡(u)exp⁡(v)\exp(u+v)=\exp(u)\exp(v), while exp⁡\exp and log⁡\log are continuous inverse functions on their stated domains (The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y)\exp(x+y)=\exp(x)\exp(y), The exponential function is strictly increasing, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L6]

An infinite product converges when a tail of nonzero factors has nonzero limiting tail products; initial factors may be arbitrary (Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors).

Proof

technique · direct
1.1

By [L1], choose NN such that ∣pn∣≤1/2|p_n|\le1/2 for n≥Nn\ge N; then 1+pn≥1/2>01+p_n\ge1/2>0 on that tail.

L1choose
1.2

For ∣t∣≤1/2|t|\le1/2, the tail of the series in [L2] has absolute value at most ∑k≥2∣t∣k≤2t2\sum_{k\ge2}|t|^k\le2t^2, hence ∣log⁡(1+t)−t∣≤2t2|\log(1+t)-t|\le2t^2.

L2algebra
1.3

Conversely, a nonzero limit of those positive tail products has a logarithm; continuity of log⁡\log and the same finite-product identity make the tail logarithm partial sums converge.

L5L6
2.1

Applying step 1.2 to pnp_n and using [L3] shows that ∑n≥N(log⁡(1+pn)−pn)\sum_{n\ge N}(\log(1+p_n)-p_n) converges absolutely.

step 1.1step 1.2L3
3.1

By [L4], ∑npn\sum_n p_n converges if and only if ∑n≥Nlog⁡(1+pn)\sum_{n\ge N}\log(1+p_n) converges.

step 2.1L4
4.1

The mm-th tail product equals exp⁡(∑n=NN+m−1log⁡(1+pn))\exp(\sum_{n=N}^{N+m-1}\log(1+p_n)) by repeated use of [L5], so convergence of the logarithm series gives a nonzero tail-product limit.

step 3.1L5L6
5.1

Steps 3.1, 4.1, and 1.3 prove both directions, and [L6] makes finite initial zero factors harmless.

step 3.1step 4.1step 1.3L6∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 149 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources