Neyman orthogonality of the partially linear DML score (Lean-verified core)

Neyman orthogonality of the partially linear DML score, Lean-verified

The conceptual heart of Double/Debiased Machine Learning (Chernozhukov et al. 2018) — why it works — formalized on the site pin (Lean v4.29.1 / Mathlib v4.29.1).

The setup

Random variables are elements of a commutative ℝ-algebra $R$; expectation is an ℝ-linear functional $E : R \to_{\ell[\mathbb R]} \mathbb R$. Partially linear model: $Y = \theta_0 D + g_0 + \varepsilon, \qquad D = m_0 + V,$ with nuisances $g_0 = \mathbb E[Y - \theta_0 D \mid X]$, $m_0 = \mathbb E[D\mid X]$ and residuals $\varepsilon, V$. The orthogonality moments $E[\varepsilon V] = 0$, $E[\varepsilon b] = 0$, $E[a V] = 0$ (the consequences of conditional-mean-zero) are taken as hypotheses.

What's proved

The DML orthogonal score partials out both nuisances: $\psi(\theta, g, m) = (Y - \theta D - g)(D - m)$.

1. Neyman orthogonality. At the truth with nuisances perturbed to $g_0 + a$, $m_0 + b$, the score reduces to $(\varepsilon - a)(V - b)$, and its expectation is $E[\psi] = E[\varepsilon V] - E[\varepsilon b] - E[aV] + E[ab] = E[a b].$ The first three terms die by the moments; what remains is second order in the perturbations $(a,b)$.
2. First-order insensitivity. Perturbing either nuisance alone ($b=0$ or $a=0$) gives expected score exactly zero — the Gâteaux derivative at the truth vanishes. This is what lets slowly-converging ML nuisance estimates not contaminate the target.
3. Contrast: the naive score $(Y-\theta D - g)D$ has expectation $-E[a\, m_0]$ — first order in the nuisance error $a$, hence biased.

formal proof

Honest scope

This formalizes the orthogonality identity — the mechanism — in a linear-functional model of expectation. It is not the DML guarantee itself: the $\sqrt n$-consistency and asymptotic normality of the cross-fitted estimator under $o(n^{-1/4})$ nuisance rates require empirical-process / CLT machinery (Donsker or cross-fitting arguments, a CLT under estimated nuisances) that I have not formalized and that isn't readily available in Mathlib. The moment conditions are hypotheses rather than derived from a conditional-expectation operator. So: the algebraic reason orthogonality buys first-order insensitivity is verified; the limit theorem that turns that into valid inference is not.

This sits in the same vein as the robust-outcome-test formalization — a result about correct inference under weaker assumptions, with the verifiable core (here, the orthogonality algebra) cleanly separated from the analytic limit theory that remains imported/informal.