TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Newton polar iterates converge quadratically under an explicit norm condition

Statement

Let $A \in C^{n \times n}$ be nonsingular, write its polar decomposition $A = U H$ with $U$ unitary and $H$ positive definite, and define the exact Newton iterates $X_{0} = A, X_{k + 1} = \frac{1}{2} (X_{k} + X_{k}^{- *}), X_{k}^{- *} : = (X_{k}^{- 1})^{*} .$ Then every iterate is defined, $X_{k} \to U$ , and for every $k \geq 1$ , $∥ X_{k + 1} - U ∥_{2} \leq \frac{1}{2} ∥ X_{k} - U ∥_{2}^{2} .$ This is a theorem about the exact sequence, not a rounding-error guarantee for Finite-budget Newton iteration for the nonsingular polar factor.

Facts & Assumptions

Given: A nonsingular complex matrix $A$ and its exact Newton sequence.

[F1]

A nonsingular matrix has a polar factorization $A = U H$ with $U$ unitary and $H = \sqrt{A^{*} A}$ positive definite (Every endomorphism has a polar decomposition T = SU with U non-negative and S an isometry on the orthogonal complement of ker T, and S is unique exactly when T is invertible, A non-negative operator has a unique non-negative square root).

[F2]

A positive self-adjoint matrix has an orthonormal eigenbasis with positive eigenvalues when it is positive definite (A normal endomorphism is a sum of its eigenvalues times pairwise orthogonal projections, and each spectral projection is a polynomial in the endomorphism).

[F3]

The given exact sequence in the Statement is defined by $X_{k + 1} = (X_{k} + X_{k}^{- *}) / 2$ whenever $X_{k}$ is invertible. This is a defining recurrence, independent of the rounded algorithm.

Proof

1.1F1F2F3construct

If $n = 0$ , the unique empty matrix is the identity, its own inverse and its polar factor; the exact sequence is constant and both sides of the norm bound are zero. Hence assume $n \geq 1$ . By [F1] and [F2], choose a unitary basis in which $H = diag (σ_{1}, \dots, σ_{n})$ with $σ_{i} > 0$ . Inductively write $X_{k} = U g_{k} (H)$ , where $g_{0} (t) = t$ and $g_{k + 1} (t) = (g_{k} (t) + g_{k} (t)^{- 1}) / 2$ . If this holds at $k$ , then $X_{k}^{- *} = U g_{k} (H)^{- 1}$ because $U^{*} U = I$ and $g_{k} (H)$ is positive diagonal; substituting into [F3] proves the next formula and shows every iterate is invertible.

2.1step 1.1algebra

For each scalar $σ_{i} > 0$ , $g_{1} (σ_{i}) - 1 = (σ_{i} - 1)^{2} / (2 σ_{i}) \geq 0$ , so $g_{1} (σ_{i}) \geq 1$ . If $y \geq 1$ , then $\frac{1}{2} (y + y^{- 1}) \leq y$ , and $\frac{1}{2} (y + y^{- 1}) - 1 = (y - 1)^{2} / (2 y)$ . Hence each sequence $g_{k} (σ_{i})$ for $k \geq 1$ decreases to a limit $y \geq 1$ satisfying $y = (y + y^{- 1}) / 2$ , so $y = 1$ . The displayed identity also gives $∣ g_{k + 1} (σ_{i}) - 1 ∣ \leq ∣ g_{k} (σ_{i}) - 1 ∣^{2} / 2$ for $k \geq 1$ .

3.1step 2.1algebra∎

Since $U$ is unitary and $g_{k} (H)$ is diagonal, $∥ X_{k} - U ∥_{2} = \max_{i} ∣ g_{k} (σ_{i}) - 1 ∣$ . Taking maxima in step 2.1 proves $X_{k} \to U$ and the stated quadratic bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

Nicholas J. Higham, Computing the Polar Decomposition—with Applications (standard reference, not scraped)
Jan Zur, Matrix Functions, TU Berlin full lecture notes (standard reference, not scraped)