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)
For a measurable sample space with a measure, an inverse-problem system, and an outcome in the sample space, the treatment-side covariate random variable is the system's covariate projection evaluated at its observation generated by that outcome.
Definition (Lean source)
For a measurable sample space with a measure, an inverse-problem system, and an outcome in the sample space, the instrument-side covariate random variable is the system's instrument projection evaluated at its observation generated by that outcome.
Definition (Lean source)
For a measurable sample space with a measure and an inverse-problem system, the scalar target is the expectation, under the measure, of the system's treatment-side moment evaluated at the system's observation and primal nuisance function.
Definition (Lean source)
For a measurable sample space with a measure, an inverse-problem system, a primal nuisance function on the covariate space, a dual nuisance function on the instrument space, and an observation, the pointwise doubly robust pseudo-outcome is the treatment-side moment plus the outcome-side moment minus the product of the dual nuisance at the observation's instrument projection and the primal nuisance at its covariate projection.
Definition (Lean source)
For a measurable sample space with a measure, an inverse-problem system, a primal nuisance function on the covariate space, a dual nuisance function on the instrument space, and an outcome in the sample space, the pseudo-outcome along the random observation is the pointwise doubly robust pseudo-outcome evaluated at the observation generated by that outcome.
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)
Membership of q₀ in the dual candidate set.
The dual moment identity.
For a measurable sample space with a measure, an inverse-problem system, a primal nuisance function on the covariate space, and a dual nuisance function on the instrument space, the doubly robust functional is the expectation, under the measure, of the doubly robust pseudo-outcome along the system's random observation.
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.hypothesesS :q₀ :S.𝒵 → ℝhq₀ :S.DualSolution q₀q :S.𝒵 → ℝhq :q ∈ S.QbarconclusionS.Θ 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.hypothesesS :q₀ :S.𝒵 → ℝhq₀ :S.DualSolution q₀h :S.𝒳 → ℝhh :h ∈ S.HbarconclusionS.Θ 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.