Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

Finite variance logarithmic rate for iid sums

Statement

If IID real variables have mean μ and finite variance v, then for every ε>0, (Sn−nμ)/(n(log⁡n)1/2+ε)→0 almost surely, with the displayed normalization used for n≥2.

Facts & Assumptions

[F1]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: The function log⁡:(0,∞)→R is continuous and strictly increasing, is onto R, and satisfies, for x,y>0, log⁡(xy)=log⁡x+log⁡y,log⁡(x/y)=log⁡x−log⁡y,log⁡(1/x)=−log⁡x. Also log⁡1=0.

[F2]

Continuity and derivatives of positive-base real powers: For a>0, the function x↦ax is continuous on R and (ax)′=axlog⁡a. For α∈R, the function x↦xα is continuous and differentiable on (0,∞), with (xα)′=αxα−1.

[F3]

The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents: For a,b>0 and r,s∈R, ar+s=aras,(ab)r=arbr,(a/b)r=ar/br,(ar)s=ars.

[F4]

The p-series for a real exponent p converges exactly when p is greater than one: For every real p, ∑k≥11kp converges⟺p>1.

0  ≤  ak  ≤  bkfor all k≥K.

Then:

  1. if ∑bk converges then ∑ak converges (def-series);
  2. if ∑ak diverges then ∑bk diverges.

The same statement holds verbatim for series with a general starting index m, applied to the shifted sequences of def-series.

The hypothesis is on the terms from some index on, not on all of them: finitely many terms of either sequence may violate it, or be negative, without affecting the conclusion. What may not be dropped is nonnegativity of (ak) from that index on.

[F6]

Strong law under summable normalized variances: Let (Xn)n≥1 be independent square-integrable real random variables. Let 0<bn be deterministic and nondecreasing with bn→∞. If ∑n≥1Var⁡(Xn)bn2<∞, then 1bn∑k=1n(Xk−EXk)⟶0almost surely. In particular, for IID centered square-integrable variables and any ε>0, Sn/[n(log⁡n)1/2+ε]→0 almost surely (the displayed normalization is used for n≥2).

Proof

Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.

1.1F1F2

Fix ε>0 and put q=1/2+ε. By F1, log n>0 for n≥2. The derivatives in F2 show that positive powers are increasing; thus bn=n(log⁡n)q is positive and increasing for n≥2 and tends to infinity. Set b1=b2 to obtain a positive nondecreasing sequence at every index.

1.2F3F4F5

Using integer powers of 2 and F3, for 2k≤n<2k+1 with k≥1, 1/[n(log⁡n)1+2ε]≤2−k(klog⁡2)−1−2ε. There are 2k terms in this block, so its sum is at most (log⁡2)−1−2εk−1−2ε. F4 and F5 bound all partial sums of the nonnegative block series, because 1+2epsilon>1. Therefore ∑nv/bn2<∞, including the single finite n=1 term.

2.1F6step 1.2∎

The original variables are independent and square-integrable. Step 1.1 and step 1.2 verify all hypotheses of the general normalized-variance conclusion of F6. It gives (Sn−nμ)/bn→0 almost surely, as required for the arbitrarily fixed ε.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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