hasFDerivAt_finset_sum_zero
plain-language theorem explainer
If every summand has vanishing Fréchet derivative at a point, the finite sum does too. Analysts assembling the first variation of the Regge Hessian quadratic form cite this lemma. The proof is Finset induction: empty sum is the zero constant, and the inductive step adds two zero derivatives.
Claim. Let $E$ be a real normed space, $s$ a finite index set, and $f_i:E\to\mathbb{R}$ for each $i\in s$. If $\mathrm{D}f_i(x)=0$ (as a continuous linear map $E\to\mathbb{R}$) for every $i\in s$, then the map $y\mapsto\sum_{i\in s}f_i(y)$ also has Fréchet derivative $0$ at $x$.
background
The module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work is to show that named scalar functionals built from edge lengths and dihedral angles have zero Fréchet derivative at the zero vertex potential.
HasFDerivAt f L x is Mathlib's predicate that $L$ is the Fréchet derivative of $f$ at $x$. Here every summand is assumed to have $L=0$, so the claim is that finite summation preserves a zero derivative. The ambient space $E$ is an arbitrary real normed space (in applications, a space of vertex potentials on a 3D triangulation).
No deep upstream geometry is required: the lemma is pure calculus on finite sums, used later when the Hessian quadratic form is written as a sum over hinges or edges.
proof idea
Classical Finset induction on $s$.
Base case: the empty sum is the constant zero function; hasFDerivAt_const gives derivative zero.
Inductive step: split off an element $a\notin s$. The hypothesis supplies HasFDerivAt (f a) 0 x. The inductive hypothesis supplies the same for the remaining sum. Mathlib's HasFDerivAt.add adds the two zero maps to a zero map for the combined sum; a simpa cleans the Finset membership bookkeeping.
why it matters
Parent consumer is hessianQuadratic_hasFDerivAt_zero: the quadratic Hessian form of the Regge action has zero first derivative at the zero potential. That statement is a direct sum of local contributions, each already known to have vanishing derivative at the flat point; this lemma packages the sum.
In the module narrative, the target is the first variation of the nonlinear Regge action at the flat conformal potential (Schläfli cancellation plus zero deficit). Establishing that the Hessian quadratic piece is stationary at zero potential is one analytic brick in that chain. The lemma itself is framework-agnostic calculus, but it sits on the path from local Schläfli identities to the global first-variation claim in discrete gravity / Regge calculus inside Recognition Science geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.