Task-Family Law Kernel Criterion

Abstract

Separating loss expectations identify predictive laws, while finite event indicators identify probability mass functions.

Theorem 1.1 (Measure-determining tasks recover the predictive kernel).

$$\begin{array}{c}\forall H,Law,Y,T,A,Z:Type,\\ \mathrm{Fintype}(Z),\\ Psi:H\to Law,\\ E:Law\to Y\to \mathbb{R}\to \mathbb{R},\\ ell:T\to A\to Y\to \mathbb{R},\\ \forall mu,nu:Law,(\forall t:T,a:A,E(mu,(y\mapsto \mathrm{ell}(t,a,y)))=E(nu,(y\mapsto \mathrm{ell}(t,a,y))))\Rightarrow mu=nu\Rightarrow \\ \ker (Psi)=\ker ((h\mapsto (t\mapsto (a\mapsto E(Psi(h),(y\mapsto \mathrm{ell}(t,a,y)))))))\wedge \forall mu,nu:\mathrm{PMF}(Z),\\ (\forall B:\mathrm{Set}(Z),\sum _{z:Z}\mathrm{indicator}(B,(z\mapsto \mathrm{toReal}(mu(z))),z)=\sum _{z:Z}\mathrm{indicator}(B,(z\mapsto \mathrm{toReal}(nu(z))),z))\Rightarrow mu=nu.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/SequentialDecisionRisk/TaskFamilyLawKernelCriterion.task_family_law_kernel_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The risk profile is constructed from the predictive law, the expectation operator, and every loss and action coordinate. If those coordinates determine allowed laws, its equality kernel is exactly the predictive law kernel.

For a finite outcome carrier, agreement on the expectation of every event indicator includes agreement on singleton events and therefore determines every probability mass.

References

• Truth anchor: D5/S3/Estimation/SequentialDecisionRisk/TaskFamilyLawKernelCriterion.task_family_law_kernel_criterion