34. Noisy operator reconstruction in a fixed core
On this page · Permalink · Source line 1404
After choosing a core block, the square reconstruction formula yields a particularly direct error identity. It is useful even when the core was chosen on a separate discovery data set.
Let \(G_s=B_sH\) with \(s_H=\sigma_{\min}(H)>0\). Observe
Proposition 33: Noisy core-block realization
The estimate \(\widehat B_s=\widetilde G_s\widetilde H^{-1}\) satisfies
and therefore
A bound using only the fitted operator and the same perturbation budgets is
If \(\widetilde s=\sigma_{\min}(\widetilde H)\) is known and \(\|E\|_2\leq e<\widetilde s\), the last denominator may be replaced by \(\widetilde s-e\).
Read proof · Recorded Lean scope · Permalink · Source line 1416
Proof
Since \(\widetilde H\) is invertible, subtract \(B_s\) from its fitted expression and collect the terms. The least singular value of \(\widetilde H\) is at least \(s_H-\|E\|_2\). For the second identity, use
and multiply by \(H^{-1}\). Finally \(s_H\geq\widetilde s-e\) by singular-value perturbation. \(\square\)
When the first test is empty, the mass row \(\lambda=e_1^\top\) is fixed rather than estimated. Set the first component of the initial vector to one as required by \(f(\epsilon)=1\). Errors in other initial test probabilities remain initial-state error. This convention removes an avoidable normalizer-estimation ambiguity but does not enforce cone preservation or mass conservation for the fitted symbol family.
Numerical implementation should solve the linear systems rather than explicitly form a floating-point inverse. The theorem describes the exact algebraic estimator. Finite-precision solve error is an additional residual, which the reference script measures separately.