Lossless Linear Postprocessing

Abstract

A linear postprocessing preserves the observation kernel exactly when it is injective on the observed range.

Theorem 1.1 (Kernel preservation is range injectivity).

$$\begin{array}{c}\forall K,V,Y,Z:Type,M,B,\\ \mathrm{Ring}(K)\wedge \mathrm{AddCommGroup}(V)\wedge \mathrm{Module}(K,V)\wedge \mathrm{AddCommGroup}(Y)\wedge \mathrm{Module}(K,Y),\\ \mathrm{AddCommGroup}(Z)\wedge \mathrm{Module}(K,Z)\wedge M\in \mathrm{LinearMap}(K,V,Y)\wedge B\in \mathrm{LinearMap}(K,Y,Z)\Rightarrow \\ \ker (\mathrm{comp}(B,M))=\ker (M)⟺\mathrm{InjOn}(B,\mathrm{range}(M)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/LosslessLinearPostprocessing.kernel_comp_eq_iff_injective_on_range (✓ std3). ∎

Source. Repository-derived.

Commentary.

The forward direction tests two realized observations through their difference. The reverse direction compares each observed value with the observed zero, so injectivity on the realized range recovers the original kernel.

References

• Truth anchor: D5/S3/Observer/LinearMemory/LosslessLinearPostprocessing.kernel_comp_eq_iff_injective_on_range