LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

A small residual gives a nearby root under a uniform inverse and Lipschitz bound

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, and let $F : U \to R^{n}$ be $C^{1}$ with Jacobian $J = D F$ . Take $x_{0} \in U$ such that $A : = J (x_{0})$ is invertible, and let $β > 0$ be any bound with $∥ A^{- 1} ∥_{o p} \leq β$ . Suppose $ϵ : = ∥ F (x_{0}) ∥_{2} > 0$ , set $r : = 2 β ϵ$ , and assume the open ball $B_{2} (x_{0}, 2 r)$ lies in $U$ and

$∥ J (x) - J (y) ∥_{o p} \leq L ∥ x - y ∥_{2} (x, y \in B_{2} (x_{0}, 2 r))$

for some $L \geq 0$ with $β L r \leq \frac{1}{2}$ . Then $F$ has exactly one zero $x_{*}$ in the closed ball ${\overline{B}}_{2} (x_{0}, r)$ , and

$∥ x_{*} - x_{0} ∥_{2} \leq 2 β ∥ F (x_{0}) ∥_{2} .$

If $F (x_{0}) = 0$ , then $x_{0}$ itself is a zero; this separate case makes no local uniqueness assertion.

Facts & Assumptions

Given: The domain, $C^{1}$ map, invertible Jacobian $A = J (x_{0})$ , residual norm $ϵ > 0$ , inverse bound $∥ A^{- 1} ∥_{o p} \leq β$ , radius $r = 2 β ϵ$ , and derivative-Lipschitz bound in the Statement.

[F1]

Continuously differentiable maps, local inverses, and local diffeomorphisms: a $C^{1}$ map is totally differentiable and its derivative is continuous.

[F2]

Invertible Euclidean linear maps: $A$ has a two-sided inverse $A^{- 1}$ .

[F3]

On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ : on a convex open set, a uniform derivative-operator bound implies the corresponding Lipschitz bound for the map.

[F4]

Open ball, closed ball and sphere in a metric space, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ , and the choice-free closed-subspace direction of Closed subspaces of complete metric spaces are complete; the converse under countable choice: a closed Euclidean ball is a nonempty complete metric space.

[F5]

A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point: a contraction from a nonempty complete metric space to itself has a unique fixed point.

[F6]

The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector: the maximum defining the finite-dimensional Euclidean operator norm exists. By The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||, $∥ B w ∥_{2} \leq ∥ B ∥_{o p} ∥ w ∥_{2}$ , and the definition gives submultiplicativity.

[F7]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : for the composition $y \mapsto A^{- 1} F (y)$ , its derivative is $A^{- 1} J (y)$ .

Proof

technique · contraction

1.1givenF1F2F6F7algebra

Since $β > 0$ and $ϵ > 0$ , $r = 2 β ϵ > 0$ . On $B_{2} (x_{0}, 2 r)$ define $Φ (y) : = y - A^{- 1} F (y)$ . By [F1] and [F7], $D Φ (y) = I - A^{- 1} J (y) = A^{- 1} (A - J (y))$ . Since $A = J (x_{0})$ , [F6] and the Lipschitz hypothesis give $∥ D Φ (y) ∥_{o p} \leq β L ∥ y - x_{0} ∥_{2} \leq β L r \leq \frac{1}{2}$ for $y \in {\overline{B}}_{2} (x_{0}, r)$ .

2.1givenF1F3step 1.1

On the open convex ball $B_{2} (x_{0}, r)$ , step 1.1 gives $∥ D Φ (y) ∥_{o p} \leq β L ∥ y - x_{0} ∥_{2} \leq β L r \leq \frac{1}{2}$ . Applying [F3] on this open ball shows that $Φ$ is $1 / 2$ -Lipschitz there. Since $Φ$ is continuous on $B_{2} (x_{0}, 2 r)$ by [F1], approximation by interior points extends the same inequality to every pair in ${\overline{B}}_{2} (x_{0}, r)$ .

3.1givenstep 2.1F6algebra

At the center, $∥ Φ (x_{0}) - x_{0} ∥_{2} = ∥ A^{- 1} F (x_{0}) ∥_{2} \leq ∥ A^{- 1} ∥_{o p} ∥ F (x_{0}) ∥_{2} \leq β ϵ = r / 2$ by [F6]. For every $y \in {\overline{B}}_{2} (x_{0}, r)$ , step 2.1 therefore gives $∥ Φ (y) - x_{0} ∥_{2} \leq ∥ Φ (y) - Φ (x_{0}) ∥_{2} + ∥ Φ (x_{0}) - x_{0} ∥_{2} \leq r / 2 + r / 2 = r$ . Thus $Φ$ maps the closed ball into itself.

4.1F2F4F5step 3.1∎

The ball is nonempty and complete by [F4], so [F5] gives a unique fixed point $x_{*} \in {\overline{B}}_{2} (x_{0}, r)$ . The fixed-point equation is $A^{- 1} F (x_{*}) = 0$ ; invertibility in [F2] yields $F (x_{*}) = 0$ . The ball membership gives the stated distance, and any zero in the ball is a fixed point of $Φ$ , so it equals $x_{*}$ .

Depends on

Used by

Validated Hessian enclosures and a small gradient residual certify a nearby index-one saddle Theorem

Dependency tree · two levels

71 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

Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, version 1.0 (standard reference, not scraped)