TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Conditional variance of independent and without-replacement minibatches

Statement

Let $n, d \geq 1$ , let $(Ω, F, (F_{k})_{k \geq 0}, P)$ be a discrete filtered probability space, and fix $k$ . Let $f_{i} : R^{d} \to R$ be continuously differentiable, let $x : Ω \to R^{d}$ be $F_{k}$ -measurable, and suppose each $g_{i} = \nabla f_{i} (x)$ is square-integrable. Define $F = n^{- 1} \sum_{i} f_{i}$ , $\overset{ˉ}{g} = n^{- 1} \sum_{i} g_{i} = \nabla F (x)$ by Gradient of a finite sum is the finite sum of gradients, and

σ^{2} (x) = \frac{1}{n} \sum_{i = 1}^{n} ∥ g_{i} - \overset{ˉ}{g} ∥_{2}^{2} .

For an integer $b \geq 1$ , draw $I_{1}, \dots, I_{b}$ as mutually independent uniform indices from ${1, \dots, n}$ , with the whole index vector independent of $F_{k}$ , and set $G_{b} = b^{- 1} \sum_{j = 1}^{b} g_{I_{j}}$ . Then

$E [G_{b} ∣ F_{k}] = \overset{ˉ}{g}, E [∥ G_{b} - \overset{ˉ}{g} ∥_{2}^{2} ∣ F_{k}] = \frac{σ^{2} (x)}{b} .$

For sampling without replacement, let $S$ be a uniform subset of ${1, \dots, n}$ of size $b$ , independent of $F_{k}$ , and set $G_{S} = b^{- 1} \sum_{i \in S} g_{i}$ . If $n > 1$ and $1 \leq b \leq n$ , then

$E [G_{S} ∣ F_{k}] = \overset{ˉ}{g}, E [∥ G_{S} - \overset{ˉ}{g} ∥_{2}^{2} ∣ F_{k}] = \frac{n - b}{b (n - 1)} σ^{2} (x) .$

When $n = 1$ , the without-replacement case requires $b = 1$ ; both estimators equal $\overset{ˉ}{g}$ and both errors are zero.

Facts & Assumptions

Given: The discrete filtered probability space Filtration and filtered probability space, the time $k$ , the $F_{k}$ -measurable point and square-integrable gradients, and the two sampling laws in the Statement. Vector conditional expectations mean coordinatewise scalar conditional expectations.

[A1]

The Axiom of Choice: assume AC for conditional-expectation classes.

[F1]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: stochastic-gradient conditional expectations are taken with respect to the current filtration, and AC is assumed for their existence.

[F2]

Filtration and filtered probability space: $F_{k}$ is a sigma-algebra and $F_{k} \subseteq F$ .

[F3]

Conditional expectation as an ae class: under AC, conditional expectations of integrable random variables exist as almost-sure classes.

[F4]

Conditioning a known variable and an independent variable: an integrable random variable independent of the conditioning sigma-algebra has conditional expectation equal to its mean.

[F5]

Taking out what is known: an integrable factor measurable in the conditioning sigma-algebra can be taken outside conditional expectation.

[F6]

Basic algebra and order properties of conditional expectation: conditional expectation is linear and preserves finite integrable sums.

[F7]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $∥ z ∥_{2}^{2} = ⟨ z, z ⟩$ , and the inner product is bilinear.

[F8]

Gradient of a finite sum is the finite sum of gradients: the gradient of $F$ is the average of the component gradients.

[F9]

Finite sums and finite products, by recursion: a finite average is the finite recursively defined sum scaled by $1 / n$ .

[F10]

Laws of finite sums and finite products: finite sums are additive, obey scaling, and permit termwise algebra.

Proof

Given: The objects and sampling assumptions in the Statement.

1.1A1F1F2F3F4F5F6F7F8F9F10givenalgebra

For every $j, i$ , independence and [F4] give $E [1_{{I_{j} = i}} ∣ F_{k}] = 1 / n$ . Since $g_{i}$ is $F_{k}$ -measurable and square-integrable, [F1]–[F3], [F5], and [F6] allow $g_{I_{j}} = \sum_{i} 1_{{I_{j} = i}} g_{i}$ to be conditioned coordinatewise and termwise, yielding $E [g_{I_{j}} ∣ F_{k}] = \overset{ˉ}{g}$ . For $j \neq ℓ$ and every $A \in F_{k}$ , joint independence gives $P (A, I_{j} = r, I_{ℓ} = s) = P (A) / n^{2}$ ; hence $E [⟨ g_{I_{j}} - \overset{ˉ}{g}, g_{I_{ℓ}} - \overset{ˉ}{g} ⟩ ∣ F_{k}] = n^{- 2} \sum_{r, s} ⟨ g_{r} - \overset{ˉ}{g}, g_{s} - \overset{ˉ}{g} ⟩ = ⟨ n^{- 1} \sum_{r} (g_{r} - \overset{ˉ}{g}), n^{- 1} \sum_{s} (g_{s} - \overset{ˉ}{g}) ⟩ = 0$ , since each centered finite sum vanishes. Expanding $∥ G_{b} - \overset{ˉ}{g} ∥_{2}^{2}$ leaves $b$ diagonal terms, each with conditional expectation $σ^{2} (x)$ , so division by $b^{2}$ proves the with-replacement identities.

1.2A1F1F2F4F6F10givenalgebra

Assume $n > 1$ . Let $Z_{i} = 1_{{i \in S}}$ . Relabeling the elements of the uniform size- $b$ subsets shows that $E [Z_{i} ∣ F_{k}]$ has one common value $p$ for all $i$ , and that $E [Z_{i} Z_{j} ∣ F_{k}]$ has one common value $r$ for all ordered pairs $i \neq j$ ; independence of $S$ from $F_{k}$ makes these conditional values constant. There are $n$ singleton indices and $n (n - 1)$ ordered distinct pairs, by choosing the first and then the second index. Every such subset satisfies $\sum_{i} Z_{i} = b$ and $\sum_{i \neq j} Z_{i} Z_{j} = b (b - 1)$ , since each selected index has exactly $b - 1$ other selected indices. Taking conditional expectations and using finite-sum linearity [F6, F10] gives $n p = b$ and $n (n - 1) r = b (b - 1)$ . Thus $p = b / n$ and $r = b (b - 1) / (n (n - 1))$ , including $b = 1$ where $r = 0$ .

2.1A1F1F4F5F6F7F10step 1.2givenalgebra∎

The first inclusion probability in step 1.2, with [F5] and [F6], gives $E [G_{S} ∣ F_{k}] = b^{- 1} \sum_{i} (b / n) g_{i} = \overset{ˉ}{g}$ . Put $a_{i} = g_{i} - \overset{ˉ}{g}$ ; since $G_{S} - \overset{ˉ}{g} = b^{- 1} \sum_{i} Z_{i} a_{i}$ , [F5]–[F7] give $E [∥ G_{S} - \overset{ˉ}{g} ∥_{2}^{2} ∣ F_{k}] = b^{- 2} [(b / n) \sum_{i} ∥ a_{i} ∥_{2}^{2} + (b (b - 1) / (n (n - 1))) \sum_{i \neq j} ⟨ a_{i}, a_{j} ⟩]$ . The cross sum is $- \sum_{i} ∥ a_{i} ∥_{2}^{2}$ by expanding $⟨ \sum_{i} a_{i}, \sum_{j} a_{j} ⟩ = 0$ , so the result is $(n - b) / (b (n - 1)) σ^{2} (x)$ . If $n = 1$ , the only draw and subset contain the sole component, so both errors are zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 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

Robert M. Gower and Alexandre Gramfort, Optimization for Data Science: Stochastic Variance Reduced Gradient Methods, lecture notes (standard reference, not scraped)
John Duchi, Elad Hazan, and Yoram Singer, Adaptive Subgradient Methods for Online Learning and Stochastic Optimization, JMLR 12 (2011) (standard reference, not scraped)