Asymmetric Family Deficiency

Abstract

Deficiency is directed along each fixed-mass fibre of the asymmetric experiment.

Theorem 1.1 (Exact directed deficiencies on a fixed-mass fibre).

$$\begin{gathered} \forall a,M,dOne,dTwo:\mathbb{R}, \\ (0<2\cdot a) \\ \Rightarrow (M<1) \\ \Rightarrow (a\le dOne) \\ \Rightarrow (dOne<dTwo) \\ \Rightarrow (dTwo<(M-a)) \\ \Rightarrow (\text{let }D=1-M,L=M-a,QOne=\mathrm{asymmetricExperiment}(a,dOne,(L-dOne)),QTwo=\mathrm{asymmetricExperiment}(a,dTwo,(L-dTwo)),gamma=\frac{D\cdot (dTwo-dOne)}{(2\cdot dTwo+D)},h=\frac{2\cdot (dTwo-dOne)}{(2\cdot dTwo+D)}\text{ in }((\mathrm{finiteDeficiency}(QTwo,QOne)=0)\wedge \\ (\mathrm{finiteDeficiency}(QOne,QTwo)=\mathrm{ofReal}(gamma))\wedge \\ (0<gamma)\wedge \\ (0<(\frac{(dTwo-dOne)}{(L-dOne)}))\wedge \\ ((\frac{(dTwo-dOne)}{(L-dOne)})<1)\wedge \\ (0<h)\wedge \\ (h<1)\wedge \\ (\exists K:\mathrm{FiniteMarkovKernel}(\mathrm{Fin}(3),\mathrm{Fin}(3)), \\ ((K.1=\left(\begin{array}{ccc}1-(\frac{(dTwo-dOne)}{(L-dOne)})& 0& \frac{(dTwo-dOne)}{(L-dOne)}\\ 0& 1& 0\\ 0& 0& 1\end{array}\right))\wedge \\ (\forall i:\mathrm{Fin}(2),\mathrm{channelOutput}(K.1,QOne\left(i\right))=QTwo\left(i\right))))\wedge \\ (\exists reverseKernel:\mathrm{FiniteMarkovKernel}(\mathrm{Fin}(3),\mathrm{Fin}(3)), \\ ((reverseKernel.1=\left(\begin{array}{ccc}1& 0& 0\\ 0& 1& 0\\ h& 0& 1-h\end{array}\right))\wedge \\ (\forall i:\mathrm{Fin}(2),\mathrm{totalVariation}(QOne\left(i\right),\mathrm{channelOutput}(reverseKernel.1,QTwo\left(i\right)))=gamma)\wedge \\ (\mathrm{uniformSimulationError}(QOne,QTwo,reverseKernel)=gamma))))). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Increasing the second label mass is an exact garbling through the displayed state-independent kernel: the common output is split between itself and the second label while both labels remain fixed.

In the reverse direction, the optimal error is the positive quantity gamma. A zero-one Bayes risk comparison gives the lower bound, and the displayed kernel moves mass from the third output to the common output and has total-variation error exactly gamma in each state.

References

• Truth anchor: D5/S3/Estimation/DecisionRisk/AsymmetricFamilyDeficiency.asymmetric_family_deficiency
• Dependency: D5/S3/Estimation/DecisionRisk/AsymmetricFamilyRiskInjectivity