LemmaStatement: 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.

Forward-difference Jacobian error bound

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, and let each component $F_{j} : U \to R$ , $j < n$ , be $C^{2}$ (twice continuously differentiable). Fix $x \in U$ and increments $h = (h_{0}, \dots, h_{n - 1}) \in R^{n}$ with $h_{i} \neq 0$ for every $i < n$ . For each $i < n$ , suppose an open interval $I_{i} \subseteq R$ contains $[0, 1]$ and $x + t h_{i} e_{i} \in U$ for every $t \in I_{i}$ . Suppose finite constants $M_{i j} \geq 0$ satisfy $∣ \partial_{i i} F_{j} (x + t h_{i} e_{i}) ∣ \leq M_{i j} (0 \leq t \leq 1, j < n) .$ Put $M_{i} : = (\sum_{j < n} M_{i j}^{2})^{1 / 2}$ and $M : = \max_{i < n} M_{i}$ . Let $J_{h} F (x)$ be the forward-difference matrix of Forward-difference Jacobian on an open domain, let $J_{F} (x)$ be the Jacobian matrix of The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case. With the Euclidean operator norm on matrices, $∥ J_{h} F (x) - J_{F} (x) ∥_{o p} \leq \frac{M}{2} ∥ h ∥_{2} .$

Facts & Assumptions

Given: The open domain, $C^{2}$ components, point $x$ , coordinate increments, intervals $I_{i}$ , and second-partial bounds $M_{i j}$ from the Statement.

[F1]

Forward-difference Jacobian on an open domain: for $i < n$ , column $i$ of $J_{h} F (x)$ is $[F (x + h_{i} e_{i}) - F (x)] / h_{i}$ , when $h_{i} \neq 0$ and the sample is in $U$ .

[F2]

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: for $i, j < n$ , the Jacobian entries are $\partial_{i} F_{j} (x)$ .

[F3]

A total derivative computes every directional derivative, and its matrix is the Jacobian: the matrix of $D F$ in the standard basis is the Jacobian matrix.

[F4]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : the derivative of a composition with an affine line is the total derivative applied to the line direction.

[F5]

Multivariable Taylor formula with a Lagrange remainder along a line segment: for a scalar $C^{2}$ function on an open interval, its order-one Taylor expansion on $[0, 1]$ has a second-order Lagrange remainder at some point in $(0, 1)$ .

[F6]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ \sum_{i} a_{i} b_{i} ∣ \leq (\sum_{i} a_{i}^{2})^{1 / 2} (\sum_{i} b_{i}^{2})^{1 / 2}$ .

[F7]

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative: continuous first partial derivatives give a total derivative with the coordinate Jacobian matrix. Applied to each $F_{j}$ and each first partial of $F_{j}$ , the componentwise $C^{2}$ hypotheses give the total differentiability needed below; continuity of the derivative entries makes $F$ a $C^{1}$ map admissible for [F1].

Proof

Given: The data in the Statement.

1.1givenF3F4F5F7choose

By [F7], the $C^{2}$ components and their first partials have the total derivatives needed for the chain rule, and $F$ is admissible for [F1]. For each input coordinate $i < n$ and output component $j < n$ , put $g_{i j} (t) : = F_{j} (x + t h_{i} e_{i})$ on $I_{i}$ . The chain rule [F4] and Jacobian identification [F3] give $g_{i j}^{'} (t) = h_{i} \partial_{i} F_{j} (x + t h_{i} e_{i})$ and $g_{i j}^{''} (t) = h_{i}^{2} \partial_{i i} F_{j} (x + t h_{i} e_{i})$ . Taylor's theorem [F5] between $0$ and $1$ supplies $θ_{i j} \in (0, 1)$ with $F_{j} (x + h_{i} e_{i}) - F_{j} (x) = h_{i} \partial_{i} F_{j} (x) + \frac{h_{i}^{2}}{2} \partial_{i i} F_{j} (x + θ_{i j} h_{i} e_{i})$ . The points $θ_{i j}$ may differ between components.

2.1step 1.1F1F2givenalgebra

Divide by the nonzero $h_{i}$ . In column $i$ , output coordinate $j$ has error at most $M_{i j} ∣ h_{i} ∣ / 2$ ; hence the Euclidean column error is at most $M_{i} ∣ h_{i} ∣ / 2$ , even though the remainder points $θ_{i j}$ may differ.

3.1step 2.1F6algebra∎

For a unit vector $v$ , the triangle inequality and [F6] give $∥ (J_{h} F (x) - J_{F} (x)) v ∥_{2} \leq \sum_{i < n} ∣ v_{i} ∣ ∥ (J_{h} F (x) - J_{F} (x)) e_{i} ∥_{2} \leq \frac{1}{2} (\sum_{i < n} v_{i}^{2})^{1 / 2} (\sum_{i < n} M_{i}^{2} h_{i}^{2})^{1 / 2} \leq \frac{M}{2} ∥ h ∥_{2}$ . Taking the supremum over unit $v$ proves the operator-norm bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

E. Hairer and G. Wanner, Solving Ordinary Differential Equations II, Chapter VI: Iterative Methods—Nonlinear Equations (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, version 1.0 (standard reference, not scraped)