Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Approximate CAR recovery

Abstract

One approximate coarsening-at-random simulation admits a common reverse kernel with a signed pairwise recovery budget.

Definition 1.1 (Nonempty blocks).

Formalization. D5/S3/Estimation/DecisionRisk/CARApproximateRecovery.Block (✓ std3).

Source. Repository-derived.

Commentary.

The output alphabet consists of all nonempty finite subsets of the state space. Blocks of zero weight remain in the alphabet.

Definition 1.2 (CAR rows).

Formalization. D5/S3/Estimation/DecisionRisk/CARApproximateRecovery.row (✓ std3).

Source. Repository-derived.

Commentary.

A state assigns weight w(B) to a block containing it and zero to every other block. Nonnegative weights and unit row sums make these probability rows.

Definition 1.3 (Pairwise block weights).

Formalization. D5/S3/Estimation/DecisionRisk/CARApproximateRecovery.pair (✓ std3).

Source. Repository-derived.

Commentary.

The pair weight sums the weights of blocks containing both states; the definition also includes equal states.

Theorem 1.4 (Common reverse kernel and signed recovery bound).

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

Source. Repository-derived.

Commentary.

The state space A is finite and nonempty, with decidable equality. Both profiles have nonnegative weights and unit row sums. The one forward Markov kernel H is shared by every state, and the existentially quantified reverse kernel R is shared by all conclusions. Kernel arguments are ordered as input then output. Total variation is half the sum of absolute coordinate differences.

Delta is signed: it is the pair weight for v minus the pair weight for w. Only Delta(i,j) + epsilon(i) + epsilon(j) is asserted nonnegative. The function eta is the maximum absolute off-diagonal pair difference, with diagonal entries set to zero. Thus eta and each empty row sum are zero on a one-state space, and the recovery error is zero there.

The deficiency has target row(w) and source row(v): it measures simulation of w from v. It is the infimum over all reverse Markov kernels of the maximum statewise total-variation error, embedded in the extended nonnegative reals. The bound is truncated at one.

For the construction, put F_i(B,C) = row(w,i,B) H(B,C) and Q_i(C) = sum_B F_i(B,C). Multiply each column by a_i(C) = min(1,V_i(C)/Q_i(C)) when Q_i(C) is positive, and by one when it is zero, obtaining t_i. The nonnegative residuals u_i(B) = W_i(B) - sum_C t_i(B,C) and z_i(C) = V_i(C) - sum_B t_i(B,C) both have total mass epsilon(i). For positive epsilon(i), set g_i = t_i + u_i z_i / epsilon(i). When epsilon(i) is zero, both residuals vanish and g_i = t_i; no division by zero is needed.

The table g_i has marginals W_i and V_i and is supported on blocks containing i. The overlap of g_i and g_j is at least pair(w,i,j) - epsilon(i) - epsilon(j). Consequently their columnwise half-L1 difference, summed over columns containing both states, is at most the signed budget Delta(i,j) + epsilon(i) + epsilon(j).

For v(C) > 0 choose R(C,B) = sum_{j in C} g_j(B,C) / (|C| v(C)). For v(C) = 0 choose a point mass at one fixed singleton block; such columns carry no mass under any V_i. Averaging the tables on C and using |C| >= 2 for distinct states in C yields the factor one half in the signed row budget.

If every epsilon(i) is zero, then g_i = F_i. The very same R reduces on every positive-weight column to the displayed subset formula, and is zero when B is not contained in C. Its zero-weight rows remain arbitrary probability rows. No positive lower bound on block weights and no optimality of the coefficients are assumed.

References