Statistics

Why the disparity is uncertain

An auditor may need to measure whether a decision rule approves members of one protected group more often than members of another. The decision, the relevant outcome, and useful proxy variables may be observed in a primary dataset, while protected class and the same proxies are observed in a separate auxiliary dataset. There is no record linking the two datasets person by person. Consequently, the two observed distributions do not determine a unique joint distribution, even if they are known without sampling error. Kallus, Mao, and Zhou study what can still be said about such fairness measures from the two marginals alone (arXiv:1906.00285v2, §§2, 4–5).

The issue is relevant whenever protected labels cannot be joined to individual decisions. Proxy methods can estimate group membership, but their errors do not disappear merely because the marginal distributions are known. A set of compatible disparity values makes the uncertainty visible. This mission treats the population result in Proposition 7 of the cited preprint; estimation from finite samples and the paper's empirical case studies are separate topics.

Observed information and compatible joints

Let decision $\hat Y\in\{0,1\}$ and true outcome $Y\in\{0,1\}$. The protected class $A\in\{a,b\}$ has two groups, with $a$ conventionally advantaged and $b$ disadvantaged. The proxy $Z$ takes values in a measurable space $\mathcal Z$; it may be categorical, continuous, or mixed. The primary marginal is $P(\hat Y,Y,Z)$, and the auxiliary marginal is $P(A,Z)$. Both share one proxy distribution $P(Z)$, as required when they arise from a common population joint law.

For each proxy value $z$, write $\eta_{\mathrm{aux}}(\alpha,z)=P(A=\alpha\mid Z=z)$ and $\eta_{\mathrm{priT}}(\hat y,y,z)=P(\hat Y=\hat y,Y=y\mid Z=z)$. Their decision marginal is $\eta_{\mathrm{pri}}(\hat y,z)=\sum_y\eta_{\mathrm{priT}}(\hat y,y,z)$. A coupling of two discrete probability vectors is a nonnegative array whose row and column sums equal those vectors. The paper's set $\mathcal P_D$ contains all measurable conditional joint arrays $\pi(\alpha,\hat y,y\mid z)$ that couple $\eta_{\mathrm{priT}}(\cdot,\cdot,z)$ and $\eta_{\mathrm{aux}}(\cdot,z)$ at each $z$, together with the fixed $P(Z)$. It imposes no additional assumptions on the unknown association of class and outcomes.

The demographic disparity of a compatible joint $P'$ is $\delta_{DD}(a,b;P')=P'(\hat Y=1\mid A=a)-P'(\hat Y=1\mid A=b)$. Its partial identification set is

$$\Delta_{DD}(\mathcal P_D)=\{\delta_{DD}(a,b;P'):P'\in\mathcal P_D\}.$$

This set lists every disparity that the two observed marginals permit, rather than selecting a particular way to combine them.

Formalization targets

For a group $\alpha$, decision $\hat y$, and proxy value $z$, define the Fréchet–Hoeffding weight endpoints

$$w^L_\alpha(\hat y,z)=\max\left\{0,1+\frac{P(A=\alpha\mid Z=z)-1}{P(\hat Y=\hat y\mid Z=z)}\right\},\qquad w^U_\alpha(\hat y,z)=\min\left\{1,\frac{P(A=\alpha\mid Z=z)}{P(\hat Y=\hat y\mid Z=z)}\right\}.$$

For a class weight function $w$, let $\mu(\alpha;w)=E[w_\alpha(\hat Y,Z)\hat Y]/P(A=\alpha)$. The goal, Proposition 7, is the equality

$$\Delta_{DD}(\mathcal P_D)= \left[\mu(a;w^L)-\mu(b;w^U),\;\mu(a;w^U)-\mu(b;w^L)\right].$$

Equality makes the interval sharp: every compatible joint produces a value inside it, and every value inside it is produced by a compatible joint. The milestones state the finite coupling bounds, the weighted description of the disparity set, the constraints on admissible weights, the numerical bounds, and attainment of both endpoint values. The source is Proposition 1, Propositions 5–7, and the proof of Proposition 7 on pp. 10 and 14–15 of the preprint (arXiv:1906.00285v2).

What the result gives

The theorem gives an exact range for the difference in group approval rates when class and decision are never observed jointly. An interval that excludes zero has an interpretation that does not depend on choosing one compatible joint law. A wide interval identifies uncertainty due to data combination itself, before finite-sample error enters. A single point signals that the observed marginals identify the demographic disparity under these conventions.

Formalizing the known result adds a reusable definition of finite couplings and a precise model of compatible conditional joints over an arbitrary measurable proxy space. The proposition is proved in the paper; the Lean goal and its milestone statements are open formalization targets. The development also records the null-cell and denominator conventions that ordinary probability notation leaves implicit. It does not claim a machine-checked proof of Proposition 7 yet.

Central difficulty

The observed data fix the class marginal and the joint decision–outcome marginal, but they do not fix their association within a proxy cell. Bounding one cell of a coupling does not by itself prove that an extreme disparity is simultaneously attainable under all marginal constraints. The true outcome $Y$ remains in the compatible-joint model even though demographic disparity uses only $\hat Y$. When a decision cell has zero probability, a conditional class weight on that cell is undefined, so pointwise weight statements require care. A set inclusion alone would miss the sharpness claim.

Formalization scope

The Lean model uses Fin 2 for each binary outcome and a two-constructor type for protected class. It represents the two observed marginals by one probability measure on $Z$ and measurable, normalized, nonnegative conditional vectors $\eta_{\mathrm{aux}}$ and $\eta_{\mathrm{priT}}$. The set $\mathcal P_D$ consists of measurable conditional couplings for every $z$. Conditional probabilities in the candidate joint are ratios of integrals of that joint array. In particular, the denominator of $\delta_{DD}(a,b;P')$ is computed from $P'$, not inserted from the auxiliary marginal.

The theorem explicitly assumes $P(A=a)>0$ and $P(A=b)>0$, since conditioning on a group of zero probability is undefined in the paper. The paper's conditional laws are defined almost everywhere; requiring a coupling at every $z$ selects a version and does not change the attainable disparities. On a cell with $P(\hat Y=\hat y\mid Z=z)=0$, weight identities and bounds are imposed only when that cell has positive probability; all weighted expectations multiply by the cell probability. The integrands arising from compatible joints and admissible weights are measurable and bounded on a probability space, so their real integrals are genuine expectations.

The identification set is built from compatible joint laws and their conditional disparity. Defining it directly as an interval or as the image of a chosen weight set would erase the content of the target. Finite coupling bounds and conditional-joint modeling can be reused outside demographic disparity. Contributions proving the milestone statements, handling measurable selections, and connecting coupling arrays to probability measures are within scope. Estimation, true-positive and true-negative disparities, and additional assumptions on the joint law are outside this mission.

Selected references

• Nathan Kallus, Xiaojie Mao, and Angela Zhou, Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination, Management Science 68(3), 2022; preprint arXiv:1906.00285v2, 2020. Pinned preprint.

Motivation

An intervention inside a continuing system can change what happens after the moment at which it is assigned. In a search service, for example, an action shown now can alter the system state that later users encounter. A simple randomized experiment therefore mixes two effects: the immediate reward of treatment and the change in the distribution of future states. Farias, Li, Peng and Zheng model this setting as a finite Markov decision process and study how to estimate the long-run effect of always using the intervention from data collected while treatment is randomized Farias et al., 2022.

The paper calls the difference between treatment and control averages the Naive estimator. It can be biased at first order in the intervention's effect on transitions, because both averages use the state distribution generated by the randomized experiment. The differences-in-Q estimator uses state-action values instead of immediate rewards. Theorem 1 asserts that its population bias is at most second order in that transition effect under a geometric mixing assumption Farias et al., 2022, Theorem 1.

Setting

Let $S$ be a finite state space. At each time, the system takes one of two actions: $0$ is control and $1$ is intervention. An action $a$ at state $s$ earns a real reward $r(s,a)$ and moves to the next state according to the row $P_a(s,\cdot)$ of a stochastic matrix $P_a$. The control policy always selects $0$; the intervention policy always selects $1$. The experiment policy selects each action with probability one half independently at each decision, so its transition matrix and expected reward vector are

$$P_{1/2}=\tfrac12(P_0+P_1),\qquad r_{1/2}=\tfrac12(r_0+r_1).$$

Write $\rho_0$, $\rho_1$ and $\rho_{1/2}$ for stationary probability distributions of these three matrices. The average treatment effect is the difference between the long-run average rewards under always intervening and always controlling:

$$\mathrm{ATE}=\rho_1^{\top}r_1-\rho_0^{\top}r_0.$$

For the experiment policy, $Q_{1/2}(s,a)$ is the expected excess reward when action $a$ is taken first at state $s$ and the experiment policy is followed thereafter. Excess means reward relative to the experiment's stationary average reward $\rho_{1/2}^{\top}r_{1/2}$. The idealized differences-in-Q value is

$$D=\sum_{s\in S}\rho_{1/2}(s)\bigl(Q_{1/2}(s,1)-Q_{1/2}(s,0)\bigr).$$

This is the population quantity whose bias Theorem 1 bounds. It is distinct from the finite-sample estimator calculated from a trajectory Farias et al., 2022, §3.1–3.2.

The mixing condition, Assumption 1, says that for every state $s$ and time $k\ge0$, the total-variation distance between the $k$-step experiment law and its stationary law is at most $C\lambda^k$. The intervention impact is measured by a second total-variation bound, $d_{\mathrm{TV}}(P_1(s,\cdot),P_0(s,\cdot))\le\delta$ for every $s$ Farias et al., 2022, Assumption 1 and Theorem 1.

Formalization targets

Second-order population bias

The goal is Theorem 1. With $r_{\max}=\max_{s,a}|r(s,a)|$, it asks for one polynomial $q$, valid uniformly over all finite models and all admissible $C$, $\lambda$ and $\delta$, such that

$$|\mathrm{ATE}-D|\le q(\log C)\left(\frac1{1-\lambda}\right)^2r_{\max}\delta^2.$$

This formalizes the paper's statement that the unspecified constant depends polynomially on $\log C$. The polynomial is quantified before the state space and the model, so its coefficients cannot be chosen from a particular example.

Source milestones

Five subtargets record the paper's route to this statement: Lemma 1's stationary-distribution perturbation identity; the corrected norm bound of Appendix F, Lemma 2; the corrected average-treatment-effect expansion in Eq. (6); the identification of the experiment's relative value with a group-inverse expression; and the identity that makes $D$ the first-order truncation Farias et al., 2022, pp. 13–15, 41. The goal and these milestones concern the idealized population estimator. Asymptotic normality and finite-sample estimation from Theorem 2 are outside this mission.

Significance

The result quantifies what the DQ adjustment buys in a dynamic experiment. When action-dependent transitions differ by at most $\delta$ in total variation, the population bias scales as $\delta^2$, with an explicit dependence on the experiment chain's mixing rate and the reward bound. This provides a statement against which variants of the estimator and sharper constants can be compared Farias et al., 2022, Theorem 1.

The theorem is proved in the cited paper; the task here is to give its claim and the supporting identities machine-checkable proofs. The finite-chain definitions, perturbation identity and group-inverse bound can be reused in other average-reward Markov-chain arguments. No machine-checked proof of this theorem or these milestones was found in the local Prove2Me catalog search for this mission.

Difficulty

The immediate-reward difference averages under $\rho_{1/2}$, whereas the treatment effect compares rewards under $\rho_1$ and $\rho_0$. Replacing both stationary laws by $\rho_{1/2}$ therefore loses a term of order $\delta$ in general. The relative-value and Q-function expressions account for that term, but their definitions involve infinite excess-reward series. A formal proof must establish their convergence from mixing and reconcile them with the matrix group inverse. It must also control the norm of that inverse with the paper's precise row norm; using a generic matrix norm would change the claim.

Formalization scope

The state type is finite, actions are Fin 2, and reward vectors take real values. The matrices $P_0$ and $P_1$ are row stochastic. Primitivity represents the §2 standing ergodicity convention for the control and intervention policies. A stationary distribution is a nonnegative vector summing to one, so an empty state space cannot satisfy the theorem's hypotheses. Total variation is half the rowwise $\ell_1$ distance. The paper's $\|M\|_{1,\infty}$ is the maximum absolute row sum, and $\mathbf1\rho^{\top}$ is a rank-one matrix. The group inverse is represented by $(I-P+\mathbf1\rho^{\top})^{-1}-\mathbf1\rho^{\top}$, used under hypotheses making the inverse valid Farias et al., 2022, Appendix A.

The relative value $V_{1/2}$ and action value $Q_{1/2}$ are sums of expected excess rewards, matching the reading of the paper's expectation formulas used in §3.3. They are not defined by the group inverse: the equivalence is a milestone. The idealized DQ value averages their action difference under $\rho_{1/2}$; the ATE uses the stationary-distribution form stated on p. 13. The goal assumes $0<\lambda<1$, as required by the mixing expression and the denominator. Its polynomial constant is uniform over all instances. These choices exclude an instance-dependent constant or a definition that builds the desired equality into $V$.

The Appendix F version of Lemma 2 is corrected with $C\ge1$: without it, the one-state case permits a negative stated upper bound. Its premise bounds the maximum row norm. The p. 14 total-variation version omits the factor of two needed to convert to that norm. Accordingly, the remainder inequality and Eq. (6) milestones use the corrected Appendix F premise; their verbatim fields preserve what the paper prints Farias et al., 2022, pp. 14, 41. Contributions that establish these identities and bounds under the stated hypotheses, including reusable finite-chain matrix results and summability facts, are within scope.

Selected references

• V. F. Farias, A. A. Li, T. Peng and A. Zheng, Markovian Interference in Experiments, arXiv preprint arXiv:2206.02371v2, 2022. Preprint.

Motivation

An experiment may compare two ways to select initial participants in a social network. Each selected seed set can lead to a different outcome, and the experiment observes only the outcome for the seed set actually selected. Chin, Eckles and Ugander study how known selection probabilities let observations from one experimental design estimate the outcomes of two other seeding strategies. Their setting includes one hop targeting and random targeting, but their statistical results apply to any two stochastic strategies with known probabilities. The central result here is their Proposition 2: the Hájek estimator, which normalizes the observed importance weights separately for the two strategies, is consistent and asymptotically normal. These properties are needed to interpret a large experiment's estimated difference and its uncertainty. Chin, Eckles and Ugander, §§2–3.3 and Proposition 2.

Setting

Let $\Omega$ be a countable space of possible seed sets, including any network information that varies across the superpopulation. Strategies $A$ and $B$ give probability mass functions $p_A$ and $p_B$ on $\Omega$. An experimental design distribution $p_\Delta$ gives the law of each observed seed set. A fixed function $y:\Omega\to\mathbb R$ records the potential outcome for each possible seed set. For a draw $S$, the observed outcome is $Y=y(S)$. The design supplies independent draws $S_0,S_1,\ldots$ with common law $p_\Delta$; the outcome is a deterministic function of each draw. The paper allows outcomes such as counts and fractions and does not require a finite seed space. Chin, Eckles and Ugander, pp. 8–9.

The strategy means are $\mu_A=\mathbb E_A[Y]$ and $\mu_B=\mathbb E_B[Y]$. Their difference is the superpopulation contrast $\tau_{\mathrm{sp}}=\mu_A-\mu_B$. For a seed set $s$ with positive design probability, its importance weights are $w_A(s)=p_A(s)/p_\Delta(s)$ and $w_B(s)=p_B(s)/p_\Delta(s)$. Write $\bar w_{A,N}=N^{-1}\sum_{i<N}w_A(S_i)$, with analogous notation for $B$. The paper's estimator in equation (7) separately normalizes the two sets of weights:

$$\widetilde\tau_N=\frac1N\sum_{i<N}\left(\frac{w_A(S_i)}{\bar w_{A,N}}-\frac{w_B(S_i)}{\bar w_{B,N}}\right)y(S_i).$$

The design can be a mixture of $p_A$ and $p_B$, but the proposition also addresses other designs. The formal statement therefore leaves $p_\Delta$ general. Chin, Eckles and Ugander, equations (2), (4), (5), (7), pp. 9–10.

Formalization targets

The first targets are the weight moment identities, the limits of the four sample averages, and almost sure consistency of $\widetilde\tau_N$. The joint central limit theorem for those averages and the variance identity connect these to the goal. These targets follow the displays and sentences in the proof of Proposition 2, Appendix A.2. Chin, Eckles and Ugander, pp. 39–40.

The goal is the corrected full strength of Proposition 2. Under full support of the design on the support of either strategy and finite second moments for the four weighted coordinates,

$$\widetilde\tau_N\longrightarrow\tau_{\mathrm{sp}}\quad\text{almost surely},\qquad \sqrt N(\widetilde\tau_N-\tau_{\mathrm{sp}})\Rightarrow\mathcal N(0,V_{\widetilde\tau}),$$

where the variance is the value specified by the paper's equation (15),

$$V_{\widetilde\tau}=\mathbb E_\Delta\!\left[ \left(\frac{\mu_Ap_A(S)-\mu_Bp_B(S)-y(S)(p_A(S)-p_B(S))}{p_\Delta(S)}\right)^2 \right].$$

The variance is determined by the two strategies, the design, and the outcomes; it is not a free variance parameter. The almost sure limit records the strong form supplied by the sample average law. Chin, Eckles and Ugander, Proposition 2 and equation (15), p. 14.

Significance

The result identifies both the value approached by the normalized estimator and its leading large sample variance. The two normalized terms are correlated because a single observed seed set contributes information about both strategies. Equation (15) retains that dependence, so the uncertainty of their difference is not obtained by adding two separate variance formulas. The paper uses this result to motivate inference for a superpopulation contrast rather than a finite collection of villages, for which a single observation per village does not identify each village's variance. Chin, Eckles and Ugander, §3.3, p. 14.

The mathematical result is published in the cited preprint. This mission asks for a machine checked statement and proof of its corrected version, plus reusable facts about weighted moments, strong laws for transformed samples, and a four coordinate central limit theorem. The proof infrastructure can serve other comparisons of two policies under a common sampling design. The Horvitz–Thompson result in Proposition 1 is related but is a separate theorem and is outside this mission. No proof of Proposition 2 is currently included in the mission's local formalization.

Difficulty

The estimator is a difference of two random ratios. At small sample sizes, either normalizing sum can vanish, and the two ratios are dependent. Applying a variance formula for one self normalized estimate twice would discard their covariance. There is also a source level obstacle: the printed positivity assumption permits the design to omit a seed set on which both strategies assign equal positive probability. Such a set does not affect the strategy contrast pointwise, but it changes the separate means and the normalizing weight expectations. The printed hypothesis therefore does not imply the moment identity used in Appendix A.2. Chin, Eckles and Ugander, Assumption 1, p. 11, and proof of Proposition 2, p. 40.

For example, take three seed sets with $p_A=(1/2,0,1/2)$, $p_B=(0,1/2,1/2)$, $p_\Delta=(1/2,1/2,0)$ and $y=(1,0,0)$. The paper's Assumption 1 holds, but $\tau_{\mathrm{sp}}=1/2$ and the Hájek estimator approaches $1$. This mission labels the replacement support condition as a correction. The printed intermediate expansion of the delta method variance also has a sign error in a cross term; equation (15) itself is retained. Chin, Eckles and Ugander, pp. 11, 14, 40.

Formalization scope

Lean represents $\Omega$ by an arbitrary countable type with measurable singletons, $p_A,p_B,p_\Delta$ by PMF, and the sample by measurable independent maps from one probability space, each with law $p_\Delta$. The natural number $N$ is the number of sampled villages: Lean uses draws $S_0,\ldots,S_{N-1}$ in place of the paper's $S_1,\ldots,S_N$. Probabilities enter real arithmetic through ENNReal.toReal; a PMF assigns finite mass to each point. Full positivity says $p_\Delta(s)>0$ whenever $p_A(s)>0$ or $p_B(s)>0$. It is stronger than the paper's contrastive Assumption 1 and is needed for the separate means and normalization identities.

The four second moment conditions apply to $w_A$, $w_B$, $w_Ay$, and $w_By$ under $p_\Delta$. They make the joint covariance finite even when $y$ is unbounded. The consistency milestone uses only the first moments it needs. The variance is the real integral from equation (15), then converted to a nonnegative real variance for Mathlib's Gaussian law. Lean's total division assigns zero weight when $p_\Delta(s)=0$; such a seed set is not observed under the design. The estimator is zero at $N=0$, and a finite sample with a zero normalizing sum uses Lean's division by zero value. The almost sure and distributional limits address the paper's asymptotic claim.

The intended statement includes every countable seed space and every qualifying independent sample. Restricting to a finite seed space, assuming the estimator's limit or a central limit theorem, or selecting an arbitrary Gaussian variance would change the claim. The development needs Mathlib's probability measures, integration, strong law, Gaussian laws, distributional convergence, and moment theory. Contributions that establish the listed milestones or develop the general joint limit and ratio tools are in scope.

Selected references

• Chin, Alex, Dean Eckles, and Johan Ugander. Evaluating Stochastic Seeding Strategies in Networks. arXiv:1809.09561v3, 2020. Preprint.

Motivation

Networks of autonomous sensors — machines on a factory floor, vehicles, devices in the Internet of Things — each measure a common environment with their own noise and can improve their estimates by asking other sensors for theirs. Communication capacity is limited, so each sensor must decide whom to ask, and the answer it receives is useful only to the extent that it understands how the other sensor turns measurements into estimates. Saghafian, Tomlin and Biller (SSRN 3124417, version of October 16, 2020; published in Manufacturing & Service Operations Management, 2021) model this as a dynamic target-selection problem and ask which communication network forms in the long run. Their abstract leads with the answer: each sensor eventually settles on a constant target set, which is sample-path dependent. With known, pairwise distinct qualities this target set is a single sensor (Proposition 4, p. 21). This mission formalizes that result.

Setting

There are $n$ sensors $N = \{1, \dots, n\}$. Sensor $i$ has a quality $q_i > 0$: its measurement of the state has noise variance $1/q_i^2$. Sensor $i$ starts with initial familiarities $v_{ij0}, w_{ij0} > 0$ with each other sensor $j$, the precisions of its initial Gaussian beliefs about $j$'s inference parameters. A sample path $S_\infty = (s_0, s_1, s_2, \dots)$ is the sequence of realized states, an arbitrary sequence of reals.

The familiarity function of $i$ with $j$ in period $t$ is a function $\psi_{ijt} : \mathbb R \to \mathbb R$. It starts at

$$\psi_{ij1}(s) = \frac{v_{ij0}^2 w_{ij0}^2}{w_{ij0}^2 + v_{ij0}^2 s^2} \qquad (12)$$

In period $t$, after $s_{t-1}$ is revealed, sensor $i$ targets the sensor of least signal variance

$$j^*_{it} = \arg\min_{j \in N\setminus\{i\}} \frac{q_j^2 + 1/\psi_{ijt}(s_{t-1})}{q_j^4}, \qquad (10)\text{–}(11)$$

with ties broken toward the lower index (footnote 11). Writing $a_{ijt} = 1$ if $j^*_{it} = j$ and $0$ otherwise, the familiarity grows by the stickiness factor:

$$\psi_{ij,t+1}(s) = \psi_{ijt}(s) + f(q_i,q_j)\,a_{ijt}, \qquad f(q_i,q_j) = \frac{1+q_i^2}{q_j^2(1+q_i^2+q_j^2)}. \qquad (14)$$

The long-run contacts of $i$ along $S_\infty$ are (Definition 2)

$$T_i(S_\infty) = \{\, j \in N\setminus\{i\} : \lim_{t\to\infty} \psi_{ijt}(s_{t-1}) = \infty \,\}. \qquad (20)$$

In Lean these are Instance (q, v, w), psi1, sigma2, stick, lowArgmin, the joint recursion fam/target, count and longRunContacts in IoTFusion.KnownQuality.

Formalization targets

Goal: Proposition 4 (p. 21)

If the qualities are asymmetric ($q_j \neq q_{j'}$ for $j \ne j'$, Definition 3), then for every sample path

$$|T_i(S_\infty)| = 1 \qquad \text{for all } i \in N.$$

No hypothesis on the state process is involved: the statement holds path by path.

Milestones

1. Proposition 2 (p. 15): the closed form $\psi_{ij,t+1}(s) = \psi_{ij1}(s) + f(q_i,q_j)\sum_{l=1}^{t} a_{ijl}$ (15).
2. Remark 1 (p. 20): $j \in T_i(S_\infty)$ iff $i$ targets $j$ infinitely often.
3. Lemma 2 (p. 21): for every $\epsilon > 0$ there is a fixed threshold $\bar\psi_\epsilon$ such that $\psi_{ijt}(s_{t-1}) > \bar\psi_\epsilon$ and $q_j/q_{j'} > 1+\epsilon$ imply $j^*_{it} \ne j'$.

Supporting items: $T_i(S_\infty) \ne \emptyset$ for $n \ge 2$ (long_run_contacts_nonempty); each sensor eventually targets one fixed sensor (eventually_constant_target, the wording of p. 5); and the rank-one precision identity (EC.66).

Significance

Proposition 4 says that, with known and distinct qualities, the long-run communication network is a functional graph — every sensor has out-degree one — although which graph forms depends on the realized states, and a sensor's eventual partner need not be the highest-quality sensor available. The paper builds on it its description of the long-run network as a random directed graph (Propositions 5–6) and its managerial discussion of early-period "momentum" in familiarity.

The result is proved in the paper; nothing in it is machine-checked. The work here is a formal proof of the deterministic core, including the existence half $T_i \neq \emptyset$, which the printed proof (p. ec22) does not give: it shows only $|T_i| \le 1$.

Difficulty

Every statement is elementary in isolation; the difficulty is that the target sequence is defined by a feedback loop. The target of period $t$ depends on familiarities, which depend on all earlier targets, which depend on earlier states. Statements about "infinitely often" therefore cannot be reduced to the behavior of any single function of $t$ fixed in advance.

The tempting argument "the highest-quality sensor eventually wins" is false: a sensor that becomes familiar early with a lower-quality partner can keep choosing it forever, so no fixed candidate for the unique contact exists. The uniqueness argument must instead compare two putative long-run contacts with each other, using a familiarity threshold that does not depend on the familiarity with the worse one (Lemma 2), and the existence half needs a separate counting argument over the finitely many possible targets.

Formalization scope

• Sensors are Fin n (0-based) with $n \ge 2$ on the existence statements; for $n = 1$ there is no other sensor and $T_i = \emptyset$.
• Periods are 0-based: Lean step $k$ is the paper's period $k+1$, the target at step $k$ uses the state $s_k$, and fam P i s k is $\psi_{ij,k+1}$.
• $q_i > 0$, and $v_{ij0}, w_{ij0}$ finite and positive, are theorem hypotheses (the paper's standing assumptions; its limiting case "fully knows", $v = w = \infty$, is not posed).
• Ties go to the lower index; "$\lim = \infty$" is Filter.Tendsto … atTop atTop; $|T_i|$ is Set.ncard; asymmetry is Function.Injective q.
• The familiarity function is defined by (12) and (14), the paper's familiarity dynamics. The paper derives (14) by Bayesian updating of the scalar $\hat\alpha_j + \hat\beta_j s_{t-1}$. Under the joint Gaussian beliefs, the update is exact for the precision at the realized state $s_{t-1}$ (the item (EC.66)), but at other states $s$ the posterior precision grows by less than $f$. Proposition 2(i) "for any $s$" is therefore a modelling choice. Every later result of the paper is derived from (15), so the dynamics (12) + (14) is the paper's operative model. Whether Proposition 4 survives under the exact bivariate posterior is open and not posed.
• Not posed: Propositions 5–6. Proposition 5's step "(EC.87): at $t^*$ the sets $T_i(S_\infty)$ are all determined" does not follow. Even with Gaussian innovations, a continuation of the path through a state near $0$ after any $t^*$ can make a never-targeted higher-quality sensor the unique long-run contact, so the printed claim fails without further assumptions on the state process. Lemma 1, Proposition 3 and Proposition 7 (unknown qualities) are outside this mission.
• Lemma 2's threshold depends on the pair $(j, j')$ in the paper's proof; the statement fixes the instance first and asks for one threshold per $\epsilon$, uniform over paths, sensors and periods (the maximum over the finitely many pairs).
• Trivializations ruled out: the target ranges over $j \neq i$ only, with a specified tie-break; familiarity and target form one trajectory determined by the instance, the sensor and the path, with no free history argument; $T_i$ is defined by divergence of $\psi_{ijt}(s_{t-1})$, not by target counts; the goal is $|T_i| = 1$, not $\le 1$; and it quantifies over every real path, with no AR(1) or typicality hypothesis.
• Infrastructure: none beyond Mathlib (finite sets, filters, $2\times2$ matrices for (EC.66)). Proofs of the milestones, of the existence half and of the goal are welcome in any order. A general lemma that "a sequence in a finite set takes some value infinitely often" with the matching Set.ncard bookkeeping would be reusable.

Selected references

• S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, SSRN 3124417, version of October 16, 2020. https://ssrn.com/abstract=3124417
• S. Saghafian, B. Tomlin, S. Biller, The Internet of Things and Information Fusion: Who Talks to Who?, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2020.0958

Motivation

Off-policy evaluation (OPE) asks for the long-run value of a target decision policy, using only data collected under a different policy. It arises wherever running the target policy is expensive or unsafe: a new treatment rule in medicine, a new recommendation or pricing rule, a candidate controller in reinforcement learning. Importance-sampling estimators reweight whole trajectories. Their variance grows exponentially with the horizon, the curse of horizon (Liu et al. 2018, arXiv:1810.12429).

Kallus and Uehara (arXiv:1909.05850, Operations Research 2022) treat infinite-horizon discounted OPE as a semiparametric estimation problem. They derive the efficiency bound under three models: non-Markov, time-varying Markov and time-invariant Markov (MDP). They then propose double reinforcement learning (DRL), an estimator that combines a q-function estimate with an estimate of the ratio between the discounted state visitation of the target policy and the state distribution of the data. In the MDP model it attains the efficiency bound. This mission formalizes the transition-sampling version of that result, Theorem 6.

Timeline:

• 2016: Jiang and Li (arXiv:1511.03722) and Thomas and Brunskill (arXiv:1604.00923) give doubly robust OPE estimators for finite horizons, built on trajectory-wise importance weights.
• 2018: Liu, Li, Tang and Zhou (arXiv:1810.12429) replace trajectory weights by stationary state-distribution ratios, removing the exponential dependence on the horizon, but without efficiency guarantees.
• 2018: Chernozhukov et al. (arXiv:1608.00060) formalize cross-fitting and Neyman orthogonality for estimation with machine-learned nuisances (double machine learning).
• 2019–2022: Kallus and Uehara derive the MDP efficiency bound (Theorem 3) and prove that cross-fitted DRL attains it (Theorem 6), also under trajectory sampling with mixing (Theorems 10–13).

Setting

States lie in a measurable space $S$ and actions in a measurable space $A$. A time-invariant MDP is a transition kernel $p(s'\mid s,a)$ and a reward kernel $p(r\mid s,a)$ with rewards in $[0,R_{\max}]$. A policy $\pi(a\mid s)$ is a kernel from $S$ to $A$. Fix a discount $\gamma\in[0,1)$, a known target policy $\pi_e$ with known initial law $p^{(0)}_{\pi_e}$, and a behavior policy $\pi_b$.

The estimand is the normalized discounted value

$$\rho^{\pi_e}=\lim_{T\to\infty}\Big(\sum_{t=0}^T\gamma^t\Big)^{-1}\mathbb E_{p_{\pi_e}}\Big[\sum_{t=0}^T\gamma^tr_t\Big].$$

The q-function is $q(s,a)=\mathbb E_{p_{\pi_e}}[\sum_k\gamma^kr_k\mid s_0=s,a_0=a]$, and $v(s)=\int q(s,a)\,\pi_e(da\mid s)$. The discounted visitation is $p^{(\infty)}_{\pi_e,\gamma}=(1-\gamma)\sum_t\gamma^t p^{(t)}_{\pi_e}$, where $p^{(t)}_{\pi_e}$ is the law of $s_t$.

Transition sampling. The data are i.i.d. observations $O_i=(s,a,r,s')$ with law $p_{\pi_b}$: $s\sim p^{(0)}_{\pi_b}$, $a\sim\pi_b(\cdot\mid s)$, and, given $(s,a)$, independently $r\sim p(\cdot\mid s,a)$ and $s'\sim p(\cdot\mid s,a)$. The law of $s'$ may differ from that of $s$.

The density ratios are $\eta(s,a)=\pi_e(a\mid s)/\pi_b(a\mid s)$ and $w(s)=p^{(\infty)}_{\pi_e,\gamma}(s)/p^{(0)}_{\pi_b}(s)$. For candidate nuisances $w',q'$, with $v'(s)=\int q'(s,a)\pi_e(da\mid s)$, the estimating function is

$$\psi(s,a,r,s';w',q')=(1-\gamma)\,\mathbb E_{p^{(0)}_{\pi_e}}[v'(s_0)]+w'(s)\eta(s,a)\big(r+\gamma v'(s')-q'(s,a)\big).$$

The cross-fitted estimator $\hat\rho_{\rm DRL}(\mathcal M_3)$ splits the sample into two folds. It fits $\hat w^{[j]},\hat q^{[j]}$ on fold $j$ and averages $\psi$ over all observations, each evaluated at the nuisances of the other fold. The efficient influence function is $\phi_{\rm eff}=w(s)\eta(s,a)(r+\gamma v(s')-q(s,a))$, and the efficiency bound is $\mathrm{EB}(\mathcal M_3)=\mathbb E[\phi_{\rm eff}^2]$.

Formalization targets

Goal: Theorem 6

Assume the following:

• $w\le C_w$ and $p_{b,S'}\le C_{S'}p_{b,S}$ (6a);
• $\eta\le C_\eta$ (added);
• $\hat w^{[j]},\hat q^{[j]}$ lie in $[0,C_w]$ and $[0,R_{\max}/(1-\gamma)]$ (6b);
• $\|\hat w^{[j]}-w\|_2,\|\hat q^{[j]}-q\|_2=o_p(1)$ (6c);
• $\sqrt n\,\|\hat w^{[j]}-w\|_2\|\hat q^{[k]}-q\|_2=o_p(1)$ for all $j,k\in\{0,1\}$ (6d, equivalent to common envelopes for both folds).

Then

$$\sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)-\frac1{\sqrt n}\sum_{i<n}\phi_{\rm eff}(O_i)\xrightarrow{p}0,\qquad \sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)\xrightarrow{d}N\big(0,\mathrm{EB}(\mathcal M_3)\big).$$

No rate exponent or learner class is fixed. Only the product rate enters.

Milestones, in proof order

1. Lemma 1 (forward): $\mathbb E[\gamma w(s)\eta(s,a)f(s')-w(s)f(s)]+(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[f]=0$ for bounded measurable $f$.
2. $\rho^{\pi_e}=\mathbb E[w(s)\eta(s,a)r]$ (p. 16).
3. Eq. (5): $\mathbb E[\psi(w',q)]=(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[v]=\rho^{\pi_e}$ for every bounded $w'$.
4. $\psi(w,q)=\rho^{\pi_e}+\phi_{\rm eff}$ pointwise (p. 22).
5. Eqs. (6)–(8): $\mathbb E[\psi(w,q')]=\rho^{\pi_e}$ for every bounded $q'$.
6. Jensen step, corrected: $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}C_\eta}\,\|\hat q-q\|_2$.
7. Term (30): $|\mathbb E\psi(\hat w,\hat q)-\rho^{\pi_e}|\le C_\eta(1+\gamma\sqrt{C_{S'}C_\eta})\|\hat w-w\|_2\|\hat q-q\|_2$.
8. Term (28), variance: $\operatorname{var}[\psi(\hat w,\hat q)-\psi(w,q)]\le2a^2\|\hat w-w\|_2^2+2b^2\|\hat q-q\|_2^2$.
9. Term (28) is $o_p(1)$: the centred fold empirical process at the opposite fold's nuisances vanishes.

Significance

Theorem 6 shows that, in a Markov model, a $\sqrt n$-consistent and efficient OPE estimator exists whose variance scales with the number of observed transitions, not trajectories. It requires no complexity (Donsker or entropy) restriction on the nuisance estimators, only a product rate. Any black-box learners with $\|\hat w-w\|_2\|\hat q-q\|_2=o_p(n^{-1/2})$, which allows two subparametric rates, give asymptotically valid confidence intervals at the efficiency bound. The mixed-bias identities (Eqs. (5)–(8)) and Lemma 1 are the same ingredients used by later minimax and adversarial estimators of $w$ and $q$.

The result is proved in the paper; nothing here is presented as open. As far as is known, none of it has a machine-checked proof: no off-policy evaluation, density-ratio characterization or cross-fitting asymptotics exists in Mathlib or on the platform. Formalizing it checks the appendix argument, which is short and contains errors (below). It also produces a reusable layer: kernel-based discounted MDPs on general measurable spaces, discounted visitation measures, and the cross-fitting plus Slutsky template that other double-machine-learning results share.

Difficulty

The obvious route is "the estimator equals the oracle average $\mathbb P_n\psi(w,q)$ plus negligible terms, then apply the CLT". Two of its steps are not routine.

First, the negligible terms are random functions evaluated at random data. The empirical-process term (28) is controlled only conditionally on the other fold, through a conditional Chebyshev argument that needs the independence structure of the split. Treating $\hat w,\hat q$ as fixed functions loses exactly this.

Second, the bias term (30) is second order only because of the mixed-bias structure. That structure rests on Lemma 1, a change-of-measure identity between the discounted visitation of $\pi_e$ and the data distribution. The printed constants are wrong. The Jensen step $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}}\|\hat q-q\|_2$ fails when $\eta$ is large: with one state, $\pi_b$ uniform on two actions and $\pi_e$ a point mass, the left side is $1$ and the right side is $1/\sqrt2$. The bound by $\|\hat w-w\|_2\|\eta\|_2\|\hat q-q\|_2$ is not a valid inequality for a triple product. Both need a bound $\eta\le C_\eta$, which the mission adds.

Formalization scope

• Spaces and kernels. $S$, $A$ are measurable spaces, the action σ-algebra countably generated (for Mathlib's jointly measurable Kernel.rnDeriv). The MDP, the policies and the observation law are Mathlib kernels and measures. The paper's base measures are not used.
• Ratios. $w$ and $\eta$ are toReal of Radon–Nikodym derivatives, not free functions satisfying an identity. Overlap ($\pi_e(\cdot\mid s)\ll\pi_b(\cdot\mid s)$, $p^{(\infty)}_{\pi_e,\gamma}\ll p^{(0)}_{\pi_b}$) is a standing assumption.
• Objects. $q$ is the discounted series, not "a solution of the Bellman equation". $\rho^{\pi_e}$ is the limit of normalized discounted sums, not $(1-\gamma)\mathbb E[v]$ or $\mathbb E[w\eta r]$; those identities are milestones. The discounted visitation is the measure $(1-\gamma)\sum_t\gamma^tp^{(t)}_{\pi_e}$, the limit of the paper's normalized averages.
• Cross-fitting. The folds are $\{i<\lfloor n/2\rfloor\}$ and the rest. Each learner is a jointly measurable function of its own fold's observations only. Rates are convergence in probability of the actual random $L^2$ errors.
• Conclusion. "RAL and efficient" is posed as asymptotic linearity with influence function $\phi_{\rm eff}$ plus the normal limit. Regularity needs the tangent-space framework of Theorem 3 and is not posed.
• Ruled out. The oracle statement with $\hat w=w$, $\hat q=q$ is an i.i.d. CLT for a fixed function and drops the theorem's content. It is not an acceptable substitute for the goal.
• Infrastructure needed. Linearity and Fubini for kernel compositions; summation of discounted occupancies; conditional Chebyshev for cross-fitted empirical processes; Slutsky (TendstoInDistribution with TendstoInMeasure) and Mathlib's i.i.d. CLT tendstoInDistribution_inv_sqrt_mul_sum_sub. The occupancy and Lemma 1 layer and the cross-fitting template are reusable beyond this mission. Proofs of any milestone, and helper lemmas on kernel powers and discounted sums, are welcome.

Selected references

• N. Kallus and M. Uehara, Efficiently Breaking the Curse of Horizon in Off-Policy Evaluation with Double Reinforcement Learning, Operations Research 70(6), 2022; arXiv:1909.05850v6 (2023). https://arxiv.org/abs/1909.05850
• Q. Liu, L. Li, Z. Tang and D. Zhou, Breaking the Curse of Horizon: Infinite-Horizon Off-Policy Estimation, NeurIPS 2018. https://arxiv.org/abs/1810.12429
• V. Chernozhukov, D. Chetverikov, M. Demirer, E. Duflo, C. Hansen, W. Newey and J. Robins, Double/Debiased Machine Learning for Treatment and Structural Parameters, The Econometrics Journal 21(1), 2018. https://arxiv.org/abs/1608.00060
• N. Jiang and L. Li, Doubly Robust Off-Policy Value Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1511.03722
• P. Thomas and E. Brunskill, Data-Efficient Off-Policy Policy Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1604.00923

Why estimation risk matters for mean-variance portfolios

Mean-variance analysis (Markowitz, 1952) tells an investor which portfolio to hold once the mean vector $\mu$ and covariance matrix $\Sigma$ of asset returns are known. In practice both are estimated from a finite window of past returns, and the portfolio built from the estimates (the plug-in portfolio) performs badly out of sample: its weights are noisy and its realized utility is often far below the theoretical optimum. A long literature asks how to choose portfolio rules that take this estimation risk into account; Kan and Zhou (2007) treat the case with a risk-free asset.

Kan, Wang and Zhou (2022) study the case without a risk-free asset, where the investor must be fully invested in $N$ risky assets. There the optimal portfolio splits into the global minimum-variance (GMV) portfolio plus a scaled zero-investment portfolio, and estimation errors enter the two parts very differently. Their §2 derives the exact expected out-of-sample utility of the family of rules that rescale the estimated zero-investment part, and the coefficient that maximizes it. This mission formalizes that derivation.

Setting

An investor chooses weights $w \in \mathbb R^N$ with $1_N' w = 1$ to maximize the mean-variance utility

$$U(w) = w'\mu - \frac{\gamma}{2}\, w'\Sigma w,$$

where $\gamma > 0$ is the risk-aversion coefficient and $\Sigma$ is positive definite. The population quantities that matter are the GMV variance $\sigma_g^2 = 1/(1_N'\Sigma^{-1}1_N)$, the GMV mean $\mu_g = 1_N'\Sigma^{-1}\mu\,\sigma_g^2$, and the squared slope of the asymptote of the minimum-variance frontier, $\psi^2 = \mu'\Sigma^{-1}\mu - \mu_g^2/\sigma_g^2 \ge 0$.

The returns $r_1, \dots, r_h$ of an estimation window of length $h$ are independent and identically distributed $\mathcal N(\mu, \Sigma)$. The maximum-likelihood estimators are $\hat\mu_t = \frac1h\sum_s r_s$ and $\hat\Sigma_t = \frac1h\sum_s (r_s - \hat\mu_t)(r_s - \hat\mu_t)'$. From them come the sample GMV portfolio and the sample zero-investment portfolio

$$\hat w_{g,t} = \frac{\hat\Sigma_t^{-1}1_N}{1_N'\hat\Sigma_t^{-1}1_N}, \qquad \hat w_{z,t} = \hat\Sigma_t^{-1}(\hat\mu_t - 1_N\hat\mu_{g,t}),$$

with $\hat\mu_{g,t} = 1_N'\hat\Sigma_t^{-1}\hat\mu_t/(1_N'\hat\Sigma_t^{-1}1_N)$. For a constant combining coefficient $\tilde c$ the paper considers

$$\hat w_t(\tilde c) = \hat w_{g,t} + \frac{\tilde c}{\gamma}\,\hat w_{z,t};$$

$\tilde c = 1$ is the plug-in rule. The expected out-of-sample utility $E[U(\hat w_t(\tilde c))]$ evaluates $U$ at the true $\mu$, $\Sigma$ and averages over the sample. The five random quantities $\mu_{g,t} = \hat w_{g,t}'\mu$, $\mu_{z,t} = \hat w_{z,t}'\mu$, $\sigma^2_{g,t} = \hat w_{g,t}'\Sigma\hat w_{g,t}$, $\sigma^2_{z,t} = \hat w_{z,t}'\Sigma\hat w_{z,t}$ and $\sigma_{gz,t} = \hat w_{g,t}'\Sigma\hat w_{z,t}$ determine it.

Formalization targets

Goal: the optimal combining coefficient (§2.3, eqs. (20)–(21))

For $N \ge 2$ and $h > N + 3$, with

$$k = \frac{(h-N)(h-N-3)}{h(h-2)}, \qquad \tilde c^* = \frac{k\psi^2}{\psi^2 + \frac{N-1}{h}},$$

the coefficient $\tilde c^*$ is the unique maximizer of $\tilde c \mapsto E[U(\hat w_t(\tilde c))]$ over $\mathbb R$, and $0 \le \tilde c^* < 1$, with $\tilde c^* > 0$ when $\psi^2 > 0$.

Lemma 1 (eq. (17))

For $h > N + 3$ and every constant $\tilde c$,

$$E[U(\hat w_t(\tilde c))] = \mu_g - \frac{\gamma(h-2)\sigma_g^2}{2(h-N-1)} + \frac{h}{\gamma(h-N-1)}\left[\tilde c\psi^2 - \frac{\tilde c^2(h-2)(h\psi^2+N-1)}{2(h-N)(h-N-3)}\right].$$

The moments (A9)–(A13) and the auxiliary moments

$$E[\mu_{g,t}] = \mu_g,\quad E[\mu_{z,t}] = \frac{h\psi^2}{h-N-1},\quad E[\sigma^2_{g,t}] = \frac{(h-2)\sigma_g^2}{h-N-1},$$ $$E[\sigma^2_{z,t}] = \frac{h(h-2)(h\psi^2+N-1)}{(h-N)(h-N-1)(h-N-3)},\quad E[\sigma_{gz,t}] = 0,$$

together with the first and second moments of the auxiliary variables $y_1$, $y_2$ of Proposition 1 that the proof of Lemma 1 uses.

Significance

The result gives a closed-form, implementable-in-principle correction to the plug-in rule: since $\tilde c^* < 1$, the investor should always under-weight the estimated zero-investment portfolio, by a factor that depends only on $h$, $N$ and $\psi^2$. Replacing $\psi^2$ by an adjusted estimator gives the paper's feasible rules (§2.4, §3), which are compared empirically in §4. The moment formulas (A9)–(A13) are of independent use: they give the exact out-of-sample mean and variance of the sample GMV and zero-investment portfolios, which recur in the shrinkage literature (for instance Lassance, Martín-Utrera and Simaan, 2024, who build on this paper's Proposition 1).

The result is proved in the paper, but the proof rests on Proposition 1, a stochastic representation of the out-of-sample moments whose detailed proof is in an online appendix. No machine-checked proof exists. On Prove2Me, Proposition 1 is posed (Open) as RiskEU.OOSUVar.kan_representation in Lassance et al.'s restatement, together with special cases (eq_IA60, eq_IA49) of the combinations $\mu_{g,t} + (\kappa/\gamma)\mu_{z,t}$ and of the portfolio variance for $\kappa \in [0, 1]$ and $h > N + 7$. The closed-form vertex of the quadratic (17) is already proved there (RiskEU.RobustShrink.proposition_IA_1_3). What this mission adds is the statement about the actual expectation over the Gaussian sample, for all real $\tilde c$, under the paper's own threshold $h > N + 3$, with uniqueness of the maximizer.

Difficulty

Once Lemma 1 is available, the goal is the vertex of a concave quadratic. The difficulty is Lemma 1 itself: computing expectations of quadratic forms in $\hat\Sigma_t^{-1}$ and in the normalized vector $\hat\Sigma_t^{-1}1_N/(1_N'\hat\Sigma_t^{-1}1_N)$. The weights are ratios of dependent random quantities, so linearity of expectation does not apply directly, and inverse-Wishart moment formulas alone do not cover the ratio in $\hat w_{g,t}$. The threshold $h > N + 3$ is Lemma 1's hypothesis; the factor $h-N-3$ in the denominator of (A12) shows that it is what keeps the expected variance of the estimated zero-investment portfolio finite, so integrability is part of the content.

Formalization scope

The model is the published definition RiskEU.OOSUVar.Setting: Market N carries $\mu$, $\Sigma$, $\gamma$; sigmaG2, muG, psi2, U, sampleMean, sampleCov (divided by $h$), wHatG, wHatZ and IsGaussianSample are the objects above (that setting calls the window $T$; here it is $h$). The auxiliary family of Proposition 1 and $y_1$, $y_2$ come from the published RiskEU.OOSUVar.KanRepresentation. The mission's own definitions (KanCombine.Optimal.Model) add the standing assumptions, the combining portfolio, the five sample moments, the expected utility, $k$ and $\tilde c^*$.

Conventions committed to:

• $N \ge 2$, $\Sigma \succ 0$ and $\gamma > 0$ are explicit hypotheses (implicit in the paper); $h > N + 3$ is Lemma 1's. The $y$-moment milestone also assumes $N > 3$, as Proposition 1 does.
• $\tilde c$ ranges over all of $\mathbb R$, and "the optimal value" is stated as a unique maximizer.
• Every expectation identity asserts integrability: a Lean Bochner integral of a non-integrable function is $0$.
• Lean's matrix inverse is $0$ on singular matrices; $\hat\Sigma_t$ is almost surely nonsingular for $h > N$, so this does not change any expectation.
• The page's "$0 < \tilde c^* < 1$" fails at $\psi^2 = 0$, where $\tilde c^* = 0$; the goal states $0 \le \tilde c^* < 1$ and $\tilde c^* > 0$ under $\psi^2 > 0$.

The goal is about the integral over the Gaussian sample. Stating it about the closed-form right-hand side of (17) would reduce it to the vertex of a quadratic, which is already proved, and is ruled out. The hypotheses are satisfiable: $N = 2$, $h = 6$, $\mu = (0, 1)$, $\Sigma = I$, $\gamma = 1$ meets them with the product Gaussian sample, and gives $\tilde c^* = 1/8$.

A complete development needs Wishart and inverse-Wishart theory (the Bartlett decomposition, moments of chi-squared ratios) and a formal version of Proposition 1. These are reusable well beyond this mission; contributions proving (A9)–(A13) by any route, including directly from inverse-Wishart moments, are welcome.

Selected references

• R. Kan, X. Wang and G. Zhou, Optimal portfolio choice with estimation risk: No risk-free asset case, Management Science 68(3), 2022 (cited from the submitted manuscript, November 2020). https://doi.org/10.1287/mnsc.2021.3989 ; https://ssrn.com/abstract=2819254
• R. Kan and G. Zhou, Optimal portfolio choice with parameter uncertainty, Journal of Financial and Quantitative Analysis 42(3), 2007. https://doi.org/10.1017/S0022109000004129
• H. Markowitz, Portfolio selection, Journal of Finance 7(1), 1952. https://doi.org/10.1111/j.1540-6261.1952.tb01525.x
• N. Lassance, A. Martín-Utrera and M. Simaan, The risk of expected utility under parameter uncertainty, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.00178
• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982. https://doi.org/10.1002/9780470316559

Motivation

Personalized decisions in medicine, marketing and public policy are increasingly learned from observational data: records of who received which treatment and how it turned out. Standard policy-learning methods assume unconfoundedness, that treatment assignment depends only on observed covariates. When an unobserved factor influences both the treatment and the outcome, these methods can return a policy that is worse than the status quo, and nothing in the data reveals it.

Kallus and Zhou (arXiv:1805.08593, published in Management Science 2021 as Minimax-Optimal Policy Learning Under Unobserved Confounding) take the robust route. They fix a bound $\Gamma \ge 1$ on how far the unobserved confounding may distort the propensity scores, in the marginal sensitivity model of Tan (2006), and learn the policy that minimizes the worst-case regret against a baseline policy $\pi_0$ over every distortion the model allows. The paper proves two guarantees for this policy: it never does worse than the baseline up to vanishing terms (Theorem 2), and it is asymptotically minimax-optimal (Corollary 7). This mission is about the second.

Setting

Data are iid triples $(X, T, Y)$: covariates $X \in \mathcal X$, one of $m \ge 2$ treatments $T \in \{0, \dots, m-1\}$, and a real outcome $Y$, read as a loss. The nominal propensity is $\tilde e_t(x) = P(T = t \mid X = x)$. A policy $\pi$ assigns to each $x$ a probability vector $\pi(\cdot \mid x)$ over treatments; $\Pi$ is a class of policies and $\pi_0$ a baseline.

Inverse propensity weights $W(t,x,y)$ are unknown under confounding. The marginal sensitivity model with parameter $\Gamma$ confines them to the weight box

$$a^\Gamma_t(x) \le W(t,x,y) \le b^\Gamma_t(x), \qquad a^\Gamma_t(x) = 1 + \Gamma^{-1}\big(\tfrac{1}{\tilde e_t(x)} - 1\big), \quad b^\Gamma_t(x) = 1 + \Gamma\big(\tfrac{1}{\tilde e_t(x)} - 1\big).$$

The set of such weight functions is $\mathcal W^\Gamma$, and its restriction to a sample of size $n$ is the box $\mathcal W^\Gamma_n \subseteq \mathbb R^n$.

For weights $W$, the Hájek regret of $\pi$ against $\pi_0$ is $R_{\pi_0}(\pi; W) = \sum_{t=0}^{m-1} R^{(t)}_{\pi_0}(\pi; W)$ with

$$R^{(t)}_{\pi_0}(\pi; W) = \frac{\mathbb E\big[\mathbb I[T=t]\,(\pi(t\mid X) - \pi_0(t\mid X))\, W(T,X,Y)\, Y\big]}{\mathbb E\big[\mathbb I[T=t]\, W(T,X,Y)\big]},$$

and $\hat R_{\pi_0}(\pi; W)$ is the same expression with $\mathbb E$ replaced by the sample average $\mathbb E_n$. The worst-case regrets are

$$\bar R_{\pi_0}(\pi; \mathcal W^\Gamma) = \sup_{W \in \mathcal W^\Gamma} R_{\pi_0}(\pi; W), \qquad \hat{\bar R}_{\pi_0}(\pi; \mathcal W^\Gamma_n) = \sup_{W \in \mathcal W^\Gamma_n} \hat R_{\pi_0}(\pi; W).$$

The learned policy $\hat{\bar\pi}$ minimizes $\hat{\bar R}_{\pi_0}(\cdot\,; \mathcal W^\Gamma_n)$ over $\Pi$; the population minimax regret is $\inf_{\pi\in\Pi} \bar R_{\pi_0}(\pi; \mathcal W^\Gamma)$.

The complexity of $\Pi$ is measured by its VC-major dimension (Definition 1): the largest $v$ such that some $v$ points $(t_j, x_j)$ have all $2^v$ subsets cut out by superlevel sets $\{(t,x) : \pi(t\mid x) > \theta\}$, $\pi \in \Pi$, $\theta \in \mathbb R$. The standing assumptions are bounded outcomes $|Y| \le B$ (Assumption 1), overlap with constant $\nu > 0$ (Assumption 2), and VC-major dimension of $\Pi$ at most $v$ (Assumption 3).

Formalization targets

Goal: Corollary 7 (p. 15)

There is a constant $K$ depending only on $v$ such that, with probability at least $1-\delta$,

$$\bar R_{\pi_0}(\hat{\bar\pi}; \mathcal W^\Gamma) \le \inf_{\pi \in \Pi} \bar R_{\pi_0}(\pi; \mathcal W^\Gamma) + 36(12 + \nu^{-1})\big(BK + \nu^{-1}(\Gamma - \Gamma^{-1})(K + B + m)\big)\sqrt{\frac{\log(15m/\delta)}{n}}.$$

Milestones

1. Proposition 3 and Corollary 4: each treatment's worst case over the box is attained among monotone weights $a^\Gamma_t(x) + u\big(y(\pi(t\mid x) - \pi_0(t\mid x))\big)(b^\Gamma_t(x) - a^\Gamma_t(x))$, $u$ nondecreasing into $[0,1]$, in the population and in every sample.
2. Lemma 5: $\sup h - \sup g \le \sup (h - g)$.
3. Lemma 2: uniform deviation of $(\pi(T\mid X) - 1/m)Y$ over $\Pi$, at rate $\tfrac92 C\sqrt K (v+2)\sqrt{\log(5/\delta)/n}$.
4. Lemma 3 and Corollary 15: for a fixed policy, uniform deviation over monotone $u$, at rate $9\sqrt{2\pi\log(1/p)/n}$, overall and per treatment.
5. Lemma 4: the same jointly over $\Pi$ and $u$, given the VC-major dimension of the composition class.
6. Theorem 6 (as proved): with probability at least $1-\delta$, $\sup_{\pi\in\Pi} |\hat{\bar R}_{\pi_0}(\pi; \mathcal W^\Gamma_n) - \bar R_{\pi_0}(\pi; \mathcal W^\Gamma)|$ is at most the goal's rate with $18$ in place of $36$.

Significance

The result. Corollary 7 says that the confounding-robust policy loses at most $O(n^{-1/2})$ against the best possible worst-case guarantee in its class. The worst-case regret $\bar R_{\pi_0}(\pi; \mathcal W^\Gamma)$ cannot be identified from data. It is the regret the decision maker must budget for when the confounding is only known to lie within $\Gamma$. With Theorem 2, it makes the procedure both safe and asymptotically optimal among safe procedures, for randomized and multi-treatment policy classes of finite VC-major dimension.

Formalizing it. The paper's proof of the dimension-only dependence of $K$ is incomplete. Its Proposition 5, which states that the monotone weight class $\bar{\mathcal W}^\Gamma = \bigcup_{\pi\in\Pi} \bar{\mathcal W}^\Gamma(\pi)$ has finite VC-major dimension under Assumption 3, is false as printed. A class of monotone policies on $[0,1]$ with VC-major dimension at most $2$ gives a $\bar{\mathcal W}^\Gamma$ that shatters arbitrarily large grids. The printed proof of Theorem 6 runs through Proposition 5 and Lemma 4, so Theorem 6 and Corollary 7 are believed true but are not established by the paper. A formal proof would settle the claim. None of the statements has a machine-checked proof.

Difficulty

The worst case over $\mathcal W^\Gamma$ is a supremum over an essentially arbitrary bounded function class, which is far too large for a uniform law of large numbers. Proposition 3 reduces it to monotone transformations of the score $y(\pi(t\mid x) - \pi_0(t\mid x))$. This is a linear-fractional program whose population version lives in a function space. The natural next step is to apply a uniform law over the pairs $(\pi, u)$. That step needs a complexity bound on the composition $u \circ \text{score}_\pi$ in terms of the dimension of $\Pi$ alone, and this is exactly where the printed argument fails. A different route is needed. One candidate exploits the Lipschitz dependence of the worst-case Hájek value on the scores. The Hájek ratios also need denominators bounded away from zero uniformly. The paper's decomposition (p. 42) uses $\mathbb E[W\,\mathbb I[T=t]] = 1$, which holds for the true weights only.

Formalization scope

All statements live in the namespace ConfoundRobust.Minimax, with one definitions file Setting.

• Data and sampling. An observation is a point of 𝒳 × Fin m × ℝ, with treatments 0-indexed as on the page. The population is a probability measure μ, and a sample is ω : Fin n → Obs 𝒳 m under Measure.pi. $\mathbb E_n$ is $(1/n)\sum_i$.
• Policies and propensity. A policy is π : 𝒳 → Fin m → ℝ, with π x t $= \pi(t \mid x)$, measurable and simplex-valued. The nominal propensity is a measurable version of $P(T = t \mid X = x)$, given by its defining integral identity, with $\nu \le \tilde e \le 1$.
• Assumptions. Assumption 1 is $|Y| \le B$ almost surely. Assumption 2 enters only through its observable consequence $\tilde e_t(x) \ge \nu$; this is a weaker hypothesis, so the statements are at least as strong. Assumption 3 is the predicate "VC-major dimension at most $v$" on the functions $(t,x) \mapsto \pi(t\mid x)$.
• Weights and suprema. Weight functions in $\mathcal W^\Gamma$ are measurable. Suprema and infima are real sSup/sInf; the weight sets are nonempty (they contain $1/\tilde e$) and the regrets are bounded, so these are true extrema. An empty treatment group gives a Hájek ratio $0/0 = 0$.
• Probability statements. "With probability at least $1-\delta$" means a measurable event of that product measure on which the bound holds for every policy. $\hat{\bar\pi}$ is any sample minimizer.
• Constants. In the goal, Theorem 6, Lemma 2 and Lemma 4 the constant $K$ is quantified as ∀ v, ∃ K, ∀ (everything else). Letting $K$ depend on $\Pi$, $\mu$, $n$ or $\delta$ would trivialize the bound and is ruled out.
• Disclosed readings.
  • Lemmas 3, 4 and Corollary 15 are posed for $p \le 1/2$: as printed (every $p$) they are false for $p$ near $1$.
  • The clipped bounds of Corollary 15 and Lemma 4 (PDF p. 41) are reconstructed.
  • Lemma 2 drops "for $n$ large enough", which its proof does not use.
  • Lemma 2, Theorem 6 and the goal assume $\Pi$ is pointwise separable (a countable subclass approximates every policy pointwise), and Lemma 4 assumes the same of its composition class. This is the measurability condition of the empirical-process tools the proofs use. Without it the uniform statements fail (initial segments of $\omega_1$ under the countable–cocountable measure).
  • Theorem 6 uses $18$, the constant its proof ends with. The goal's $36$ follows from it, but not from the printed Theorem 6.
  • The printed proof of Theorem 6 passes through Proposition 5, which is false as printed. Do not expect that route to work. Lemma 4 is kept as a statement about the composition class's own dimension.

A complete development needs: linear-fractional optimization over function boxes; Dudley-type entropy bounds for VC-major and VC-hull classes; the Dvoretzky–Kiefer–Wolfowitz inequality with Massart's constant (posed separately on the platform as MassartDKW.Tight.corollary_1); and a uniform bound for Hájek ratios. The empirical-process pieces (VC-major classes, monotone classes) are reusable well beyond this mission. Contributions to any milestone, and alternative routes to Theorem 6 that avoid Proposition 5, are welcome.

Selected references

• N. Kallus and A. Zhou, Confounding-Robust Policy Improvement, arXiv:1805.08593v3, 2019; published as Minimax-Optimal Policy Learning Under Unobserved Confounding, Management Science, 2021. https://arxiv.org/abs/1805.08593v3
• Z. Tan, A distributional approach for causal inference using propensity scores, Journal of the American Statistical Association 101(476), 2006. https://doi.org/10.1198/016214506000000023
• P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3), 1990. https://doi.org/10.1214/aop/1176990746
• A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2