Estimation.NPIV

Nonparametric instrumental variables: the conditional-moment operator, sieve primal analysis, ill-posedness measures, and doubly robust NPIV functionals.

Operator 47 core · 40 supporting · 7 submodules Extends the inverse-problem system with population operators for NPIV estimation. Primal 30 core · 17 supporting · 3 submodules The sieve primal NPIV analysis: projected residuals, variance and bias terms, and the rate theorem for the structural function. DR 11 core · 5 supporting · 4 submodules Doubly robust estimation of linear functionals of the NPIV structural function.
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 closed under subtraction. No topological closedness or minimum-norm property is recorded here. Later operator-system files add an ambient Lp formulation; this setup layer records only the moment-equation contract and the linearity needed for the mixed-bias proof.

structure InverseProblemSystem reviewed
Causalean.Estimation.NPIV

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 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)
parameters
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
fields
Observation type.
𝒲 :
Type*
"Action" / treatment-side covariate type used by `Hbar`-side functions.
𝒳 :
Type*
Instrument-side covariate type used by `Qbar`-side functions.
𝒵 :
Type*
inst𝒲 :
MeasurableSpace 𝒲
inst𝒳 :
MeasurableSpace 𝒳
inst𝒵 :
MeasurableSpace 𝒵
Observed data point.
W :
Ω → 𝒲
meas_W :
@Measurable Ω 𝒲 _ inst𝒲 W
Treatment-side projection from `𝒲` to `𝒳`.
xOf :
𝒲 → 𝒳
Instrument-side projection from `𝒲` to `𝒵`.
zOf :
𝒲 → 𝒵
meas_xOf :
@Measurable 𝒲 𝒳 inst𝒲 inst𝒳 xOf
meas_zOf :
@Measurable 𝒲 𝒵 inst𝒲 inst𝒵 zOf
Candidate set for the primal nuisance (`Hbar ⊆ L²(P_X)` in the TeX; here it is a plain set of measurable ℝ-valued functions, without a topological-closedness field).
Hbar :
Set (𝒳 → ℝ)
Candidate set for the dual nuisance (`Qbar ⊆ L²(P_Z)` in the TeX; here it is a plain set of measurable ℝ-valued functions, without a topological-closedness field).
Qbar :
Set (𝒵 → ℝ)
meas_of_Hbar :
∀ h ∈ Hbar, Measurable h
meas_of_Qbar :
∀ q ∈ Qbar, Measurable q
Closure under subtraction (the only algebraic property the mixed-bias proof needs; standing in for the closed-linear-subspace assumption).
Hbar_sub :
∀ h₁ ∈ Hbar, ∀ h₂ ∈ Hbar, (fun x => h₁ x - h₂ x) ∈ Hbar
Qbar_sub :
∀ q₁ ∈ Qbar, ∀ q₂ ∈ Qbar, (fun z => q₁ z - q₂ z) ∈ Qbar
Observation-level moment map `m(W; q)`, linear in the dual nuisance argument `q`.
m :
𝒲 → (𝒵 → ℝ) → ℝ
Observation-level moment map `m_e(W; h)`, linear in the primal nuisance argument `h`.
m_e :
𝒲 → (𝒳 → ℝ) → ℝ
Linearity of `m` over subtraction in the dual argument.
m_sub :
∀ (w : 𝒲) (q₁ q₂ : 𝒵 → ℝ), m w (fun z => q₁ z - q₂ z) = m w q₁ - m w q₂
Linearity of `m_e` over subtraction in the primal argument.
m_e_sub :
∀ (w : 𝒲) (h₁ h₂ : 𝒳 → ℝ), m_e w (fun x => h₁ x - h₂ x) = m_e w h₁ - m_e w h₂
Joint measurability of `ω ↦ m(W ω; q)` for `q ∈ Qbar`.
measurable_m :
∀ q ∈ Qbar, Measurable (fun ω => m (W ω) q)
Joint measurability of `ω ↦ m_e(W ω; h)` for `h ∈ Hbar`.
measurable_m_e :
∀ h ∈ Hbar, Measurable (fun ω => m_e (W ω) h)
Integrability of `ω ↦ m(W ω; q)` for `q ∈ Qbar`.
integrable_m :
∀ q ∈ Qbar, Integrable (fun ω => m (W ω) q) μ
Integrability of `ω ↦ m_e(W ω; h)` for `h ∈ Hbar`.
integrable_m_e :
∀ h ∈ Hbar, Integrable (fun ω => m_e (W ω) h) μ
Integrability of the cross product `q(Z) · h(X)` for `h ∈ Hbar, q ∈ Qbar`, where `X = xOf ∘ W` and `Z = zOf ∘ W`.
integrable_qh :
∀ h ∈ Hbar, ∀ q ∈ Qbar, Integrable (fun ω => q (zOf (W ω)) * h (xOf (W ω))) μ
Primal nuisance candidate `h₀ ∈ Hbar` satisfying the moment equation.
h₀ :
𝒳 → ℝ
h₀_mem :
h₀ ∈ Hbar
Primal moment identity (Definition 4.5, item 5): `E[m(W; q)] = E[h₀(X) q(Z)]` for every `q ∈ Qbar`.
primal_moment :
∀ q ∈ Qbar, ∫ ω, m (W ω) q ∂μ = ∫ ω, h₀ (xOf (W ω)) * q (zOf (W ω)) ∂μ
Causalean.Estimation.NPIV.InverseProblemSystem · Causalean/Estimation/NPIV/Setup.lean:46
def X reviewed
Causalean.Estimation.NPIV.InverseProblemSystem

The treatment-side covariate random variable of an inverse-problem system on a measured sample space sends each outcome to the covariate projection of its generated observation.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
S :
InverseProblemSystem Ω μ
ω :
Ω
def
X S ω :
S.𝒳
given by
S.xOf (S.W ω)
Causalean.Estimation.NPIV.InverseProblemSystem.X · Causalean/Estimation/NPIV/Setup.lean:149 · uses InverseProblemSystem
def Z reviewed
Causalean.Estimation.NPIV.InverseProblemSystem

The instrument-side covariate random variable of an inverse-problem system on a measured sample space sends each outcome to the instrument projection of its generated observation.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
S :
InverseProblemSystem Ω μ
ω :
Ω
def
Z S ω :
S.𝒵
given by
S.zOf (S.W ω)
Causalean.Estimation.NPIV.InverseProblemSystem.Z · Causalean/Estimation/NPIV/Setup.lean:154 · uses InverseProblemSystem
def θ₀ reviewed
Causalean.Estimation.NPIV.InverseProblemSystem

The scalar target of an inverse-problem system on a measured sample space is the expected treatment-side moment evaluated at the true primal nuisance.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
S :
InverseProblemSystem Ω μ
def
θ₀ S :
ℝ
given by
∫ ω, S.m_e (S.W ω) S.h₀ ∂μ
Causalean.Estimation.NPIV.InverseProblemSystem.θ₀ · Causalean/Estimation/NPIV/Setup.lean:159 · uses InverseProblemSystem
def phiVal reviewed
Causalean.Estimation.NPIV.InverseProblemSystem

The pointwise doubly robust pseudo-outcome for an inverse-problem system on a measured sample space combines a primal nuisance and a dual nuisance at an observation as the treatment-side moment plus the outcome-side moment minus their covariate–instrument product.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
S :
InverseProblemSystem Ω μ
h :
S.𝒳 → ℝ
q :
S.𝒵 → ℝ
w :
S.𝒲
def
phiVal S h q w :
ℝ
given by
S.m_e w h + S.m w q - q (S.zOf w) * h (S.xOf w)
Causalean.Estimation.NPIV.InverseProblemSystem.phiVal · Causalean/Estimation/NPIV/Setup.lean:164 · uses InverseProblemSystem
def phi reviewed
Causalean.Estimation.NPIV.InverseProblemSystem

The pseudo-outcome along the random observation evaluates the pointwise score of an inverse-problem system on a measured sample space, using a primal nuisance and a dual nuisance, at the observation generated by the given outcome.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
S :
InverseProblemSystem Ω μ
h :
S.𝒳 → ℝ
q :
S.𝒵 → ℝ
ω :
Ω
def
phi S h q ω :
ℝ
given by
S.phiVal h q (S.W ω)
Causalean.Estimation.NPIV.InverseProblemSystem.phi · Causalean/Estimation/NPIV/Setup.lean:178 · uses InverseProblemSystem
structure DualSolution reviewed
Causalean.Estimation.NPIV.InverseProblemSystem

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)
parameters
Ω :
Type u_1
shared
μ :
Measure Ω
shared
S :
InverseProblemSystem Ω μ
q₀ :
S.𝒵 → ℝ
assumes
mem :
q₀ ∈ S.Qbar

Membership of q₀ in the dual candidate set.

identity :
∀ h ∈ S.Hbar, ∫ ω, S.m_e (S.W ω) h ∂μ = ∫ ω, q₀ (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ

The dual moment identity.

Causalean.Estimation.NPIV.InverseProblemSystem.DualSolution · Causalean/Estimation/NPIV/Setup.lean:189 · uses InverseProblemSystem
def Θ reviewed
Causalean.Estimation.NPIV.InverseProblemSystem

The doubly robust functional for an inverse-problem system on a measured sample space is the expected pseudo-outcome formed from a primal nuisance and a dual nuisance.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
S :
InverseProblemSystem Ω μ
h :
S.𝒳 → ℝ
q :
S.𝒵 → ℝ
def
Θ S h q :
ℝ
given by
∫ ω, S.phi h q ω ∂μ
Causalean.Estimation.NPIV.InverseProblemSystem.Θ · Causalean/Estimation/NPIV/Setup.lean:202 · uses InverseProblemSystem
Mixed­Bias 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.

theorem mixed_bias_identity reviewed
Causalean.Estimation.NPIV

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 Hbar and any dual candidate function q in 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
hypotheses
Ω :
Type u_1
Measure Ω
shared
S :
InverseProblemSystem Ω μ
q₀ :
S.𝒵 → ℝ
hq₀ :
S.DualSolution q₀
h :
S.𝒳 → ℝ
hh :
h ∈ S.Hbar
q :
S.𝒵 → ℝ
hq :
q ∈ S.Qbar
conclusion
S.Θ h q - S.θ₀ = ∫ ω, (q₀ (S.Z ω) - q (S.Z ω)) * (h (S.X ω) - S.h₀ (S.X ω)) ∂μ
Proof (Lean source)
theorem mixed_bias_identity (S : InverseProblemSystem Ω μ) {q₀ : S.𝒵 → ℝ} (hq₀ : S.DualSolution q₀) {h : S.𝒳 → ℝ} (hh : h ∈ S.Hbar) {q : S.𝒵 → ℝ} (hq : q ∈ S.Qbar) : S.Θ h q - S.θ₀ = ∫ ω, (q₀ (S.Z ω) - q (S.Z ω)) * (h (S.X ω) - S.h₀ (S.X ω)) ∂μ := by -- Integrability witnesses for each piece appearing in the proof. have h_int_meh := S.integrable_m_e h hh have h_int_meh₀ := S.integrable_m_e S.h₀ S.h₀_mem have h_int_mq := S.integrable_m q hq have h_int_qh := S.integrable_qh h hh q hq have h_int_q₀h := S.integrable_qh h hh q₀ hq₀.mem have h_int_q₀h₀ := S.integrable_qh S.h₀ S.h₀_mem q₀ hq₀.mem have h_int_qh₀ := S.integrable_qh S.h₀ S.h₀_mem q hq -- Reordered version (the primal moment uses `h₀(X) · q(Z)` not `q(Z) · h₀(X)`). have h_int_h₀q : Integrable (fun ω => S.h₀ (S.xOf (S.W ω)) * q (S.zOf (S.W ω))) μ := by have h := h_int_qh₀ simpa [mul_comm] using h -- Step 1: distribute the LHS over its three summands. have hΘ_eq : S.Θ h q = (∫ ω, S.m_e (S.W ω) h ∂μ) + (∫ ω, S.m (S.W ω) q ∂μ) - (∫ ω, q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ) := by unfold InverseProblemSystem.Θ InverseProblemSystem.phi InverseProblemSystem.phiVal calc ∫ ω, S.m_e (S.W ω) h + S.m (S.W ω) q - q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ = (∫ ω, S.m_e (S.W ω) h + S.m (S.W ω) q ∂μ) - ∫ ω, q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ := integral_sub (h_int_meh.add h_int_mq) h_int_qh _ = (∫ ω, S.m_e (S.W ω) h ∂μ) + (∫ ω, S.m (S.W ω) q ∂μ) - ∫ ω, q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ := by rw [integral_add h_int_meh h_int_mq] -- Step 2: dual identity applied at `h - h₀ ∈ Hbar` gives -- ∫ m_e(W; h) − ∫ m_e(W; h₀) -- = ∫ q₀(Z) · (h(X) − h₀(X)) ∂μ. have h_sub_mem : (fun x => h x - S.h₀ x) ∈ S.Hbar := S.Hbar_sub h hh S.h₀ S.h₀_mem have h_dual := hq₀.identity (fun x => h x - S.h₀ x) h_sub_mem have h_me_sub_pw : ∀ ω, S.m_e (S.W ω) (fun x => h x - S.h₀ x) = S.m_e (S.W ω) h - S.m_e (S.W ω) S.h₀ := fun ω => S.m_e_sub (S.W ω) h S.h₀ have h_me_diff_eq : (∫ ω, S.m_e (S.W ω) h ∂μ) - (∫ ω, S.m_e (S.W ω) S.h₀ ∂μ) = ∫ ω, q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω))) ∂μ := by rw [← integral_sub h_int_meh h_int_meh₀] have hcongr : (fun ω => S.m_e (S.W ω) h - S.m_e (S.W ω) S.h₀) = (fun ω => S.m_e (S.W ω) (fun x => h x - S.h₀ x)) := by funext ω exact (h_me_sub_pw ω).symm rw [hcongr, h_dual] -- Step 3: primal moment identity at `q`: -- ∫ m(W; q) ∂μ = ∫ h₀(X) · q(Z) ∂μ. have h_prim := S.primal_moment q hq -- Step 4: rewrite the RHS as a sum of three atomic integrals. have hRHS_eq : (∫ ω, (q₀ (S.Z ω) - q (S.Z ω)) * (h (S.X ω) - S.h₀ (S.X ω)) ∂μ) = (∫ ω, q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω))) ∂μ) + (∫ ω, S.h₀ (S.xOf (S.W ω)) * q (S.zOf (S.W ω)) ∂μ) - (∫ ω, q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ) := by -- Pointwise expansion: (q₀ − q)·(h − h₀) = q₀·(h − h₀) + h₀·q − q·h. have h_int_diff_q₀ : Integrable (fun ω => q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω)))) μ := by have : (fun ω => q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω)))) = (fun ω => q₀ (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) - q₀ (S.zOf (S.W ω)) * S.h₀ (S.xOf (S.W ω))) := by funext ω; ring rw [this]; exact h_int_q₀h.sub h_int_q₀h₀ -- ∫ (q₀ − q)·(h − h₀) = ∫ q₀·(h − h₀) + ∫ h₀·q − ∫ q·h have h_pw : ∀ ω, (q₀ (S.Z ω) - q (S.Z ω)) * (h (S.X ω) - S.h₀ (S.X ω)) = q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω))) + S.h₀ (S.xOf (S.W ω)) * q (S.zOf (S.W ω)) - q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) := fun ω => by simp only [InverseProblemSystem.X, InverseProblemSystem.Z] ring have hcongr : (fun ω => (q₀ (S.Z ω) - q (S.Z ω)) * (h (S.X ω) - S.h₀ (S.X ω))) = (fun ω => q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω))) + S.h₀ (S.xOf (S.W ω)) * q (S.zOf (S.W ω)) - q (S.zOf (S.W ω)) * h (S.xOf (S.W ω))) := by funext ω; exact h_pw ω rw [hcongr] calc ∫ ω, q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω))) + S.h₀ (S.xOf (S.W ω)) * q (S.zOf (S.W ω)) - q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ = (∫ ω, q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω))) + S.h₀ (S.xOf (S.W ω)) * q (S.zOf (S.W ω)) ∂μ) - ∫ ω, q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ := integral_sub (h_int_diff_q₀.add h_int_h₀q) h_int_qh _ = (∫ ω, q₀ (S.zOf (S.W ω)) * (h (S.xOf (S.W ω)) - S.h₀ (S.xOf (S.W ω))) ∂μ) + (∫ ω, S.h₀ (S.xOf (S.W ω)) * q (S.zOf (S.W ω)) ∂μ) - ∫ ω, q (S.zOf (S.W ω)) * h (S.xOf (S.W ω)) ∂μ := by rw [integral_add h_int_diff_q₀ h_int_h₀q] -- Step 5: combine. rw [hΘ_eq, hRHS_eq, ← h_me_diff_eq, ← h_prim] unfold InverseProblemSystem.θ₀ ring
Causalean.Estimation.NPIV.mixed_bias_identity · Causalean/Estimation/NPIV/MixedBias.lean:45 · uses InverseProblemSystem , DualSolution , X , Z , Θ , θ₀
2 supporting declarations (lemmas, instances)
  • Θ_h₀_eq_θ₀ theorem — DR cancellation at the truth on the primal side: Θ(h₀, q) = θ₀ for every q ∈ Qbar.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    shared
    S :
    InverseProblemSystem Ω μ
    q₀ :
    S.𝒵 → ℝ
    hq₀ :
    S.DualSolution q₀
    q :
    S.𝒵 → ℝ
    hq :
    q ∈ S.Qbar
    conclusion
    S.Θ 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
    Causalean.Estimation.NPIV.Θ_h₀_eq_θ₀ · Causalean/Estimation/NPIV/MixedBias.lean:174
  • Θ_q₀_eq_θ₀ theorem — DR cancellation at the truth on the dual side: Θ(h, q₀) = θ₀ for every h ∈ Hbar.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    shared
    S :
    InverseProblemSystem Ω μ
    q₀ :
    S.𝒵 → ℝ
    hq₀ :
    S.DualSolution q₀
    h :
    S.𝒳 → ℝ
    hh :
    h ∈ S.Hbar
    conclusion
    S.Θ 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
    Causalean.Estimation.NPIV.Θ_q₀_eq_θ₀ · Causalean/Estimation/NPIV/MixedBias.lean:186
Source­Condition 6 core · 4 supporting This file records the β-source condition for the primal NPIV nuisance and the Tikhonov bias bounds assumed by the primal rate theorem. ★ strong_bias

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.

structure SourceCondition reviewed
Causalean.Estimation.NPIV

The β-source condition represents the true primal nuisance as the image, under a positive 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)
parameters
Ω :
Type u_1
shared
μ :
Measure Ω
shared
S :
OperatorSystem Ω μ
β :
ℝ
fields
The source smoothness exponent is positive.
beta_pos :
0 < β
The pre-image of `h₀` under the spectral lift `(T*T)^{β/2}`.
w₀_fun :
S.𝒳 → ℝ
`w₀` lies in the primal candidate set `Hbar`.
w₀_mem :
w₀_fun ∈ S.Hbar
Spectral identity: `(h₀)_{L²} = (T†T)^{β/2} (w₀)_{L²}` inside the canonical trimmed realization of `L²(σ(X))`.
spectral_identity :
S.primalTrimEquiv (S.hL2 S.h₀_mem)
= @Complexification.realCFC Ω S.m_X (μ.trim S.m_X_le) S.Tstar_T_trim (fun x : ℝ => rpow (max x 0) (β/2)) (S.primalTrimEquiv (S.hL2 w₀_mem))
Causalean.Estimation.NPIV.SourceCondition · Causalean/Estimation/NPIV/SourceCondition.lean:57 · uses OperatorSystem
structure TikhonovBiasBound reviewed
Causalean.Estimation.NPIV

The uniform Tikhonov bias-bound bundle for an NPIV operator system, a source exponent, and its source condition records one nonnegative constant, population solutions at every positive regularization level, their strong- and weak-metric bias bounds, and their population strong-convexity inequality.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
μ :
Measure Ω
shared
S :
OperatorSystem Ω μ
β :
ℝ
sc :
SourceCondition S β
fields
The family of population Tikhonov solutions, indexed by the regularization level.
h_lambda_star_fun :
ℝ → S.𝒳 → ℝ
At every positive level, `h*_λ` lies in the primal candidate set `Hbar`.
h_lambda_star_mem :
∀ {lambda : ℝ}
if
0 < lambda
then
h_lambda_star_fun lambda ∈ S.Hbar
Constant absorbing the proof's `≲`.
C :
ℝ
The constant is non-negative.
C_nonneg :
0 ≤ C
Strong-metric Tikhonov bias bound: `‖h*_λ − h₀‖²_{L²(P_X)} ≤ C · ‖w₀‖_{L²(P_X)} · λ^{min(β, 2)}`.
strong_bias :
∀ {lambda : ℝ} (hlambda : 0 < lambda),
S.strongNorm (S.hL2 (h_lambda_star_mem hlambda) - S.hL2 S.h₀_mem) ^ 2
≤ C * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min β 2)
Weak-metric Tikhonov bias bound: `‖T(h*_λ − h₀)‖²_{L²(P_Z)} ≤ C · ‖w₀‖_{L²(P_X)} · λ^{min(β+1, 2)}`.
weak_bias :
∀ {lambda : ℝ} (hlambda : 0 < lambda),
S.weakNorm (S.hL2 (h_lambda_star_mem hlambda) - S.hL2 S.h₀_mem) ^ 2
≤ C * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min (β + 1) 2)
**Population strong convexity** at `h*_λ` (proof sketch lines 287–304 of `doc/basic_concepts/po/estimation/trae_inverse_problems.tex`). For any candidate `ĥ ∈ Hbar`, λ‖ĥ − h*_λ‖²_{L²(P_X)} + ‖T(ĥ − h*_λ)‖²_{L²(P_Z)} ≤ ‖T(ĥ − h₀)‖²_{L²(P_Z)} − ‖T(h*_λ − h₀)‖²_{L²(P_Z)} + λ(‖ĥ‖²_{L²(P_X)} − ‖h*_λ‖²_{L²(P_X)}). This field records the inequality as part of the certificate. The spectral-calculus discharge constructs the minimizer over the full primal `L²(σ(X))`, proves the ambient first-order identity, and requires a `TikhonovPullback` witness identifying that minimizer with an `Hbar` function. It does not prove minimization over an arbitrary closed candidate subspace.
strong_convexity :
∀ {lambda : ℝ} (hlambda : 0 < lambda) h,
∀ hh : h ∈ S.Hbar,
lambda * (S.strongNorm (S.hL2 hh - S.hL2 (h_lambda_star_mem hlambda))) ^ 2
+ (S.weakNorm (S.hL2 hh - S.hL2 (h_lambda_star_mem hlambda))) ^ 2
≤ (S.weakNorm (S.hL2 hh - S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm (S.hL2 (h_lambda_star_mem hlambda) - S.hL2 S.h₀_mem)) ^ 2
+ lambda * ((S.strongNorm (S.hL2 hh)) ^ 2 - (S.strongNorm (S.hL2 (h_lambda_star_mem hlambda))) ^ 2)
Causalean.Estimation.NPIV.TikhonovBiasBound · Causalean/Estimation/NPIV/SourceCondition.lean:93 · uses OperatorSystem , SourceCondition
structure TikhonovBiasBoundAt reviewed
Causalean.Estimation.NPIV

A fixed-level Tikhonov view packages an NPIV operator system, a source exponent, a selected regularization level, the corresponding source condition, a uniform bias certificate, and positivity of the selected level, without changing the certificate's uniform constant.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
μ :
Measure Ω
shared
S :
OperatorSystem Ω μ
β lambda :
ℝ
sc :
SourceCondition S β
fields
The uniform certificate from which this fixed-level view is obtained.
uniform :
TikhonovBiasBound S β sc
The selected regularization level is positive.
lambda_pos :
0 < lambda
Causalean.Estimation.NPIV.TikhonovBiasBoundAt · Causalean/Estimation/NPIV/SourceCondition.lean:155 · uses OperatorSystem , SourceCondition
abbrev h_lambda_star_fun reviewed
Causalean.Estimation.NPIV.TikhonovBiasBoundAt

The population Tikhonov solution in a fixed-level view.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
OperatorSystem Ω μ
shared
β :
ℝ
shared
lambda :
ℝ
shared
sc :
SourceCondition S β
shared
tb :
TikhonovBiasBoundAt S β lambda sc
def
h_lambda_star_fun tb :
S.𝒳 → ℝ
given by
tb.uniform.h_lambda_star_fun lambda
Causalean.Estimation.NPIV.TikhonovBiasBoundAt.h_lambda_star_fun · Causalean/Estimation/NPIV/SourceCondition.lean:170 · uses OperatorSystem , SourceCondition , TikhonovBiasBoundAt
abbrev C reviewed
Causalean.Estimation.NPIV.TikhonovBiasBoundAt

The level-independent bias constant in a fixed-level view.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
OperatorSystem Ω μ
shared
β :
ℝ
shared
lambda :
ℝ
shared
sc :
SourceCondition S β
shared
tb :
TikhonovBiasBoundAt S β lambda sc
def
C tb :
ℝ
given by
tb.uniform.C
Causalean.Estimation.NPIV.TikhonovBiasBoundAt.C · Causalean/Estimation/NPIV/SourceCondition.lean:180 · uses OperatorSystem , SourceCondition , TikhonovBiasBoundAt
lemma strong_bias reviewed
Causalean.Estimation.NPIV.TikhonovBiasBoundAt

A fixed-level view bounds its strong-metric Tikhonov bias.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
OperatorSystem Ω μ
shared
β :
ℝ
shared
lambda :
ℝ
shared
sc :
SourceCondition S β
shared
tb :
TikhonovBiasBoundAt S β lambda sc
conclusion
S.strongNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem) ^ 2
≤ tb.C * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min β 2)
Proof (Lean source)
lemma strong_bias (tb : TikhonovBiasBoundAt S β lambda sc) : S.strongNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem) ^ 2 ≤ tb.C * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min β 2) := tb.uniform.strong_bias tb.lambda_pos
Causalean.Estimation.NPIV.TikhonovBiasBoundAt.strong_bias · Causalean/Estimation/NPIV/SourceCondition.lean:187 · uses OperatorSystem , PrimalL2 , hL2 , strongNorm , SourceCondition , TikhonovBiasBoundAt , C , h_lambda_star_fun , h_lambda_star_mem
4 supporting declarations (lemmas, instances)
  • h_lambda_star_mem lemma — The fixed-level population solution from a bias certificate belongs to the admissible class.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    OperatorSystem Ω μ
    shared
    β :
    ℝ
    shared
    lambda :
    ℝ
    shared
    sc :
    SourceCondition S β
    shared
    tb :
    TikhonovBiasBoundAt S β lambda sc
    conclusion
    tb.h_lambda_star_fun ∈ S.Hbar
    Proof (Lean source)
    lemma h_lambda_star_mem (tb : TikhonovBiasBoundAt S β lambda sc) : tb.h_lambda_star_fun ∈ S.Hbar := tb.uniform.h_lambda_star_mem tb.lambda_pos
    Causalean.Estimation.NPIV.TikhonovBiasBoundAt.h_lambda_star_mem · Causalean/Estimation/NPIV/SourceCondition.lean:174
  • C_nonneg lemma — The level-independent constant in a fixed-level view is nonnegative.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    OperatorSystem Ω μ
    shared
    β :
    ℝ
    shared
    lambda :
    ℝ
    shared
    sc :
    SourceCondition S β
    shared
    tb :
    TikhonovBiasBoundAt S β lambda sc
    conclusion
    0 ≤ tb.C
    Proof (Lean source)
    lemma C_nonneg (tb : TikhonovBiasBoundAt S β lambda sc) : 0 ≤ tb.C := tb.uniform.C_nonneg
    Causalean.Estimation.NPIV.TikhonovBiasBoundAt.C_nonneg · Causalean/Estimation/NPIV/SourceCondition.lean:183
  • weak_bias lemma — A fixed-level view satisfies the weak-metric bias bound.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    OperatorSystem Ω μ
    shared
    β :
    ℝ
    shared
    lambda :
    ℝ
    shared
    sc :
    SourceCondition S β
    shared
    tb :
    TikhonovBiasBoundAt S β lambda sc
    conclusion
    S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem) ^ 2
    ≤ tb.C * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min (β + 1) 2)
    Proof (Lean source)
    lemma weak_bias (tb : TikhonovBiasBoundAt S β lambda sc) : S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem) ^ 2 ≤ tb.C * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min (β + 1) 2) := tb.uniform.weak_bias tb.lambda_pos
    Causalean.Estimation.NPIV.TikhonovBiasBoundAt.weak_bias · Causalean/Estimation/NPIV/SourceCondition.lean:193
  • strong_convexity lemma — A fixed-level view satisfies population strong convexity for every admissible candidate.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    OperatorSystem Ω μ
    shared
    β :
    ℝ
    shared
    lambda :
    ℝ
    shared
    sc :
    SourceCondition S β
    shared
    tb :
    TikhonovBiasBoundAt S β lambda sc
    h :
    S.𝒳 → ℝ
    hh :
    h ∈ S.Hbar
    conclusion
    lambda * (S.strongNorm (S.hL2 hh - S.hL2 tb.h_lambda_star_mem)) ^ 2
    + (S.weakNorm (S.hL2 hh - S.hL2 tb.h_lambda_star_mem)) ^ 2
    ≤ (S.weakNorm (S.hL2 hh - S.hL2 S.h₀_mem)) ^ 2
    - (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
    + lambda * ((S.strongNorm (S.hL2 hh)) ^ 2 - (S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2)
    Proof (Lean source)
    lemma strong_convexity (tb : TikhonovBiasBoundAt S β lambda sc) (h : S.𝒳 → ℝ) (hh : h ∈ S.Hbar) : lambda * (S.strongNorm (S.hL2 hh - S.hL2 tb.h_lambda_star_mem)) ^ 2 + (S.weakNorm (S.hL2 hh - S.hL2 tb.h_lambda_star_mem)) ^ 2 ≤ (S.weakNorm (S.hL2 hh - S.hL2 S.h₀_mem)) ^ 2 - (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2 + lambda * ((S.strongNorm (S.hL2 hh)) ^ 2 - (S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2) := tb.uniform.strong_convexity tb.lambda_pos h hh
    Causalean.Estimation.NPIV.TikhonovBiasBoundAt.strong_convexity · Causalean/Estimation/NPIV/SourceCondition.lean:199