Least-Squares Reconstruction Noise Bound

Abstract

Full-column-rank least-squares reconstruction is stable under additive noise.

Theorem 1.1 (A lower frame bound controls reconstruction error).

$$\begin{array}{r}\forall State,Observation:\mathrm{Type},\\ [\mathrm{NormedAddCommGroup}(State)],[\mathrm{InnerProductSpace}(\mathbb{R},State)],[\mathrm{FiniteDimensional}(\mathbb{R},State)],\\ [\mathrm{NormedAddCommGroup}(Observation)],[\mathrm{InnerProductSpace}(\mathbb{R},Observation)],[\mathrm{FiniteDimensional}(\mathbb{R},Observation)],\\ \forall measurement:\mathrm{LinearMap}(\mathbb{R},State,Observation),\alpha :\mathbb{R},\\ 0<\alpha \Rightarrow \\ \forall difference:State,\alpha {\Vert difference\Vert }^2\le {\Vert \mathrm{measurement}(difference)\Vert }^2\Rightarrow \\ \forall trueState,reconstructed:State,data,noise:Observation,\\ data=\mathrm{measurement}(trueState)+noise\Rightarrow \\ \mathrm{adjoint}(measurement)(\mathrm{measurement}(reconstructed)-data)=0\Rightarrow \\ \Vert reconstructed-trueState\Vert \le \frac{\Vert noise\Vert }{\sqrt{\alpha }}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Linear/LeastSquaresReconstructionNoiseBound.least_squares_reconstruction_noise_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The measurement operator is defined on arbitrary finite-dimensional real inner-product spaces. A positive lower frame bound makes it injective and supplies the smallest-singular-value scale.

The reconstructed state is characterized publicly by the exact least-squares normal equation. Under the lower frame premise this is the full-column-rank Moore–Penrose reconstruction.

Normal-equation orthogonality bounds the measured reconstruction error by the noise norm. The lower frame inequality then gives the sharp inverse-square-root stability factor.

References

• Truth anchor: D5/S3/Observer/Linear/LeastSquaresReconstructionNoiseBound.least_squares_reconstruction_noise_bound