Positive Weighted Readout Gram Kernel

Abstract

A finite positive-weighted readout Gram operator has the common readout kernel.

Theorem 1.1 (Strictly positive weights preserve exactly the common readout kernel).

$$\begin{array}{r}\forall I:\mathrm{Type},[\mathrm{Fintype}(I)],\\ V:\mathrm{Type},\mathrm{RealInnerFD}(V),\\ \forall i:I,Y_i:\mathrm{Type}\wedge \mathrm{RealInnerFD}(Y_i),\\ C:\forall i:I,V\to Y_i,w:I\to \mathbb{R},\\ \forall i:I,0<w_i,\\ W:=\sum _{i\in I}{w}_i{C}_i^{\ast }{C}_i,\\ \forall v:V,⟨v,Wv⟩=\sum _{i\in I}{w}_i\mathrm{norm}(C_i(v){)}^2,\\ \ker (W)=\{v\in V\mid \forall i:I,C_i(v)=0\}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/PositiveWeightedReadoutGramKernel.positive_weighted_readout_gram (✓ std3). ∎

Source. Repository-derived.

Commentary.

The index type is finite, the state space is a finite-dimensional real inner-product space, and each readout may have its own finite-dimensional real inner-product codomain.

The energy identity follows from the adjoint pairing. If the Gram energy vanishes, nonnegativity of every summand and strict positivity of every weight force each readout norm to vanish.

The empty protocol family is included: both kernels are then the whole state space. Strict positivity is essential for nonempty families because a zero weight could hide a nonzero readout.

References

• Truth anchor: D5/S3/Observer/PositiveWeightedReadoutGramKernel.positive_weighted_readout_gram