Alphabeta MathHow 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.
Mixed-precision refinement has an error recurrence and a finite precision floor
Statement
Let A be nonsingular, Ax_=b, A-hat nonsingular, and e_k=x_-x_k. Suppose the successful refinement algorithm has r-hat_k=Ae_k+delta_r,k with ||delta_r,k||_2<=eta_r(||A||_2||x_k||_2+||b||_2)+xi_r and combined solve/update residual-equivalent error ||delta_w,k||_2<=eta_w||r-hat_k||_2+xi_w. Set rho_0=xi_r+eta_r(||A||2||x*||_2+||b||_2), q=||I-A-hat^{-1}A||_2+||A-hat^{-1}||_2((1+eta_w)eta_r+eta_w)||A||_2, eta=||A-hat^{-1}||2((1+eta_w)rho_0+xi_w). Then e{k+1}=(I-A-hat^{-1}A)e_k-A-hat^{-1}(delta_r,k+delta_w,k). If q<1 then ||e_k||_2<=q^k||e_0||_2+eta(1-q^k)/(1-q) for every executed k<=N. The precision floor is eta/(1-q); this is conditional and does not promise exact termination.
Facts & Assumptions
Given: residual and combined solve/update certificates at distinct precisions u_r, u_f, and u_w.
Bounded mixed-precision iterative refinement: residual, factorization, and update precisions are distinct; the algorithm represents solve/update error by delta_w and fails inconclusively on missing certificates.
Induced matrix norms are compatible with matrix-vector multiplication, submultiplicative, and satisfy ||I|| = 1: the induced norm is compatible with matrix-vector products.
Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: the finite-dimensional spectral norm is the operator norm used in the estimates.
Proof
By the residual-equivalent update certificate, e_{k+1}=e_k-A-hat^{-1}(r-hat_k+delta_w,k). Substituting r-hat_k=Ae_k+delta_r,k gives the exact recurrence.
Since ||x_k||2<=||x*||_2+||e_k||_2, the residual certificate yields ||delta_r,k||_2<=eta_r||A||_2||e_k||_2+rho_0 and ||r-hat_k||_2<= (1+eta_r)||A||_2||e_k||_2+rho_0. Therefore ||delta_w,k||_2<=eta_w(1+eta_r)||A||_2||e_k||_2+eta_w rho_0+xi_w.
Apply compatibility and the triangle inequality to the recurrence. The error coefficient is q because eta_r+eta_w(1+eta_r)=(1+eta_w)eta_r+eta_w; the additive term is eta. Thus ||e_{k+1}||_2<=q||e_k||_2+eta.
If q<1, induction gives ||e_k||_2<=q^k||e_0||2+eta sum{j=0}^{k-1}q^j. The finite geometric sum is (1-q^k)/(1-q), proving the assertion.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
16 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
- Fundamentals of Numerical Computation, floating-point arithmetic (standard reference, not scraped)
- Stuart and Voss, Matrix Analysis and Algorithms, Warwick lecture notes (standard reference, not scraped)
- Higham and Mary, Mixed Precision Algorithms in Numerical Linear Algebra (standard reference, not scraped)