Asymmetric Family Risk and Injective Queries

Abstract

The asymmetric three-output experiment has an explicit Bayes risk, and the fixed-mass risk queries are injective exactly below the saturation prior.

Definition 1.1 (The asymmetric experiment).

$$\begin{gathered} \forall a,d,b:\mathbb{R}, \\ \text{let }D=1-(b+a+d)\text{ in }\mathrm{asymmetricExperiment}(a,d,b)=((b,a+D,d),(b,a,d+D)). \end{gathered}$$

Formalization. D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetricExperiment (✓ std3).

Source. Repository-derived.

Commentary.

The two states share mass b in the first output. The residual mass D is placed in the second output for state zero and in the third output for state one.

Definition 1.2 (Optimal zero-one Bayes risk).

$$\begin{gathered} \forall a,d,b,pi:\mathbb{R}, \\ \mathrm{asymmetricBayesRisk}(a,d,b,pi)=\mathrm{sInf}(\mathrm{range}((delta:\mathrm{FiniteMarkovKernel}(\mathrm{Fin}(3),\mathrm{Fin}(2))\mapsto \mathrm{finiteBayesCost}(\mathrm{vec}(pi,1-pi),(i,j)\mapsto \text{if }i=j\text{then }0\text{else }1,\mathrm{asymmetricExperiment}(a,d,b),delta)))). \end{gathered}$$

Formalization. D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetricBayesRisk (✓ std3).

Source. Repository-derived.

Commentary.

The risk is the infimum over all row-stochastic decisions from the three outputs to the two actions, for the prior (pi, 1 - pi) and zero-one loss.

Definition 1.3 (Risk along a fixed-mass fiber).

$$\begin{gathered} \forall M,a,pi,d:\mathbb{R}, \\ \mathrm{asymmetricFiberRisk}(M,a,pi,d)=\mathrm{asymmetricBayesRisk}(a,d,M-a-d,pi). \end{gathered}$$

Formalization. D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetricFiberRisk (✓ std3).

Source. Repository-derived.

Commentary.

Fixing M and a leaves d as the fiber coordinate and sets b equal to M - a - d.

Theorem 1.4 (Piecewise risk and injectivity threshold).

$$\begin{array}{c}\forall aOne,dOne,bOne,piOne,aTwo,mTwo,piTwo:\mathbb{R},\\ ((0<aOne\wedge \\ aOne\le dOne\wedge \\ 0<bOne\wedge \\ bOne+aOne+dOne<1\wedge \\ piOne\in \mathrm{Icc}(0,1))\Rightarrow \text{let }M=bOne+aOne+dOne,D=1-M,tMinus=\frac{aOne}{2\cdot aOne+D},tPlus=\frac{dOne+D}{2\cdot dOne+D}\text{ in }((0<tMinus\wedge \\ tMinus<\frac{1}{2}\wedge \\ \frac{1}{2}<tPlus\wedge \\ tPlus<1)\wedge \\ ((piOne\in \mathrm{Icc}(0,tMinus))\Rightarrow (\mathrm{asymmetricBayesRisk}(aOne,dOne,bOne,piOne)=piOne))\wedge \\ ((piOne\in \mathrm{Icc}(tMinus,\frac{1}{2}))\Rightarrow (\mathrm{asymmetricBayesRisk}(aOne,dOne,bOne,piOne)=aOne+piOne\cdot (M-2\cdot aOne)))\wedge \\ ((piOne\in \mathrm{Icc}(\frac{1}{2},tPlus))\Rightarrow (\mathrm{asymmetricBayesRisk}(aOne,dOne,bOne,piOne)=M\cdot (1-piOne)+(2\cdot piOne-1)\cdot dOne))\wedge \\ ((piOne\in \mathrm{Icc}(tPlus,1))\Rightarrow (\mathrm{asymmetricBayesRisk}(aOne,dOne,bOne,piOne)=1-piOne))))\wedge \\ ((0<2\cdot aTwo\wedge \\ 2\cdot aTwo<mTwo\wedge \\ mTwo<1\wedge \\ \frac{1}{2}<piTwo\wedge \\ piTwo\le 1)\Rightarrow \text{let }D=1-mTwo,L=mTwo-aTwo,U=2\cdot L+D,s=2\cdot piTwo-1,c=mTwo\cdot (1-piTwo),t=\frac{D\cdot (1-s)}{2\cdot s}\text{ in }((\forall d\in \mathrm{Ico}(aTwo,L),\mathrm{asymmetricFiberRisk}(mTwo,aTwo,piTwo,d)=c+s\cdot \min (d,t))\wedge \\ ((\mathrm{InjOn}(\mathrm{asymmetricFiberRisk}(mTwo,aTwo,piTwo),\mathrm{Ico}(aTwo,L)))⟺(piTwo\le \frac{L+D}{2\cdot L+D}))\wedge \\ \frac{L+D}{2\cdot L+D}=\frac{1+\frac{D}{U}}{2}\wedge \\ ((\mathrm{InjOn}(\mathrm{asymmetricFiberRisk}(mTwo,aTwo,piTwo),\mathrm{Ico}(aTwo,L)))\Rightarrow (s\le \frac{D}{U}))\wedge \\ \mathrm{InjOn}(\mathrm{asymmetricFiberRisk}(mTwo,aTwo,\frac{L+D}{2\cdot L+D}),\mathrm{Ico}(aTwo,L))\wedge \\ 2\cdot \frac{L+D}{2\cdot L+D}-1=\frac{D}{U})).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetric_family_risk_and_injective_queries (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive asymmetric masses with a at most d, the two likelihood crossings lie strictly on opposite sides of one half. Minimizing the error contribution separately at each output gives the four displayed affine pieces.

On a fixed-mass fiber and above prior one half, the risk is a positive affine multiple of min(d,t). It is strictly increasing when t is at least the fiber endpoint L, and otherwise it is constant on a nontrivial terminal interval. This yields the exact injectivity threshold and the maximal admissible slope.

References

• Truth anchor: D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetricBayesRisk
• Truth anchor: D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetricExperiment
• Truth anchor: D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetricFiberRisk
• Truth anchor: D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity.asymmetric_family_risk_and_injective_queries
• Dependency: D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyRiskTransfer