Estimation.CATE

Estimation of conditional average treatment effects: the DR-Learner, its oracle expansions, linear-smoother specializations, and orthogonal-statistical-learning analyses.

Core 11 core · 7 supporting · 5 submodules Core DR-Learner pseudo-outcome theory for CATE: conditional bias, directional derivatives, conditional-mean identities, and second-order bias. Kennedy 8 core · 0 supporting · 3 submodules Kennedy-style DR-Learner theory: the doubly robust pseudo-outcome, its oracle expansion, and the linear-smoother error bound. Orthogonal­Learning 21 core · 5 supporting · 3 submodules DR-Learner orthogonal-learning system and oracle inequalities for CATE, including analytic derivatives, empirical-process moduli, and random-nuisance variants.
Setup 3 core · 1 supporting Defines the CATE estimation system as a function-valued version of the back-door ATE setup. ★ tau_val_eq_CATE

Defines the CATE estimation system as a function-valued version of the back-door ATE setup. It exposes the conditional treatment-effect target and the nuisance representatives needed by CATE pseudo-outcomes.

structure CATEEstimationSystem reviewed
Causalean.Estimation.CATE

Wrapper around BackdoorEstimationSystem whose semantic role is to expose the CATE target τ_val x = μ_val 1 x − μ_val 0 x as a derived function-valued estimand. No new fields are introduced; the underlying BackdoorEstimationSystem carries consistency, conditional exchangeability, overlap, integrability, the value-space μ_val / e_val, observable outcome-regression compatibility μ_reg_compat, and propensity compatibility e_compat. Counterfactual outcome-regression compatibility is derived later from the back-door causal assumptions, not inherited as a field.

Definition (Lean source)
parameters
P :
POSystem
γ :
Type*
MeasurableSpace γ
StandardBorelSpace P.Ω
IsFiniteMeasure P.μ
extends :
BackdoorEstimationSystem P γ
Causalean.Estimation.CATE.CATEEstimationSystem · Causalean/Estimation/CATE/Setup.lean:48 · uses POSystem
def τ_val reviewed
Causalean.Estimation.CATE.CATEEstimationSystem

Value-space CATE: τ_val x := μ_val 1 x − μ_val 0 x. This is the "observable CATE regression" τ_0 of def:est-cate-system.

Definition (Lean source)
def τ_val (S : CATEEstimationSystem P γ) (x : γ) : ℝ := S.μ_val true x - S.μ_val false x
Causalean.Estimation.CATE.CATEEstimationSystem.τ_val · Causalean/Estimation/CATE/Setup.lean:65 · uses CATEEstimationSystem , POSystem
theorem tau_val_eq_CATE reviewed
Causalean.Estimation.CATE.CATEEstimationSystem

Value-space CATE recovers the conditional average treatment effect. Under the back-door causal assumptions — consistency of observed and potential outcomes, treatment ignorability given the covariates, two-sided overlap, and integrability of both potential outcomes, the value-space CATE, evaluated at the observed covariate and viewed as a random variable on the sample space, agrees almost surely with the σ(X)-conditional expectation of the potential-outcome contrast Y(1) − Y(0). This is the last sentence of def:est-cate-causal-assumptions:

Formal statement
hypotheses
S :
CATEEstimationSystem P γ
hA :
S.toPOBackdoorSystem.Assumptions
conclusion
(fun ω => S.τ_val (S.toPOBackdoorSystem.factualX ω))
=ᵐ[P.μ] (P.μ[fun ω => S.toPOBackdoorSystem.YofD true ω - S.toPOBackdoorSystem.YofD false ω | S.toPOBackdoorSystem.sigmaX])
Proof (Lean source)
theorem tau_val_eq_CATE (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) : (fun ω => S.τ_val (S.toPOBackdoorSystem.factualX ω)) =ᵐ[P.μ] (P.μ[fun ω => S.toPOBackdoorSystem.YofD true ω - S.toPOBackdoorSystem.YofD false ω | S.toPOBackdoorSystem.sigmaX]) := by have hcompat : (fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) =ᵐ[P.μ] (fun ω => P.μ[S.toPOBackdoorSystem.YofD true | S.toPOBackdoorSystem.sigmaX] ω - P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX] ω) := (S.μ_compat hA true).symm.sub (S.μ_compat hA false).symm have hsub : P.μ[fun ω => S.toPOBackdoorSystem.YofD true ω - S.toPOBackdoorSystem.YofD false ω | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => P.μ[S.toPOBackdoorSystem.YofD true | S.toPOBackdoorSystem.sigmaX] ω - P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX] ω) := MeasureTheory.condExp_sub hA.integrable_Y1 hA.integrable_Y0 S.toPOBackdoorSystem.sigmaX calc (fun ω => S.τ_val (S.toPOBackdoorSystem.factualX ω)) =ᵐ[P.μ] (fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) := by filter_upwards with ω rfl _ =ᵐ[P.μ] (fun ω => P.μ[S.toPOBackdoorSystem.YofD true | S.toPOBackdoorSystem.sigmaX] ω - P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX] ω) := hcompat _ =ᵐ[P.μ] P.μ[fun ω => S.toPOBackdoorSystem.YofD true ω - S.toPOBackdoorSystem.YofD false ω | S.toPOBackdoorSystem.sigmaX] := hsub.symm
Causalean.Estimation.CATE.CATEEstimationSystem.tau_val_eq_CATE · Causalean/Estimation/CATE/Setup.lean:75 · uses CATEEstimationSystem , τ_val , Assumptions , YofD , factualX , sigmaX , POSystem
1 supporting declaration (lemmas, instances)