ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

An infinite-mean law requiring diverging centering

Example

Assume countable choice and dependent choice. Let $X \geq e$ have survival function $P (X > x) = 1 / (x \log x)$ for $x \geq e$ , with an atom of mass $1 - 1 / e$ at $e$ . For IID copies $(X_{k})$ , the untruncated mean is infinite but $S_{n} / n - μ_{n} ⟶ 0 in probability, μ_{n} = e + \log \log n - \frac{1}{\log n} (n \geq e) .$ Here $μ_{n} = E [X 1_{{X \leq n}}]$ ; for integer $n < e$ set $μ_{n} = 0$ . More generally, the survival family $1 / [x (\log x)^{α}]$ for $x \geq e$ , $α \geq 0$ , has infinite second moment for every $α$ , finite first moment exactly for $α > 1$ , and admits deterministic weak-law centering exactly for $α > 0$ .

Facts & Assumptions

[F1]

Exact tail criterion for a truncated-centered IID weak law: For IID real random variables $(X_{n})_{n \geq 1}$ and $S_{n} = \sum_{k = 1}^{n} X_{k}$ , there exist deterministic real constants $(μ_{n})$ with $S_{n} / n - μ_{n} \to 0$ in probability if and only if $n P (∣ X_{1} ∣ > n) ⟶ 0.$ When this condition holds, $μ_{n} = E [X_{1} 1_{{∣ X_{1} ∣ \leq n}}]$ works. Neither existence of an untruncated mean nor convergence of $(μ_{n})$ is asserted.

[F2]

Countably many independent copies of a prescribed law exist: Assume countable choice and dependent choice. Every probability measure $ν$ on $(S, Σ)$ is the common law of a countable independent family of $S$ -valued random elements.

[F3]

Layer-cake formulas for random variables: Let $(Ω, F, P)$ be a probability space. 1. If $X : Ω \to [0, + \infty]$ is measurable, then $E [X] = \int_{0}^{\infty} P (X > t) d t,$ where the right-hand side may be $+ \infty$ . 2. If $X$ is an integrable real random variable, then $E [X] = \int_{0}^{\infty} P (X > t) d t - \int_{0}^{\infty} P (X < - t) d t .$

[F4]

Probability laws correspond to distribution functions: Assume the Axiom of Countable Choice. 1. Let $X$ be a real random variable, let $P_{X}$ be its law, and let $F_{X} (x) = P (X \leq x)$ . Then $F_{X}$ is nondecreasing and right-continuous, satisfies $\lim_{x \to - \infty} F_{X} (x) = 0, \lim_{x \to + \infty} F_{X} (x) = 1,$ and obeys $P_{X} ((a, b]) = F_{X} (b) - F_{X} (a) (a < b) .$ 2. Conversely, if $F : R \to R$ is nondecreasing and right-continuous with $\lim_{x \to - \infty} F (x) = 0, \lim_{x \to + \infty} F (x) = 1,$ then there is a unique Borel probability measure $μ$ on $R$ such that $μ ((a, b]) = F (b) - F (a) (a < b),$ equivalently $F (x) = μ ((- \infty, x]) (x \in R) .$

Verification

Given: The construction and assumptions above.

1.1

Define $F (x) = 0$ for $x < e$ and $F (x) = 1 - 1 / [x (\log x)^{α}]$ for $x \geq e$ , where $α \geq 0$ . It is nondecreasing and right-continuous with limits zero and one at the two infinities. Its jump at $e$ is $1 - 1 / e$ . The distribution-function theorem constructs its Borel probability law (using countable choice); under countable choice and dependent choice the countable-copy result constructs IID variables with it.

F4F2givenalgebra

2.1

Layer cake gives $E X = e + \int_{e}^{\infty} [x (\log x)^{α}]^{- 1} d x = e + \int_{1}^{\infty} u^{- α} d u$ . This is finite exactly for $α > 1$ , when it equals $e + 1 / (α - 1)$ . Applying layer cake to $X^{2}$ and substituting $t = x^{2}$ gives $E X^{2} = e^{2} + 2 \int_{e}^{\infty} (\log x)^{- α} d x = \infty$ : eventually $(\log x)^{α} \leq x$ , so the last integrand dominates $1 / x$ . The comparison follows from $u^{α} \leq e^{u}$ for large $u$ , for example by an exponential-series term of integer degree greater than $α$ .

F3step 1.1algebra

2.2

For $n \geq e$ the tail quantity is $n P (X > n) = (\log n)^{- α}$ . It tends to zero exactly for $α > 0$ , whereas for $α = 0$ it equals one. Both directions of the truncated-centering criterion therefore give exactly the asserted centering range, even in the infinite-mean cases $0 < α \leq 1$ .

F1step 1.1algebra

3.1

For $α = 1$ use the pointwise identity $\min (X, n) = X 1_{{X \leq n}} + n 1_{{X > n}}$ . Layer cake for the bounded minimum gives $μ_{n} = \int_{0}^{n} P (X > t) d t - n P (X > n) = e + \log \log n - 1 / \log n$ for real $n \geq e$ . At $n = e$ this is $e - 1$ , exactly the contribution of the atom; below $e$ the zero truncation is zero. These finite centers work by the preceding step, although $E X = \infty$ and $μ_{n} \sim \log \log n \to \infty$ .

F3step 2.1step 2.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

Example 4.7, pp. 3–4, alpha=1 with endpoint correction (standard reference, not scraped)