Exact CAR revelation scaling
Abstract
Mixing CAR experiments with complete revelation scales both directed deficiencies exactly and gives ordinary partition realizations on one public product seed.
Theorem 1.1 (Two directed equalities and a common partition seed).
Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/CARRevelationScaling.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
A is an arbitrary finite nonempty state type at any universe level u, with decidable equality, and n is its cardinality. Block(A) is the alphabet of all nonempty finite subsets of A. The profiles w and v take arbitrary nonnegative real values, and each CAR row sums to one. The row(u,i,B) equals u(B) if i belongs to B and zero otherwise. Singleton and zero-weight blocks remain in this alphabet.
finiteDeficiency takes the target first and the source second. It minimizes the maximum statewise half-L1 error over all stochastic kernels on the full alphabet. One kernel is used for every state; its output rows may assign mass to zero-weight target blocks and to blocks that do not contain the true state. No support restriction or prior is imposed on this minimization.
The function M mixes a profile with complete revelation: the revealing profile is one on every singleton and zero on every larger block. Both equalities hold for every real t between zero and one, with multiplication by ofReal(t) in the extended nonnegative reals. For n = 1 the only block is the unique singleton, both original profiles have weight one, and both original deficiencies vanish.
Finite Bayes minima are attained. For a probability prior mu, a finite nonempty action set D, and a loss l between zero and one, choose at each observation an action minimizing its finite sum of weighted losses. The resulting deterministic decision rule is stochastic and no randomized rule has a smaller cost. For a CAR profile u this choice separates block by block: H(B) is independent of u, including when u(B) is zero. Thus the same H applies to both profiles and their revealing mixtures.
To obtain a shared optimizing kernel and task, take stochastic experiments X and Y on O = Block(A). The kernel domain is the finite product of probability simplexes, and the second domain is the probability simplex on A times Finset(O). The displayed payoff is continuous and affine in each variable. These nonempty compact convex domains admit an actual Sion saddle (Kstar,zstar). The saddle inequalities hold for every kernel K and every state-event probability vector z.
Sum zstar over events to obtain the prior mu, and over events containing an output letter to obtain g. Then zero is at most g(i,C) and g(i,C) is at most mu(i). The loss is g(i,C)/mu(i) for positive mu(i), and zero when mu(i) is zero. In the latter case g(i,C) is also zero, so mu(i) l(i,C) = g(i,C) holds without discarding any state.
The positive-difference event of each simulated row realizes its half-L1 distance from the target row. Testing the saddle against these events and an attained Bayes decision bounds every state error of Kstar by the same task’s Bayes-risk gap. Bounded-loss risk transport gives the converse bound by deficiency, and the defining infimum bounds deficiency by the error of Kstar. All three values are equal. Probability rows bound deficiency by one, and the attained nonnegative Bayes costs are finite, so the conversions to real values in these formulas are valid.
For each fixed task, the complete-revelation contribution in the block risk formula is identical for w and v and cancels. Apply the attained task for the mixed experiments to bound their deficiency above by t times the original deficiency. Apply the attained task for the original experiments to the mixed ones to obtain the reverse inequality. Interchanging w and v proves the second directed equality. This argument includes t = 0 and never divides by t; no duality or attainment hypothesis is required.
For the partition construction suppose n is at least two and 0 <= t <= 2/n, which also implies t <= 1. For either original profile u, let S(u) be the total weight of nonsingleton blocks. Summing the CAR row equations over states counts each block weight once per member. Nonnegativity and the size of each nonsingleton give S(u) <= n/2, hence t S(u) <= 1.
For every nonempty block B form the ordinary partition with B as one part and each state outside B as its own singleton part. These parts are nonempty, pairwise disjoint, and have union A. Let T(none) be the discrete partition and T(some(B)) this partition. The selector law q(u) gives mass t u(B) to some(B) when B is nonsingleton, zero to singleton selectors, and the residual mass 1 - t S(u) to none. All masses are nonnegative and their sum is one.
A nonsingleton block B occurs with total probability t u(B). A singleton {i} occurs under the discrete selector and under exactly those nonsingleton selectors whose block omits i. The CAR row equation gives its probability 1 - t + t u({i}). Thus the induced profile is exactly M(t,u) on every block.
Use the actual product law of the two selector laws on Seed = Option(Block(A)) times Option(Block(A)). Define P from its first coordinate and Q from its second. The law is independent of the state, nonnegative, and of total mass one; its induced profiles are M(t,w) and M(t,v), respectively. Both experiments reveal the entire same seed r, together with the part containing the state. The common seed and the partition realizations are constructed, not assumed.
The experiment E(p,T) assigns p(r) to the output (r,B) precisely when B is the part of T(r) containing the state. For each of T = P and T = Q separately, let h be its induced profile, respectively M(t,w) and M(t,v). Forgetting the seed uses the deterministic kernel F((r,C),B) = indicator(C = B). For reconstruction, choose a fixed state iota and output ostar = ((none,none),{iota}) to complete each zero-weight input row. Positive-weight input rows condition the entire seed on the event that B is a part of T(r), while keeping the observed block.
The induced-profile equation makes each positive reconstruction row sum to one. If h(B) = 0 and B is a part of T(r), nonnegativity gives 0 <= p(r) <= h(B), hence p(r) = 0. This proves the reconstruction identity also on zero-weight blocks, while the fixed point mass makes those kernel rows stochastic. Finally, B is the part containing i exactly when B is a part and i belongs to B. This gives both exact channelOutput identities for P and both for Q. At t = 0 the product law concentrates on (none,none), so the same construction covers complete revelation without a positive-t assumption.