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

For a potential-outcomes system with a standard Borel sample space and finite probability measure, a measurable covariate space, a CATE estimation system, and a covariate value, the value-space conditional average treatment effect is the conditional mean outcome under treatment at that covariate value minus the conditional mean outcome under control at that covariate value.

Definition (Lean source)
parameters
P :
POSystem
shared
γ :
Type u_1
shared
S :
CATEEstimationSystem P γ
x :
γ
def
τ_val S x :
ℝ
given by
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
P :
POSystem
shared
γ :
Type u_1
shared
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:77 · uses CATEEstimationSystem , τ_val , Assumptions , YofD , factualX , sigmaX , POSystem
1 supporting declaration (lemmas, instances)