Estimation.CATE.Orthogonal­Learning

DR-Learner orthogonal-learning system and oracle inequalities for CATE, including analytic derivatives, empirical-process moduli, and random-nuisance variants.

DRLearner 9 core · 3 supporting · 1 submodule Builds the DR-Learner orthogonal-learning system for CATE estimation. Local­Emp­Process 11 core · 2 supporting · 6 submodules Empirical-process modulus results for the CATE DR-Learner: Rademacher, localized, honest-split, random-nuisance, and end-to-end oracle bounds.
Second­Order­Bias 1 core · 0 supporting This file shows that the nuisance-induced bias in the doubly robust learner for conditional treatment effects is bounded by the product of the outcome-regression error and the propensity-score error. ★ drBias_le_product

DR-Learner Second-Order Bias

This file shows that the nuisance-induced bias in the doubly robust learner for conditional treatment effects is bounded by the product of the outcome-regression error and the propensity-score error. The result makes the double-robust second-order remainder in the orthogonal statistical-learning oracle inequality explicit.

theorem drBias_le_product reviewed
Causalean.Estimation.OrthogonalLearning

DR-Learner second-order product bias bound. For a CATE estimation system built on a potential-outcome model that satisfies the back-door identification assumptions, with the true nuisance η₀ lying in the strict-overlap band at some margin ε > 0, fix a convex candidate target class in an inner-product space with a real-valued evaluation map, and suppose θ₀ belongs to this class, every candidate's evaluation is measurable, and θ₀'s evaluation agrees pointwise with the true value-space CATE. Fix a candidate nuisance h that also lies in the strict-overlap band at the same margin, a candidate target θ̂, and a nonnegative constant B bounding the evaluation-map directional derivative at θ̂. Assume the arm-wise outcome-regression fit of h, the AIPW pseudo-outcome discrepancy between h and the truth, and that discrepancy weighted by the directional derivative are all integrable, the outcome-regression error of h and the propensity error of h are square-integrable arm by arm, and the loss-gradient integrand at the true nuisance and the loss-gradient integrand at the candidate nuisance h are each integrable against the observation law. Then the loss-gradient nuisance bias Bias_n, evaluated between the true and candidate nuisance directional derivatives at θ̂, is bounded in absolute value by (2B/ε) times the sum over treatment arms of the outcome-regression L² error times the propensity L² error.

Formal statement
hypotheses
S :
CATEEstimationSystem P γ
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
hε_pos :
0 < ε
h_overlap_η₀ :
S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
Θ :
Type*
NormedAddCommGroup Θ
InnerProductSpace ℝ Θ
Θ_set :
Set Θ
Θ_convex :
Convex ℝ Θ_set
θ₀ :
Θ
θ₀_mem :
θ₀ ∈ Θ_set
eval :
Θ → γ → ℝ
eval_meas :
∀ θ, Measurable (eval θ)
eval_θ₀ :
∀ x, eval θ₀ x = S.τ_val x
θ₀_minimizes :
DRThetaMinimizes S Θ_set θ₀ eval
D :
EvalDirDeriv Θ_set θ₀ eval
ND :
NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀
h :
NuisanceVec γ
h_overlap_h :
h ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
θhat :
Θ
B :
ℝ
hB_nonneg :
0 ≤ B
hdEval_bound :
∀ x, |D.dEval θhat x| ≤ B
h_μ_h_int :
∀ a : Bool, Integrable (fun ω => h.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ
h_phi_int :
Integrable (fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) h - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ
h_phiw_int :
Integrable (fun ω => (phi_eta (S.toBackdoorEstimationSystem.factualZ ω) h - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) * D.dEval θhat (S.toBackdoorEstimationSystem.factualX ω)) P.μ
hΔμ_memLp :
∀ a, MemLp (fun x => h.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X
hΔe_memLp :
MemLp (fun x => h.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X
hA_int :
Integrable (fun z => ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀).dℓ_θ θhat z) S.toBackdoorEstimationSystem.P_Z
hB_int :
Integrable (fun z => ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at h).dℓ_θ θhat z) S.toBackdoorEstimationSystem.P_Z
conclusion
|Bias_n (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀) ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at h) θhat|
≤ (2 * B / ε) * ∑ a : Bool, (eLpNorm (fun x => h.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X).toReal * (eLpNorm (fun x => h.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X).toReal
Proof (Lean source)
theorem drBias_le_product (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) {ε : ℝ} (hε_pos : 0 < ε) (h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (Θ : Type*) [NormedAddCommGroup Θ] [InnerProductSpace ℝ Θ] (Θ_set : Set Θ) (Θ_convex : Convex ℝ Θ_set) (θ₀ : Θ) (θ₀_mem : θ₀ ∈ Θ_set) (eval : Θ → γ → ℝ) (eval_meas : ∀ θ, Measurable (eval θ)) (eval_θ₀ : ∀ x, eval θ₀ x = S.τ_val x) (θ₀_minimizes : DRThetaMinimizes S Θ_set θ₀ eval) (D : EvalDirDeriv Θ_set θ₀ eval) (ND : NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀) (h : NuisanceVec γ) (h_overlap_h : h ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (θhat : Θ) {B : ℝ} (hB_nonneg : 0 ≤ B) (hdEval_bound : ∀ x, |D.dEval θhat x| ≤ B) (h_μ_h_int : ∀ a : Bool, Integrable (fun ω => h.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ) (h_phi_int : Integrable (fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) h - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ) (h_phiw_int : Integrable (fun ω => (phi_eta (S.toBackdoorEstimationSystem.factualZ ω) h - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) * D.dEval θhat (S.toBackdoorEstimationSystem.factualX ω)) P.μ) (hΔμ_memLp : ∀ a, MemLp (fun x => h.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X) (hΔe_memLp : MemLp (fun x => h.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X) (hA_int : Integrable (fun z => ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀).dℓ_θ θhat z) S.toBackdoorEstimationSystem.P_Z) (hB_int : Integrable (fun z => ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at h).dℓ_θ θhat z) S.toBackdoorEstimationSystem.P_Z) : |Bias_n (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀) ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at h) θhat| ≤ (2 * B / ε) * ∑ a : Bool, (eLpNorm (fun x => h.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X).toReal * (eLpNorm (fun x => h.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X).toReal := by -- Closed forms of the two directional-derivative integrands (literal fields). have hAclosed : ∀ z, ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀).dℓ_θ θhat z = -2 * (phi_eta z S.toBackdoorEstimationSystem.η₀ - eval θ₀ z.1) * D.dEval θhat z.1 := fun _ => rfl have hBclosed : ∀ z, ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at h).dℓ_θ θhat z = -2 * (phi_eta z h - eval θ₀ z.1) * D.dEval θhat z.1 := fun _ => rfl -- Bias_n telescopes (the `eval θ₀` term cancels) to `2 ∫ (phi_eta·h − phi₀)·dEval`. have hBias_eq : Bias_n (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀) ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at h) θhat = 2 * ∫ z, (phi_eta z h - phi₀ S z) * D.dEval θhat z.1 ∂S.toBackdoorEstimationSystem.P_Z := by unfold Bias_n rw [← integral_sub hA_int hB_int, ← integral_const_mul] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall fun z => ?_) simp only [hAclosed z, hBclosed z, phi₀] ring rw [hBias_eq, abs_mul, show |(2 : ℝ)| = 2 from by norm_num] calc 2 * |∫ z, (phi_eta z h - phi₀ S z) * D.dEval θhat z.1 ∂S.toBackdoorEstimationSystem.P_Z| ≤ 2 * ((B / ε) * ∑ a : Bool, (eLpNorm (fun x => h.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X).toReal * (eLpNorm (fun x => h.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X).toReal) := by refine mul_le_mul_of_nonneg_left ?_ (by norm_num) exact abs_integral_phiDiff_mul_le_product S hε_pos hA h h_overlap_h h_overlap_η₀ h_μ_h_int (D.dEval θhat) (D.meas θhat) hB_nonneg hdEval_bound h_phi_int h_phiw_int hΔμ_memLp hΔe_memLp _ = (2 * B / ε) * ∑ a : Bool, (eLpNorm (fun x => h.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X).toReal * (eLpNorm (fun x => h.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X).toReal := by ring
Causalean.Estimation.OrthogonalLearning.drBias_le_product · Causalean/Estimation/CATE/OrthogonalLearning/SecondOrderBias.lean:56 · uses H_ε , P_X , P_Z , factualZ , η₀ , NuisanceVec , instAddCommGroup , instModuleReal , CATEEstimationSystem , τ_val , phi_eta , phi₀ , Bias_n , DRThetaMinimizes , EvalDirDeriv , NuisanceDirDeriv , drLearningSystem , drMixedDirDeriv , Assumptions , factualX , POSystem