Linear Postprocessing Defect Contraction

Abstract

Linear postprocessing contracts realization defect by its operator norm.

Theorem 1.1 (Postprocessing contracts distance to the realizable image).

$$\begin{array}{c}\forall Y,Z:\mathrm{Type},\\ [\mathrm{NormedAddCommGroup}(Y)][{\mathrm{NormedSpace}}_{\mathbb{R}}(Y)][{\mathrm{FiniteDimensional}}_{\mathbb{R}}(Y)],\\ [\mathrm{NormedAddCommGroup}(Z)][{\mathrm{NormedSpace}}_{\mathbb{R}}(Z)],\\ B:\mathrm{ContinuousLinearMap}(\mathbb{R},Y,Z),I:\mathrm{Set}(Y),y:Y,\\ (\mathrm{IsClosed}(I)\wedge \mathrm{Nonempty}(I))\Rightarrow \\ (\mathrm{infDist}(B(y),\mathrm{image}(B,I))\le \Vert B\Vert \mathrm{infDist}(y,I))\wedge \\ (\Vert B\Vert \le 1\Rightarrow \mathrm{infDist}(B(y),\mathrm{image}(B,I))\le \mathrm{infDist}(y,I)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/DefectComposition/LinearPostprocessingDefectContraction.linear_postprocessing_defect_contraction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source and target are real normed spaces, with the source finite dimensional. The realizable set I is nonempty and closed, and B is a continuous linear postprocessor.

Closedness supplies a nearest realizable point to y. Its image under B is an admissible comparison point in image(B,I), and the operator norm bounds the resulting distance.

The source also assumes convexity and finite dimensionality of the target. Neither is needed for this conclusion, so the machine statement proves the two public clauses without them.

References

• Truth anchor: D5/S3/Observer/DefectComposition/LinearPostprocessingDefectContraction.linear_postprocessing_defect_contraction