Moment equations for finite occurrence counts

For a finite family of observations, injective candidate columns which cover all observations satisfy the weighted moment equations. A left inverse then recovers the occurrence counts cast into the coefficient semiring. Coverage is an independent hypothesis.

theorem Function.mulVec_occCount {X : Type u_1} {S : Type u_2} {C : Type u_3} {I : Type u_4} [Fintype X] [Fintype C] {K : Type u_5} [Semiring K] (obs : X → S) (columns : C → S) (hinj : Injective columns) (cover : ∀ (x : X), ∃ (c : C), columns c = obs x) (weight : I → S → K) : ((Matrix.of fun (i : I) (c : C) => weight i (columns c)).mulVec fun (c : C) => ↑(occCount obs (columns c))) = fun (i : I) => ∑ x : X, weight i (obs x)

Injective candidate columns covering every observation satisfy the moment equations.

theorem Function.eq_occCount {X : Type u_1} {S : Type u_2} {C : Type u_3} {I : Type u_4} [Fintype X] [Fintype C] [Fintype I] [DecidableEq C] {K : Type u_5} [Semiring K] (obs : X → S) (columns : C → S) (hinj : Injective columns) (cover : ∀ (x : X), ∃ (c : C), columns c = obs x) (weight : I → S → K) (A : Matrix C I K) (hA : (A * Matrix.of fun (i : I) (c : C) => weight i (columns c)) = 1) (proposed : C → K) (hsolve : (Matrix.of fun (i : I) (c : C) => weight i (columns c)).mulVec proposed = fun (i : I) => ∑ x : X, weight i (obs x)) : proposed = fun (c : C) => ↑(occCount obs (columns c))

A left inverse gives uniqueness for injective candidate columns covering every observation. Coverage is a separate premise, not a consequence of the matrix identity.