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 in the maximum norm

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, and let $F : U \to R^{n}$ be $C^{1}$ . For $x \in R^{n}$ define $∥ x ∥_{\infty} : = \max_{j < n} ∣ x_{j} ∣$ , and for a linear map $B : R^{n} \to R^{n}$ define its induced norm by $∥ B ∥_{\infty} : = \sup_{z \neq 0} ∥ B z ∥_{\infty} / ∥ z ∥_{\infty}$ . This supremum is a finite real: if $B = (b_{i j})$ in the standard basis, then for $∥ z ∥_{\infty} = 1$ ,

$∥ B z ∥_{\infty} = \max_{i < n} ∣ \sum_{j < n} b_{i j} z_{j} ∣ \leq \sum_{i < n} \sum_{j < n} ∣ b_{i j} ∣,$

and scaling reduces every nonzero $z$ to this case; the set is nonempty because $n \geq 1$ . Its supremum therefore exists by the least-upper-bound property of $R$ . Let $x_{0} \in U$ , $A : = D F (x_{0})$ be invertible, and suppose $∥ A^{- 1} ∥_{\infty} \leq β$ for some $β > 0$ . Put $ϵ : = ∥ F (x_{0}) ∥_{\infty} \geq 0$ , and choose $r > 0$ with $β ϵ \leq r / 2$ . Assume $B_{\infty} (x_{0}, 2 r) \subset U$ and

$∥ D F (x) - D F (y) ∥_{\infty} \leq L ∥ x - y ∥_{\infty} (x, y \in B_{\infty} (x_{0}, 2 r))$

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

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

In particular, when $F (x_{0}) = 0$ the unique zero in this ball is $x_{0}$ .

Facts & Assumptions

Given: The open domain, $C^{1}$ map, point $x_{0}$ , invertible derivative $A = D F (x_{0})$ , maximum-norm residual $ϵ \geq 0$ , inverse bound $∥ A^{- 1} ∥_{\infty} \leq β$ , chosen radius $r > 0$ with $β ϵ \leq 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 everywhere on its open domain with continuous derivative.

[F2]

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

[F3]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a scalar function continuous on a closed interval and differentiable on its interior has a point where its endpoint difference equals its derivative times the interval length.

[F4]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ and $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it: $∥ \cdot ∥_{\infty}$ induces the metric $d_{\infty}$ on $R^{n}$ for $n \geq 1$ . The real clause of $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ gives convergence of every Cauchy sequence of real coordinates.

[F5]

Open ball, closed ball and sphere in a metric space and Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed make a closed maximum-norm ball closed and nonempty. Once the ambient maximum-norm metric is complete, the choice-free closed-subspace direction of Closed subspaces of complete metric spaces are complete; the converse under countable choice makes that ball complete.

[F6]

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.

[F7]

$R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ , Fact L6: every nonempty finite set of natural indices has a maximum.

[F8]

Every linear map $B : R^{n} \to R^{n}$ has a matrix $(b_{i j})$ ; for $∥ z ∥_{\infty} = 1$ , the finite-sum, triangle, and absolute-value inequalities give $∥ B z ∥_{\infty} \leq \sum_{i < n, j < n} ∣ b_{i j} ∣$ . Scaling shows the defining ratio set is bounded, and $n \geq 1$ makes it nonempty; its supremum exists by the least-upper-bound property (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ , Finite sums and finite products, by recursion, Laws of finite sums and finite products, Basic properties of the absolute value, The triangle inequality, The Cauchy-sequence reals have the least-upper-bound property).

[F9]

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} D F (y)$ .

Proof

technique · contraction

1.1F1F2F8F9givenalgebra

Define $Φ (y) : = y - A^{- 1} F (y)$ on $B_{\infty} (x_{0}, 2 r)$ . By [F1] and [F9], $D Φ (y) = I - A^{- 1} D F (y) = A^{- 1} (A - D F (y))$ . The induced maximum norm is submultiplicative directly from its definition, and [F8] ensures it is well-defined, so for $y \in {\overline{B}}_{\infty} (x_{0}, r)$ the Lipschitz hypothesis gives $∥ D Φ (y) ∥_{\infty} \leq β L ∥ y - x_{0} ∥_{\infty} \leq β L r \leq \frac{1}{2}$ .

1.2F4F7givenchoose

Let $(x^{(m)})$ be Cauchy in $d_{\infty}$ . For every $j < n$ , $∣ x_{j}^{(m)} - x_{j}^{(l)} ∣ \leq d_{\infty} (x^{(m)}, x^{(l)})$ , so the $j$ th coordinate sequence is Cauchy in $R$ and converges to some $y_{j}$ by [F4]. The finitely many unique limits define $y \in R^{n}$ . Given $δ > 0$ , choose for each $j < n$ an index $K_{j}$ such that $∣ x_{j}^{(m)} - y_{j} ∣ < δ$ for $m \geq K_{j}$ ; since $n \geq 1$ , [F7] gives $K = \max_{j < n} K_{j}$ . Then $d_{\infty} (x^{(m)}, y) < δ$ for $m \geq K$ . Thus $(R^{n}, d_{\infty})$ is complete.

2.1F1F3F9step 1.1given

For any $y, z$ in the closed radius- $r$ ball, their joining segment lies in the open radius- $2 r$ ball. For each coordinate $j$ , the scalar function $t \mapsto Φ_{j} (z + t (y - z))$ is continuous on $[0, 1]$ and differentiable on $(0, 1)$ by [F1] and [F9]. Its derivative has absolute value at most $∥ D Φ (z + t (y - z)) ∥_{\infty} ∥ y - z ∥_{\infty} \leq \frac{1}{2} ∥ y - z ∥_{\infty}$ . Applying [F3] coordinatewise and taking the maximum gives $∥ Φ (y) - Φ (z) ∥_{\infty} \leq \frac{1}{2} ∥ y - z ∥_{\infty}$ .

3.1F2givenstep 2.1algebra

At the center, $∥ Φ (x_{0}) - x_{0} ∥_{\infty} = ∥ A^{- 1} F (x_{0}) ∥_{\infty} \leq β ϵ \leq r / 2$ . Thus for $y$ in the closed ball, step 2.1 gives $∥ Φ (y) - x_{0} ∥_{\infty} \leq ∥ Φ (y) - Φ (x_{0}) ∥_{\infty} + ∥ Φ (x_{0}) - x_{0} ∥_{\infty} \leq r / 2 + r / 2 = r$ , so $Φ$ maps the ball into itself.

4.1F2F5F6step 3.1step 1.2

The closed ball is nonempty and complete by step 1.2 and [F5]. Hence [F6] gives a unique fixed point $x_{*} \in {\overline{B}}_{\infty} (x_{0}, r)$ . Its fixed-point equation gives $A^{- 1} F (x_{*}) = 0$ , and invertibility in [F2] yields $F (x_{*}) = 0$ .

5.1F6step 2.1step 3.1step 4.1algebra∎

By step 2.1, $∥ Φ (x_{*}) - Φ (x_{0}) ∥_{\infty} \leq \frac{1}{2} ∥ x_{*} - x_{0} ∥_{\infty}$ . The fixed-point identity $Φ (x_{*}) = x_{*}$ and the center estimate in step 3.1 therefore give $∥ x_{*} - x_{0} ∥_{\infty} \leq \frac{1}{2} ∥ x_{*} - x_{0} ∥_{\infty} + β ϵ$ , hence $∥ x_{*} - x_{0} ∥_{\infty} \leq 2 β ϵ$ . Any zero in the ball is a fixed point of $Φ$ , hence equals $x_{*}$ .

Depends on

Used by

A gauge-fixed stable discrete path lies within second order of a smooth MEP Theorem

Dependency tree · two levels

93 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)
E. Hairer and G. Wanner, Solving Ordinary Differential Equations II, Chapter VI: Iterative Methods—Nonlinear Equations (standard reference, not scraped)