TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Consistency of the IID Monte Carlo sample variance

Statement

Let $(Y_{i})_{i \geq 1}$ be a real IID sequence with $E [Y_{1}^{2}] < \infty$ , and write $μ = E [Y_{1}]$ and $σ^{2} = Var (Y_{1})$ . For $n \geq 2$ , define $s_{n}^{2} = (n - 1)^{- 1} \sum_{i = 1}^{n} (Y_{i} - {\overset{ˉ}{Y}}_{n})^{2}$ . Then $s_{n}^{2} \to σ^{2}$ almost surely. If $σ^{2} > 0$ , then ${\hat{s e}}_{n} / (σ / \sqrt{n}) \to 1$ almost surely.

Facts & Assumptions

Given: A real IID sequence $(Y_{i})_{i \geq 1}$ with $E [Y_{1}^{2}] < \infty$ .

[F1]

IID Monte Carlo sample mean, variance, and standard error: ${\overset{ˉ}{Y}}_{n} = n^{- 1} \sum_{i = 1}^{n} Y_{i}$ , $s_{n}^{2} = (n - 1)^{- 1} \sum_{i = 1}^{n} (Y_{i} - {\overset{ˉ}{Y}}_{n})^{2}$ for $n \geq 2$ , and ${\hat{s e}}_{n} = s_{n} / \sqrt{n}$ .

[F2]

Identical distribution and IID families: IID means common law and mutual independence.

[F3]

Arithmetic and lattice operations preserve measurability whenever they are defined: Products of measurable real functions are measurable, so the square map $x \mapsto x^{2}$ is Borel measurable.

[F4]

Measurable coordinatewise functions preserve independence: Applying a measurable function separately to each member of an independent family preserves independence.

[F5]

Change of variables for expectation: For a measurable $g$ with $g (X)$ integrable, $E [g (X)]$ is the integral of $g$ against the law of $X$ .

[F6]

Kolmogorov iid l1 strong law: For real IID variables with finite first absolute moment, their sample averages converge almost surely to their common expectation.

[F7]

Moments, variance, and covariance on a probability space: For square-integrable real $X$ , $Var (X) = E [(X - E [X])^{2}]$ .

[F8]

Linearity, monotonicity, and the modulus bound for expectation: Expectation is linear on integrable real random variables.

Proof

1.1F1F6givenalgebra

Since $∣ y ∣ \leq 1 + y^{2}$ for every real $y$ , the given second moment implies $E ∣ Y_{1} ∣ < \infty$ . Applying [F6] to the original IID sequence gives ${\overset{ˉ}{Y}}_{n} \to μ$ almost surely by [F1].

1.2F2F3F4F5F6given

The identity map on $(R, B (R))$ is measurable, so its pointwise product with itself is Borel measurable by [F3]; call this square map $q$ . Applying [F4] with $q$ preserves independence. For any Borel set $B$ , $P (Y_{i}^{2} \in B) = P (Y_{i} \in q^{- 1} (B))$ , so the common-law clause of [F2] gives a common law for the $Y_{i}^{2}$ . By [F5], their common finite expectation is $E [Y_{1}^{2}]$ . Thus [F6] applies to this IID sequence and gives $n^{- 1} \sum_{i = 1}^{n} Y_{i}^{2} \to E [Y_{1}^{2}]$ almost surely.

2.1F1F7F8step 1.1step 1.2algebra

Expanding the centered squares in [F1] gives $s_{n}^{2} = \frac{n}{n - 1} (n^{- 1} \sum_{i = 1}^{n} Y_{i}^{2} - {\overset{ˉ}{Y}}_{n}^{2})$ . Steps 1.1 and 1.2 imply that the bracket tends almost surely to $E [Y_{1}^{2}] - μ^{2}$ ; also $n / (n - 1) \to 1$ . By [F7] and [F8], $E [Y_{1}^{2}] - μ^{2} = E [(Y_{1} - μ)^{2}] = σ^{2}$ . Hence $s_{n}^{2} \to σ^{2}$ almost surely.

3.1F1step 2.1algebra∎

If $σ^{2} > 0$ , step 2.1 gives $s_{n}^{2} / σ^{2} \to 1$ almost surely. Both $s_{n}$ and $σ$ are nonnegative, so continuity of the square root gives $s_{n} / σ \to 1$ . By [F1], ${\hat{s e}}_{n} / (σ / \sqrt{n}) = s_{n} / σ$ , proving the relative standard-error consistency.

Depends on

Used by

Dependency tree · two levels

38 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

Art B. Owen, Monte Carlo Theory, Methods and Examples, Chapter 2 (standard reference, not scraped)
Rick Durrett, Probability: Theory and Examples, 5th ed. (standard reference, not scraped)