Alphabeta MathHow 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.
Gradient of a finite sum is the finite sum of gradients
Statement
Let U be open in R^d, let x in U, let n>=1, and let f_1,...,f_n:U->R be totally differentiable at x. Put F=n^{-1}sum_{i=1}^n f_i. Then F is totally differentiable at x and
Facts & Assumptions
Given: The open domain U, x, n, and the functions in the Statement.
Finite sums and finite products, by recursion: finite sums are recursively defined, with each successor sum equal to the preceding sum plus its next term.
Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives: the sum and scalar multiple of totally differentiable maps are totally differentiable, with derivatives equal to the corresponding sum and scalar multiple.
A total derivative computes every directional derivative, and its matrix is the Jacobian: for each standard basis vector e_j, the partial derivative is DF(x)e_j, and the matrix of DF(x) is the Jacobian.
The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: the gradient of a scalar function is the vector of its partial derivatives.
The principle of mathematical induction: a property true at zero and inherited by each successor holds for every natural index.
The Euclidean inner product on : vectors in R^d are equal when their d coordinates agree.
The total (Fréchet) derivative as the linear first-order approximation with remainder: total differentiability means a linear first-order approximation with a remainder whose norm divided by ||h||_2 tends to zero.
Canonical naturals are positive and strictly increasing: the canonical real image of every natural n>=1 is positive.
Proof
Given: The domain and functions in the Statement.
For 0<=m<=n define S_m:U->R by S_m(y)=sum_{i<m}f_{i+1}(y), using [F1]. The base S_0 is the zero function, whose total derivative is the zero linear map directly from [F7]. If S_m is totally differentiable at x with derivative sum_{i<m}Df_{i+1}(x), then S_{m+1}=S_m+f_{m+1}; [F2] makes it differentiable with derivative sum_{i<m}Df_{i+1}(x)+Df_{m+1}(x)=sum_{i<m+1}Df_{i+1}(x). Induction [F5] proves this formula through m=n.
Since the canonical real image of n is positive by [F8], it is nonzero; the field structure in [F1] therefore supplies its inverse n^{-1}. The scalar-multiple rule [F2] gives DF(x)=n^{-1}sum_{i<n}Df_{i+1}(x).
For each coordinate j, [F3] gives partial_j F(x)=DF(x)e_j=n^{-1}sum_{i<n}Df_{i+1}(x)e_j=n^{-1}sum_{i<n}partial_j f_{i+1}(x). By [F4] these are exactly the coordinates of n^{-1}sum_{i=1}^n grad f_i(x); [F6] then identifies the vectors. Hence the displayed gradient formula holds.
Depends on
- Finite sums and finite products, by recursion
- Canonical naturals are positive and strictly increasing
- The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder
- Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives
- A total derivative computes every directional derivative, and its matrix is the Jacobian
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- The principle of mathematical induction
Used by
- Finite-sum SAGA Algorithm
- Finite-sum SVRG Algorithm
- A regularized logistic finite sum with an exact minimizer Example
- Cocoercive gradient bound for a convex smooth finite sum Lemma
- SAGA conditional estimator, variance, and table recurrence Lemma
- SVRG conditional unbiasedness and variance bound Lemma
- Conditional variance of independent and without-replacement minibatches Theorem
- Expected linear contraction of an SVRG epoch Theorem
- SAGA constant-step linear contraction with a memory-capped factor Theorem
- SAGA expected linear contraction with a memory-scaled step size Theorem
Dependency tree · two levels
40 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
- John Lebl, Basic Analysis I, Section 8.3, The Derivative (standard reference, not scraped)