Observation Rank Submodularity

Abstract

Finite observation-subspace rank is submodular and has diminishing returns.

Theorem 1.1 (Observation rank is submodular).

$$\begin{array}{r}\forall K,V,iota:\mathrm{Type},\\ [\mathrm{DivisionRing}(K)],[\mathrm{AddCommGroup}(V)],[\mathrm{Module}(K,V)],\\ [\mathrm{FiniteDimensional}(K,V)],[\mathrm{DecidableEq}(iota)],\\ \forall U:iota\to \mathrm{Submodule}(K,V),r(A:\mathrm{Finset}(iota)):=\mathrm{finrank}(K,\mathrm{finsetSup}(A,U));\\ (\forall A,B:\mathrm{Finset}(iota),r\left(\mathrm{union}(A,B)\right)+r\left(\mathrm{inter}(A,B)\right)\le r\left(A\right)+r\left(B\right))\wedge \\ (\forall A,B:\mathrm{Finset}(iota),x:iota,A\subseteq B\Rightarrow r\left(\mathrm{union}(B,\mathrm{singleton}(x))\right)-r\left(B\right)\le r\left(\mathrm{union}(A,\mathrm{singleton}(x))\right)-r\left(A\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let U assign a subspace of a finite-dimensional module to every observation index. For a finite selection A, its observation rank is the scalar dimension of the supremum of the selected subspaces.

The finite-supremum union identity identifies the combined selected space with a subspace supremum. The selected intersection embeds into the intersection of the two selected spaces, so the exact dimension formula for a supremum and infimum gives submodularity.

Applying the same inequality to A with the new index adjoined and to B yields the displayed diminishing-return form.

References

• Truth anchor: D5/S3/Observer/Linear/ObservationRankSubmodularity.observation_rank_submodularity