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.
Gauss-Newton converges quadratically at a full-rank zero-residual root
Statement
Let , and let be on an open , and let satisfy . Let be convex. Suppose is -Lipschitz on and, for some , Thus every has full column rank. For the exact Gauss-Newton iteration , where is the unique minimizer of . When the iteration uses the exact branch of Gauss-Newton linearized least-squares step with QR/SVD rank safeguards, assume each invocation is supplied with an exact reduced QR factorization of . Set . Then every satisfies If and , all iterates stay in the ball, converge to , and contract at least by per iteration after the quadratic estimate. If and , one exact step reaches . This result concerns exact solves; it asserts no finite-precision convergence rate.
Facts & Assumptions
Given: The residual, root, convex ball, Lipschitz Jacobian, uniform lower bound , and exact Gauss-Newton steps in the Statement.
Rectangular residual linearization error under a Lipschitz Jacobian: on a convex segment, .
Gauss-Newton linearized least-squares step with QR/SVD rank safeguards: an exact full-rank branch returns the unique minimizer of the linearized residual least-squares problem.
The Euclidean inner product on : the Euclidean inner product is bilinear and symmetric, and .
.
with for every and every .
Proof
Fix , put , and write . By [F1] and [A1], with .
Let be the exact Gauss-Newton step and set . For every , minimality of gives for all real . Expanding in shows the linear coefficient must be zero (otherwise a sufficiently small of the opposite sign decreases the quadratic). Since this holds for every , by step 1.1.
Set . Step 2.1 gives , so is orthogonal to ; hence . By [A2], . Therefore .
If and , step 3.1 gives . If and , the stated hypothesis also puts , and step 3.1 gives , so ; induction repeats the same bound for every , and .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
36 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
- Jorge Nocedal and Stephen J. Wright, Numerical Optimization, second edition (standard reference, not scraped)
- David Bindel, CS 4220: Numerical Analysis, Gauss-Newton and nonlinear least squares (standard reference, not scraped)