Alphabeta Math
LemmaStatement: 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.

Summability of truncated normalized variances

Statement

For identically distributed integrable real (Xn) and Yn=Xn1{∣Xn∣≤n}, ∑n≥1Var⁡(Yn)/n2≤2E∣X1∣<∞. No independence is required.

Facts & Assumptions

[F1]

Variance and covariance identities for random variables: Let X,Y be square-integrable real random variables on one probability space. Then Var⁡(X)=E[X2]−E[X]2, Cov⁡(X,Y)=E[XY]−E[X]E[Y]. Moreover, covariance is symmetric and bilinear on finite linear combinations. On finite full-power-set probability spaces these formulas reduce to the published finite identities.

[F2]

Change of variables for expectation: Let X:(Ω,F,P)→(S,Σ) be a random element, let PX be its law, and let g:(S,Σ)→R or g:(S,Σ)→C be measurable.

  1. If g≥0, then E[g(X)]=∫Sg dPX.
  2. If g(X) is integrable, then g is integrable with respect to PX and the same formula holds: E[g(X)]=∫Sg dPX.
[F3]

Integer part: for every real x there is exactly one integer m with m≤x<m+1: Identify Z with its canonical copy inside R, along the embeddings N→Z→Q→R (lem-nat-embeds-int, lem-int-embeds-rat, lem-rat-embeds-dense, def-integers). Then for every real x there is exactly one integer m with

m  ≤  x  <  m+1.

It is written ⌊x⌋ and called the integer part, or floor, of x.

Two independent ingredients are needed and neither may be dropped. Existence is the Archimedean property (thm-of-archimedean) together with the well-ordering of N (thm-well-ordering-principle): the first says that x is caught between two integers at all, the second picks the least integer above x. Uniqueness is the discreteness of Z: no integer lies strictly between m and m+1.

This lemma is stated once here and reused. It is what turns "the nearest integer to x" from a picture into an object, and the companion page's oscillator ψ(x)=inf⁡n∈Z∣x−n∣ is computed from it in one line.

[F4]

Monotone convergence for the integral: Let 0≤f1≤f2≤⋯ be measurable and suppose fn(x)↑f(x) for every x. Then ∫fn dμ↑∫f dμ.

Proof

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

1.1F1F2

The truncations satisfy ∣Yn∣≤n, so they are square-integrable. The variance identity F1 yields Var⁡(Yn)≤EYn2. By the common law and F2, the latter is E[∣X1∣21{∣X1∣≤n}].

1.2F3

For t>1 put m=⌈t⌉=−⌊−t⌋, as supplied by F3. Then m−1<t≤m and ∑n≥mn−2≤m−2+∑n>m((n−1)−1−n−1)=m−2+m−1≤2/t. For 0≤t≤1, the same telescoping bound from n=1 gives t2∑n≥1n−2≤2t2≤2t. Thus in all cases ∑n≥1t21{t≤n}/n2≤2t.

2.1F4step 1.2step 1.1∎

Apply F4 to the increasing finite sums of the nonnegative functions in step 1.2 evaluated at ∣X1∣. Combining step 1.1 and step 1.2 gives ∑nVar⁡(Yn)/n2≤E∑n∣X1∣21{∣X1∣≤n}/n2≤2E∣X1∣.

Depends on

Used by

Dependency tree · two levels

63 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