Estimation.NPIV
Nonparametric instrumental variables: the conditional-moment operator, sieve primal analysis, ill-posedness measures, and doubly robust NPIV functionals.
Setup 8 core · 0 supporting This file provides the substrate for the non-iterated Tikhonov regularized adversarial estimator (TRAE) of Bennett, Kallus, Mao, Newey, Syrgkanis, and Uehara (2023).
NPIV / TRAE setup: linear inverse-problem functional system
This file provides the substrate for the non-iterated Tikhonov regularized adversarial estimator (TRAE) of Bennett, Kallus, Mao, Newey, Syrgkanis, and Uehara (2023). The target is a scalar linear functional of a primal solution to a linear inverse problem; the main algebraic object is a doubly robust score built from the primal solution and from the solution of a dual inverse problem.
Mirrors the following definitions from
doc/basic_concepts/po/estimation/trae_inverse_problems.tex:
* def:est-trae-system — the linear inverse-problem functional system.
* def:est-trae-dual-solution — the dual solution q₀.
* def:est-trae-dr-functional — the doubly-robust functional Θ and its
pointwise score φ_{h,q}.
The candidate sets Hbar, Qbar are kept as plain sets of ℝ-valued functions;
the Hilbert, Lp, and projection structure is added by later operator-system
files. This setup layer records the moment-equation contract and the linearity
needed for the mixed-bias proof.
A linear inverse-problem functional system packages an observation space together with measurable treatment-side and instrument-side covariate projections of the observed data, measurable closed candidate sets for the primal and dual nuisances, each closed under subtraction, observation-level moment maps that are linear in their nuisance argument, jointly measurable and integrable against every candidate, whose cross product q(Z)h(X) is integrable as well, and a primal nuisance in the candidate set satisfying the inverse-problem moment equation against every dual candidate (def:est-trae-system).
Definition (Lean source)
Treatment-side covariate as a random variable X := xOf ∘ W.
Definition (Lean source)
Instrument-side covariate as a random variable Z := zOf ∘ W.
Definition (Lean source)
Scalar target θ₀ := E[m_e(W; h₀)] (Definition 4.5, item 6).
Definition (Lean source)
The pointwise pseudo-outcome at a sample value w : 𝒲: φ_{h,q}(w) := m_e(w; h) + m(w; q) − q(zOf w) h(xOf w).
Definition (Lean source)
The pseudo-outcome along the random observation W: φ_{h,q}(ω) := φ_{h,q}(W ω).
Definition (Lean source)
DualSolution S q₀ says q₀ ∈ Qbar and q₀ solves the dual moment identity E[m_e(W; h)] = E[q₀(Z) h(X)] for every h ∈ Hbar (def:est-trae-dual-solution).
Definition (Lean source)
The doubly-robust functional from def:est-trae-dr-functional: Θ(h, q) := E[m_e(W; h) + m(W; q) − q(Z) h(X)] = E[φ_{h,q}(W)].
Definition (Lean source)
MixedBias 1 core · 2 supporting This file proves the doubly robust mixed-bias identity for linear inverse-problem functionals. ★ mixed_bias_identity
Mixed-Bias Identity for NPIV
This file proves the doubly robust mixed-bias identity for linear inverse-problem functionals. It shows that, given a dual solution, the functional error factors as the expectation of the product of the dual nuisance error and the primal nuisance error, with immediate cancellation at either truth.
Mixed-bias / DR identity — prop:est-trae-mixed-bias. Fix a linear inverse-problem functional system, and suppose q₀ solves the associated dual moment equation. Then for any primal candidate function h in the closed candidate set Hbar and any dual candidate function q in the closed candidate set Qbar, the bias of the doubly-robust functional Θ(h, q) relative to the true target θ₀ equals the expectation of the product (q₀(Z) − q(Z))·(h(X) − h₀(X)) of the dual and primal nuisance errors.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
Θ_h₀_eq_θ₀theorem — DR cancellation at the truth on the primal side: Θ(h₀, q) = θ₀ for every q ∈ Qbar.hypothesesconclusionS.Θ S.h₀ q = S.θ₀Proof (Lean source)
theorem Θ_h₀_eq_θ₀ (S : InverseProblemSystem Ω μ) {q₀ : S.𝒵 → ℝ} (hq₀ : S.DualSolution q₀) {q : S.𝒵 → ℝ} (hq : q ∈ S.Qbar) : S.Θ S.h₀ q = S.θ₀ := by have hmb := mixed_bias_identity S hq₀ S.h₀_mem hq apply sub_eq_zero.mp rw [hmb] simp -
Θ_q₀_eq_θ₀theorem — DR cancellation at the truth on the dual side: Θ(h, q₀) = θ₀ for every h ∈ Hbar.hypothesesconclusionS.Θ h q₀ = S.θ₀Proof (Lean source)
theorem Θ_q₀_eq_θ₀ (S : InverseProblemSystem Ω μ) {q₀ : S.𝒵 → ℝ} (hq₀ : S.DualSolution q₀) {h : S.𝒳 → ℝ} (hh : h ∈ S.Hbar) : S.Θ h q₀ = S.θ₀ := by have hmb := mixed_bias_identity S hq₀ hh hq₀.mem apply sub_eq_zero.mp rw [hmb] simp
SourceCondition 2 core · 0 supporting This file records the β-source condition for the primal NPIV nuisance and the Tikhonov bias bounds assumed by the primal rate theorem.
Source Condition and Tikhonov Bias
This file records the β-source condition for the primal NPIV nuisance and the Tikhonov bias bounds assumed by the primal rate theorem. The source condition expresses the target nuisance as a spectral power of the normal operator applied to an admissible witness, while the bias bundle stores the strong and weak approximation inequalities later discharged by spectral calculus.
The β-source condition represents the true primal nuisance as the image, under a nonnegative spectral power of the normal NPIV operator, of an admissible witness function in the primal candidate class, via the spectral identity expressing the nuisance as that power of the operator applied to the witness, inside the L² space.
Definition (Lean source)
The Tikhonov bias-bound bundle records, at a positive regularization level, the properties of the corresponding population Tikhonov solution: a nonnegative constant for which its squared distance to the true nuisance in the strong candidate-space norm and its squared distance to the true nuisance in the weak operator-image norm are each bounded by that constant times a power of the regularization level, together with the population strong-convexity inequality it satisfies relative to every other candidate.