TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Classical bounded-sample mean baseline

Statement

Let $G$ be a finite real random variable taking values in a finite interval $[a, b]$ with $a \leq b$ , and let $X_{1}, \dots, X_{n}$ be independent copies of $G$ , with $n \geq 1$ . For ${\overline{X}}_{n} = n^{- 1} \sum_{i = 1}^{n} X_{i}$ and $μ = E [G]$ , $E [{\overline{X}}_{n}] = μ, Var ({\overline{X}}_{n}) = \frac{Var (G)}{n} \leq \frac{(b - a)^{2}}{4 n} .$ Consequently, for every $ε > 0$ , $\Pr (∣ {\overline{X}}_{n} - μ ∣ > ε) \leq \frac{(b - a)^{2}}{4 n ε^{2}} .$ The procedure uses exactly $n$ independent samples. If each draw and data load costs $C_{d r a w}$ and $C_{l o a d}$ , their total is $n (C_{d r a w} + C_{l o a d})$ ; arithmetic for the encoded values is an additional separately charged cost. When $a = b$ , every sample equals $μ = a$ and the failure probability is zero.

Facts & Assumptions

Given: A finite law, a finite random variable $G$ with $a \leq G \leq b$ , and independent copies $X_{1}, \dots, X_{n}$ with the same law as $G$ .

[F1]

Finite expectation-estimation task defines the target as the finite weighted expectation $μ = E [G]$ .

[F2]

Expectation of a real random variable on a finite probability space: $E [Y] = \sum_{ω \in Ω} Y (ω) w (ω)$ .

[F3]

Independent random elements: random variables are independent when their generated sigma-algebras are independent.

[F4]

Expectation factors over a finite product of mutually independent random variables: expectations factor for finite families of independent finite-valued real random variables.

[F5]

Moments, variance, and covariance on a probability space defines variance by $E [(Y - E Y)^{2}]$ and covariance by $E [(Y - E Y) (Z - E Z)]$ .

[F6]

Variance and covariance identities for random variables: $Cov (Y, Z) = E [Y Z] - E [Y] E [Z]$ and variance is bilinear as covariance.

[F7]

Variance of a finite sum as the sum of all variances and covariances gives the variance of a finite sum as the sum of variances and twice the sum of pairwise covariances.

[F8]

Linearity, monotonicity, and the modulus bound for expectation gives linearity of expectation for integrable random variables.

[F9]

Chebyshev's inequality for random variables: $\Pr (∣ Y - E Y ∣ \geq t) \leq Var (Y) / t^{2}$ for $t > 0$ .

[F10]

Expectation of a nonnegative or integrable random variable defines expectation by integration and the positive-negative decomposition. The nonnegative integral agrees with the simple integral on simple functions and The integral of a nonnegative simple function evaluate a nonnegative simple function by its finite sum of values times level-set probabilities on any probability space.

Proof

1.1givenF1F2F8F10algebra

For any finite-valued real random variable $Y$ on its given probability space, its positive and negative parts are nonnegative simple functions. By [F10], both have finite integrals, and subtraction gives $E [Y] = \sum_{t \in Y (Ω)} t \Pr (Y = t)$ . Thus all finite-valued variables below are integrable and square-integrable, and their general expectations equal their finite-law weighted sums, even when the underlying space is infinite. Since every $X_{i}$ has the law of $G$ , [F1], [F2], and [F10] identify $E [X_{i}]$ with the same finite weighted sum $μ$ . By [F8], $E [{\overline{X}}_{n}] = n^{- 1} \sum_{i} E [X_{i}] = μ$ .

1.2givenF3F4F5F6F10algebra

If $i \neq j$ , [F3]–[F4] give $E [X_{i} X_{j}] = E [X_{i}] E [X_{j}]$ for the general expectations; [F10] identifies each with the corresponding finite weighted sum. By [F5]–[F6], $Cov (X_{i}, X_{j}) = 0$ .

1.3givenF5F7F10algebra

Apply [F7] to the finite sum; [F10] identifies the expectations defining all variances and covariances with their finite weighted sums. Since each $X_{i}$ has the law of $G$ , $Var ({\overline{X}}_{n}) = n^{- 2} \sum_{i} Var (X_{i}) = Var (G) / n$ .

1.4givenF2F5F8F10algebra

Put $c = (a + b) / 2$ . Pointwise, $∣ G - c ∣ \leq (b - a) / 2$ , so [F2] and [F10] give $E [(G - c)^{2}] \leq (b - a)^{2} / 4$ for the finite weighted-sum expectation. Expanding the square and using [F5], [F8], and [F10] yields $E [(G - c)^{2}] = Var (G) + (μ - c)^{2}$ ; hence $Var (G) \leq (b - a)^{2} / 4$ . This also covers $a = b$ , when both sides are zero.

2.1step 1.3step 1.4algebra

Substituting step 1.4 into step 1.3 proves the stated variance bound.

3.1givenF9F10step 1.1step 2.1algebra

For $ε > 0$ , [F10] identifies the expectation and variance of the finite random variable ${\overline{X}}_{n}$ with those used by [F9]. Thus [F9] applied to ${\overline{X}}_{n}$ and step 1.1 bounds the probability of $∣ {\overline{X}}_{n} - μ ∣ \geq ε$ by $Var ({\overline{X}}_{n}) / ε^{2}$ . The event with strict inequality is a subset, so step 2.1 gives the displayed failure bound.

4.1givenconstructalgebra∎

Exactly $n$ independent draws are taken by hypothesis; summing their declared draw and load costs gives $n (C_{d r a w} + C_{l o a d})$ . The $n - 1$ additions and one division used for the mean are encoded arithmetic operations and remain separate costs.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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

Ashley Montanaro, Quantum speedup of Monte Carlo methods, Section 1 (standard reference, not scraped)
C. M. Grinstead and J. L. Snell, Introduction to Probability, 2nd ed., Sections 1.2 and 6.1 (standard reference, not scraped)
J. Matoušek and J. Vondrák, The Probabilistic Method, Lemma 5.1.3 (standard reference, not scraped)