83. Noisy invariant forms are proposals, not certificates
On this page · Permalink · Source line 3316
The exact identity \(A^{\mathsf T}HA=H\) need not survive estimation error. A useful proposal can still be obtained from a least-squares invariant form, but the residual must not be interpreted as a positive-cone guarantee.
Let \(\mathcal M_A\) map symmetric matrices into a Euclidean product space by
Use the Frobenius norm on symmetric matrices and the induced product norm. Assume \(\mathcal M_{A^*}\) is injective and \(\mathcal M_{A^*}(H^*)=(0,1)=b\). This fixes the scale of a one-dimensional invariant-form space.
Proposition 74: A posteriori proposal error
Given \(\widehat H\), let \(r=\mathcal M_{\widehat A}(\widehat H)-b\). Suppose
Then
One may take \(e_M\) from the bound
For fixed centers \(c^*=(I-A^*)^{-1}b^*\) and \(\widehat c=(I-\widehat A)^{-1}\widehat b\), with \(\|\widehat A-A^*\|_2\leq e_A\) and \(\|\widehat b-b^*\|_2\leq e_b\), one has
when the denominator is positive.
Read proof · Recorded Lean scope · Permalink · Source line 3328
Proof
The invariant-form difference satisfies
The least singular value of \(\mathcal M_{A^*}\) is at least that of \(\mathcal M_{\widehat A}\) minus \(e_M\). Apply this lower bound and the triangle inequality. To bound the map perturbation, insert and subtract \(\widehat A^{\mathsf T}HA^*\) and apply the Frobenius product inequality. The trace component is unchanged. Finally,
The same singular-value argument proves the center bound. \(\square\)
The theorem assumes an actual perturbation budget and a corresponding exact reference problem. The example reports numerical residuals but does not claim to have statistically certified these budgets. It uses a trace-normalized least-squares shape, a nearly rank-one image for scale, and rationalized center and factor. It accepts none of those computations as a proof of validity. The next checker uses only the submitted rational geometry and the complete polynomial operators.
A rationalized invertible factor \(L\) specifies \(H=L^{\mathsf T}L\) exactly. Positive definiteness is then an algebraic fact even when the factor was suggested by floating-point calculations. It still does not establish operator invariance.