PO.ID.Exact
Exact (point) identification: back-door and front-door adjustment, IV/LATE, regression discontinuity, proximal inference, dynamic regimes, and related theorems.
DTR 26 core · 26 supporting · 5 submodules Identification for dynamic treatment regimes: sequential exchangeability and the g-formula. DynamicLATE 60 core · 42 supporting · 4 submodules Dynamic LATE: identification of complier effects in multi-period instrumented settings. HeckmanRoy 24 core · 16 supporting · 2 submodules The Heckman/Roy selection model: identification of treatment parameters under self-selection. MultipleInstrumentIV 78 core · 41 supporting · 5 submodules Multiple-instrument IV: Mogstad-Torgovitsky-Walters finite-support 2SLS response-type algebra and sign-alignment results. PartialLinear 17 core · 15 supporting · 2 submodules Partially linear continuous-treatment identification: the potential-outcome setup, homogeneous dose-response restriction, Robinson residualization, and slope-identification theorem. Proximal 22 core · 24 supporting · 4 submodules Proximal causal inference: identification through outcome- and treatment-confounding proxies via bridge functions. QTE 9 core · 7 supporting · 2 submodules Quantile treatment effects (Firpo 2007): backdoor identification of the marginal QTE at level τ — the τ-quantile of the treated potential outcome Y(1) minus that of the control Y(0). DistributionalBackdoor lifts the mean-level backdoor to the whole potential-outcome law via inverse-probability weighting; QuantileEffect adds the quantile layer, identifying the QTE as the difference of the identified laws quantiles. RDD 31 core · 29 supporting · 3 submodules Regression discontinuity: identification of the cutoff effect from continuity of conditional regressions. VariableIntensityIV 49 core · 21 supporting · 2 submodules Variable-intensity instrumental variables: Angrist-Imbens average causal response over ordered treatment margins.
ATE 25 core · 20 supporting This file proves backdoor identification for the average treatment effect in the potential-outcome framework. ★ POBackdoorSystem★ cate_backdoor★ ate_backdoor★ regression_adjustment
Backdoor Average Treatment Effect
This file proves backdoor identification for the average treatment effect in the potential-outcome framework. It connects conditional independence, consistency, and overlap assumptions to the standard adjustment formula for binary treatment and real-valued outcomes.
The adjustment covariate has an arbitrary measurable value space, so the same setup covers discrete, continuous, and vector-valued covariates. The proof uses conditional expectations with respect to the sigma-algebra generated by the covariate.
The main public results are cate_backdoor_of_propScore_ne, which isolates the
per-arm propensity nonvanishing condition, cate_backdoor and ate_backdoor,
which discharge it from two-sided overlap, and regression_adjustment, which
shows the adjusted conditional functional is the observable regression
E[Y | D=d, X].
structure POBackdoorSystem reviewed
⚑ flagged
Causalean.PO
A backdoor system consists of a binary treatment variable, a real-valued outcome variable, and an adjustment covariate with an arbitrary measurable value space, where the three variables are pairwise distinct.
Definition (Lean source)
parameters
P :
γ :
Type*
def dVar reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The treatment node is packaged as a binary potential-outcome variable.
def yVar reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The outcome node is packaged as a real-valued potential-outcome variable.
Definition (Lean source)
def yVar : POVar P ℝ := ⟨S.Y, S.hYreal⟩
def xVar reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The adjustment covariate is the specified potential-outcome variable.
Definition (Lean source)
def xVar : POVar P γ := S.Xvar
def YofD reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The potential outcome under a fixed treatment arm is a real-valued function on units.
Definition (Lean source)
noncomputable def YofD (d : Bool) : P.Ω → ℝ := S.yVar.cfUnder S.dVar d
def factualD reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The factual treatment is the observed treatment assignment for each unit.
Definition (Lean source)
noncomputable def factualD : P.Ω → Bool := S.dVar.factual
def factualY reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The factual outcome is the observed outcome for each unit.
Definition (Lean source)
noncomputable def factualY : P.Ω → ℝ := S.yVar.factual
def factualX reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The factual covariate is the observed adjustment covariate for each unit.
Definition (Lean source)
noncomputable def factualX : P.Ω → γ := S.xVar.factual
def sigmaX reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The covariate sigma-algebra is generated by the observed covariate.
Definition (Lean source)
def yUnderD reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The regimed form of the potential outcome fixes treatment to the chosen arm.
Definition (Lean source)
def yUnderD (d : Bool) : RegimedVar P ℝ :=
⟨S.yVar, Regime.single S.D (S.hDbool.symm d)⟩
def cfBundle reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The counterfactual bundle collects the treated and untreated potential outcomes for unconfoundedness.
Definition (Lean source)
noncomputable def cfBundle : POCFBundle P :=
POCFBundle.cons (S.yUnderD true) <|
POCFBundle.cons (S.yUnderD false) <|
POCFBundle.nil P
def propScore reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The propensity score is the conditional probability of a treatment arm given the covariate.
def CATE reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The conditional mean potential outcome is the mean of a treatment-arm potential outcome given the covariate.
def ATE reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The ATE is the population mean difference between treated and untreated potential outcomes.
def adjustedCE reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The adjusted conditional functional is the observable outcome-indicator regression divided by the propensity score.
Definition (Lean source)
noncomputable def adjustedCE (d : Bool) : P.Ω → ℝ :=
fun ω => P.μ[fun ω' => S.factualY ω' * S.dVar.indicator d ω' | S.sigmaX] ω / S.propScore d ω
def adjustedATE reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The adjusted ATE integrates the difference of the two adjusted conditional outcome functionals.
structure Assumptions reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The backdoor (Rosenbaum–Rubin / Firpo) identifying assumptions for the ATE, at the potential-outcome level, for binary treatment D and real outcome Y adjusted for covariates X: the observed outcome equals the potential outcome of the realized treatment arm, treatment is conditionally independent of the treated and untreated potential outcomes given the covariates, every covariate stratum has a positive chance of either treatment arm, and the treated and untreated potential outcomes are integrable.
Definition (Lean source)
parameters
fields
Consistency (SUTVA): the observed outcome equals the potential outcome of
the realized arm — on `{D = d}`, `Y = Y(d)`. Links observed data to the
potential outcomes.
consistency :
P.Consistency
Unconfoundedness (conditional ignorability): treatment is independent of the
potential outcomes given the covariates, `D ⟂ (Y(1), Y(0)) | X`. Stated as
conditional independence of the realized `D` and the counterfactual bundle
`(Y(1), Y(0))` given `σ(X)`.
unconfoundedness :
P.CondIndepCF (RegimedVar.ofFactual S.dVar) S.cfBundle (RegimedVar.ofFactual S.xVar) P.μ
Overlap (common support): every covariate stratum has a positive chance of
EITHER arm — `0 < P[D=1 | σ(X)] < 1` a.s. Two-sided here because the ATE needs
both arms identified at every `x`. Bare positivity (not a uniform `c ≤ e ≤ 1−c`
strong-overlap bound, which is only needed for efficient-estimator asymptotics),
mirroring DTR.
Regularity: the treated potential outcome `Y(1)` is integrable (so `E[Y(1)]`
is well-defined).
integrable_Y1 :
Integrable (S.YofD true) P.μ
Regularity: the control potential outcome `Y(0)` is integrable (so `E[Y(0)]`
is well-defined).
integrable_Y0 :
Integrable (S.YofD false) P.μ
theorem cate_backdoor reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
CATE-level backdoor identification. Under the backdoor identification assumptions — consistency, unconfoundedness, and two-sided overlap of the propensity score, together with integrability of the potential outcomes, for a treatment arm d, the conditional average treatment effect given the covariates equals the adjusted-outcome functional:
Formal statement
hypotheses
conclusion
S.CATE d =ᵐ[P.μ] S.adjustedCE d
Proof (Lean source)
theorem cate_backdoor [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(hA : S.Assumptions) (d : Bool) :
S.CATE d =ᵐ[P.μ] S.adjustedCE d :=
S.cate_backdoor_of_propScore_ne hA.consistency hA.unconfoundedness
hA.integrable_Y1 hA.integrable_Y0 d (S.propScore_ne_of_overlap hA.overlap d)
theorem ate_backdoor reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Integrated backdoor ATE identification. Under the backdoor identification assumptions — consistency, unconfoundedness, two-sided overlap, and integrable potential outcomes, the average treatment effect equals the adjusted-outcome functional obtained by averaging the CATE-level backdoor identity over the covariate distribution.
Formal statement
hypotheses
conclusion
S.ATE = S.adjustedATE
Proof (Lean source)
theorem ate_backdoor [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(hA : S.Assumptions) : S.ATE = S.adjustedATE := by
unfold POBackdoorSystem.ATE POBackdoorSystem.adjustedATE
-- `CATE d = xVar.condExpGiven (YofD d) P.μ` definitionally.
have hf' : S.xVar.condExpGiven (S.YofD true) P.μ =ᵐ[P.μ] S.adjustedCE true :=
S.cate_backdoor hA true
have hg' : S.xVar.condExpGiven (S.YofD false) P.μ =ᵐ[P.μ] S.adjustedCE false :=
S.cate_backdoor hA false
exact S.xVar.integral_sub_eq_integral_sub_of_condExpGiven_ae_eq
hA.integrable_Y1 hA.integrable_Y0 hf' hg'
def factualDX reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Factual (D, X) pair ω ↦ (factualD ω, factualX ω) : Ω → Bool × γ. The covariate–treatment cell each unit lands in.
Definition (Lean source)
noncomputable def factualDX : P.Ω → Bool × γ :=
fun ω => (S.factualD ω, S.factualX ω)
def sigmaDX reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
σ-algebra generated by the factual (D, X). Contains σ(X) (snd projection) and is the information a regression of Y on (D, X) may use.
Definition (Lean source)
def outcomeReg reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Outcome regression E[Y | D, X] := μ[factualY | σ(D, X)], the conditional mean of the observed outcome given the observed treatment and covariate. A functional of the observed data law, learnable by regressing Y on (D, X).
Definition (Lean source)
noncomputable def outcomeReg : P.Ω → ℝ :=
P.μ[S.factualY | S.sigmaDX]
def regFn reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Value-space outcome regression regFn (d, x) = E[Y | D=d, X=x].
Definition (Lean source)
noncomputable def regFn : Bool × γ → ℝ := S.exists_regFn.choose
def eLift reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Value-space propensity eLift x (a measurable representative of E[D | X=x]).
Definition (Lean source)
noncomputable def eLift : γ → ℝ := S.exists_propScoreLift.choose
theorem regression_adjustment reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Regression-adjustment identification (observable). For a treatment arm d, if the observed outcome is integrable and the covariate- conditional probability of receiving arm d is almost surely nonzero, then the backdoor adjustment functional for arm d equals the value-space outcome regression evaluated at the arm d:
Formal statement
hypotheses
conclusion
S.adjustedCE d =ᵐ[P.μ] (fun ω => S.regFn (d, S.factualX ω))
Proof (Lean source)
theorem regression_adjustment [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(d : Bool) (hY : Integrable S.factualY P.μ)
(h_ne : ∀ᵐ ω ∂P.μ, S.propScore d ω ≠ 0) :
S.adjustedCE d =ᵐ[P.μ] (fun ω => S.regFn (d, S.factualX ω)) := by
have hratio_def :
S.adjustedCE d
= S.xVar.condExpRatio
(fun ω => S.factualY ω * S.dVar.indicator d ω)
(S.dVar.indicator d) P.μ := by
funext ω
unfold POBackdoorSystem.adjustedCE POBackdoorSystem.propScore
POBackdoorSystem.sigmaX POBackdoorSystem.factualX POVar.condExpRatio
POVar.condExpGiven
rfl
rw [hratio_def]
refine S.xVar.condExpRatio_eq_of_mul
(g := fun ω => S.factualY ω * S.dVar.indicator d ω)
(h := S.dVar.indicator d)
(target := fun ω => S.regFn (d, S.factualX ω)) ?_ ?_
· have hYint : Integrable S.factualY P.μ := hY
· let s : Set P.Ω := S.dVar.event d
let target : P.Ω → ℝ := fun ω => S.regFn (d, S.factualX ω)
have hsDX : MeasurableSet[S.sigmaDX] s := by
change MeasurableSet[comap S.factualDX inferInstance]
(S.factualD ⁻¹' {d})
exact ⟨Prod.fst ⁻¹' {d}, measurableSet_singleton d |>.preimage measurable_fst, rfl⟩
have hs : MeasurableSet s :=
S.dVar.measurableSet_event d (measurableSet_singleton d)
have hmul_indicator :
(fun ω => S.factualY ω * S.dVar.indicator d ω) = s.indicator S.factualY := by
funext ω
by_cases hω : ω ∈ s
· have hind : S.dVar.indicator d ω = 1 := S.dVar.indicator_apply_eq_one hω
rw [hind, mul_one, Set.indicator_of_mem hω]
· have hD : S.factualD ω ≠ d := hω
have hind : S.dVar.indicator d ω = 0 := S.dVar.indicator_apply_eq_zero hD
rw [hind, mul_zero, Set.indicator_of_notMem hω]
have htarget_meas : Measurable[S.sigmaX] target := by
have hreg_d : Measurable (fun x : γ => S.regFn (d, x)) :=
S.measurable_regFn.comp (measurable_const.prodMk measurable_id)
change Measurable[comap S.factualX inferInstance]
((fun x : γ => S.regFn (d, x)) ∘ S.factualX)
exact hreg_d.comp (comap_measurable S.factualX)
have htarget_sm : StronglyMeasurable[S.sigmaX] target :=
htarget_meas.stronglyMeasurable
have houtcome_target :
s.indicator S.outcomeReg = s.indicator target := by
funext ω
by_cases hω : ω ∈ s
· have hD : S.factualD ω = d := hω
rw [Set.indicator_of_mem hω, Set.indicator_of_mem hω]
rw [congrFun S.outcomeReg_eq_regFn ω]
simp [target, POBackdoorSystem.factualDX, hD]
· rw [Set.indicator_of_notMem hω, Set.indicator_of_notMem hω]
have htower :
P.μ[s.indicator S.factualY | S.sigmaX]
=ᵐ[P.μ] P.μ[s.indicator S.outcomeReg | S.sigmaX] := by
simpa [s, POBackdoorSystem.outcomeReg] using
condExp_setIndicator_condExp_of_le
(μ := P.μ) (m := S.sigmaX) (m' := S.sigmaDX)
S.sigmaX_le_sigmaDX S.sigmaDX_le hsDX hYint
have hleft :
P.μ[fun ω => S.factualY ω * S.dVar.indicator d ω | S.sigmaX]
=ᵐ[P.μ] P.μ[s.indicator target | S.sigmaX] :=
(MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := P.μ)
(Filter.EventuallyEq.of_eq hmul_indicator)).trans
(htower.trans
(MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := P.μ)
(Filter.EventuallyEq.of_eq houtcome_target)))
have hind_int : Integrable (S.dVar.indicator d) P.μ :=
S.dVar.integrable_indicator d (measurableSet_singleton d)
have htarget_mul_indicator :
target * S.dVar.indicator d = s.indicator target := by
funext ω
by_cases hω : ω ∈ s
· have hind : S.dVar.indicator d ω = 1 := S.dVar.indicator_apply_eq_one hω
rw [Pi.mul_apply, hind, mul_one, Set.indicator_of_mem hω]
· have hD : S.factualD ω ≠ d := hω
have hind : S.dVar.indicator d ω = 0 := S.dVar.indicator_apply_eq_zero hD
rw [Pi.mul_apply, hind, mul_zero, Set.indicator_of_notMem hω]
have htarget_mul_int : Integrable (target * S.dVar.indicator d) P.μ := by
rw [htarget_mul_indicator]
have houtcome_target' :
s.indicator (P.μ[S.factualY | S.sigmaDX]) = s.indicator target := by
simpa [POBackdoorSystem.outcomeReg] using houtcome_target
exact MeasureTheory.Integrable.indicator
(MeasureTheory.integrable_condExp (μ := P.μ) (m := S.sigmaDX) (f := S.factualY)) hs
|>.congr (Filter.EventuallyEq.of_eq houtcome_target')
have hpull :
P.μ[target * S.dVar.indicator d | S.sigmaX]
=ᵐ[P.μ] target * P.μ[S.dVar.indicator d | S.sigmaX] :=
MeasureTheory.condExp_mul_of_stronglyMeasurable_left
(m := S.sigmaX) (μ := P.μ) htarget_sm htarget_mul_int hind_int
change P.μ[fun ω => S.factualY ω * S.dVar.indicator d ω | S.sigmaX]
=ᵐ[P.μ] P.μ[S.dVar.indicator d | S.sigmaX] * target
refine hleft.trans ?_
refine (MeasureTheory.condExp_congr_ae (m := S.sigmaX) (μ := P.μ)
(Filter.EventuallyEq.of_eq htarget_mul_indicator.symm)).trans ?_
exact hpull.trans (Filter.EventuallyEq.of_eq (by
funext ω
exact mul_comm _ _))
· have hEq : S.xVar.condExpGiven (S.dVar.indicator d) P.μ = S.propScore d := by
unfold POVar.condExpGiven POBackdoorSystem.propScore
POBackdoorSystem.sigmaX POBackdoorSystem.factualX
rfl
rw [hEq]
exact h_ne
20 supporting declarations (lemmas, instances)
-
measurable_YofDlemma — Potential outcomes under fixed treatment arms are measurable.Proof (Lean source)
lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_factualDlemma — The observed treatment is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_factualXlemma — The observed covariate is measurable.conclusionMeasurable S.factualXProof (Lean source)
lemma measurable_factualX : Measurable S.factualX := S.xVar.measurable_factual -
sigmaX_lelemma — The covariate sigma-algebra is a sub-sigma-algebra of the ambient one.conclusionS.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaX_le : S.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualX.comap_le -
integrable_factualY_of_consistencylemma — Factual Y is integrable whenever both treatment-arm potential outcomes are integrable and consistency links the observed outcome to the realized arm.hypothesesconclusionIntegrable S.factualY P.μProof (Lean source)
lemma integrable_factualY_of_consistency (hcons : P.Consistency) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) : Integrable S.factualY P.μ := by have hY1_ind : Integrable (fun ω => S.YofD true ω * S.dVar.indicator true ω) P.μ := S.dVar.integrable_mul_indicator true (measurableSet_singleton true) hY1 have hY0_ind : Integrable (fun ω => S.YofD false ω * S.dVar.indicator false ω) P.μ := S.dVar.integrable_mul_indicator false (measurableSet_singleton false) hY0 have hsum_int : Integrable (fun ω => S.YofD true ω * S.dVar.indicator true ω + S.YofD false ω * S.dVar.indicator false ω) P.μ := hY1_ind.add hY0_ind refine hsum_int.congr ?_ filter_upwards with ω have htrue := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hcons S.yVar S.dVar true (Ne.symm S.hDY)) ω have hfalse := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hcons S.yVar S.dVar false (Ne.symm S.hDY)) ω have htrue' : S.YofD true ω * S.dVar.indicator true ω = S.factualY ω * S.dVar.indicator true ω := by simpa [POBackdoorSystem.YofD, POBackdoorSystem.factualY] using htrue.symm have hfalse' : S.YofD false ω * S.dVar.indicator false ω = S.factualY ω * S.dVar.indicator false ω := by simpa [POBackdoorSystem.YofD, POBackdoorSystem.factualY] using hfalse.symm have hsum := S.dVar.indicator_add_indicator_not ω calc S.YofD true ω * S.dVar.indicator true ω + S.YofD false ω * S.dVar.indicator false ω = S.factualY ω * S.dVar.indicator true ω + S.factualY ω * S.dVar.indicator false ω := by rw [htrue', hfalse'] _ = S.factualY ω * (S.dVar.indicator true ω + S.dVar.indicator false ω) := by ring _ = S.factualY ω := by rw [hsum, mul_one] -
integrable_factualYlemma — The observed outcome is integrable under the backdoor assumption bundle.hypothesesconclusionIntegrable S.factualY P.μProof (Lean source)
lemma Assumptions.integrable_factualY [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.Assumptions) : Integrable S.factualY P.μ := S.integrable_factualY_of_consistency hA.consistency hA.integrable_Y1 hA.integrable_Y0 -
propScore_ne_of_overlaplemma — From two-sided overlap, the per-arm propensity score P[D=d | σ(X)] is a.s. nonzero: for d = true directly from 0 < e(X), for d = false from e(X) < 1 via propScore false = 1 - e(X).Proof (Lean source)
lemma propScore_ne_of_overlap [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hov : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1) (d : Bool) : ∀ᵐ ω ∂P.μ, S.propScore d ω ≠ 0 := by cases d · -- false: propScore false = 1 - propScore true, and propScore true < 1. have hindD_integrable : ∀ e : Bool, Integrable (S.dVar.indicator e) P.μ := fun e => S.dVar.integrable_indicator e (measurableSet_singleton e) have hsum_ptwise : (fun ω => S.dVar.indicator true ω + S.dVar.indicator false ω) = (fun _ : P.Ω => (1 : ℝ)) := by funext ω exact S.dVar.indicator_add_indicator_not ω have hsum : P.μ[fun ω => S.dVar.indicator true ω + S.dVar.indicator false ω | S.sigmaX] =ᵐ[P.μ] (fun _ => (1 : ℝ)) := by rw [hsum_ptwise] exact Filter.EventuallyEq.of_eq (MeasureTheory.condExp_const S.sigmaX_le (1 : ℝ)) have hadd : P.μ[fun ω => S.dVar.indicator true ω + S.dVar.indicator false ω | S.sigmaX] =ᵐ[P.μ] P.μ[S.dVar.indicator true | S.sigmaX] + P.μ[S.dVar.indicator false | S.sigmaX] := MeasureTheory.condExp_add (hindD_integrable true) (hindD_integrable false) S.sigmaX filter_upwards [hsum, hadd, hov] with ω h1 h2 hT have heq : S.propScore true ω + S.propScore false ω = 1 := by have : P.μ[S.dVar.indicator true | S.sigmaX] ω + P.μ[S.dVar.indicator false | S.sigmaX] ω = 1 := by rw [← Pi.add_apply, ← h2, h1] unfold POBackdoorSystem.propScore exact this have hps_false : S.propScore false ω = 1 - S.propScore true ω := by linarith rw [hps_false] intro h linarith [hT.2] · filter_upwards [hov] with ω hω exact ne_of_gt hω.1 -
cate_backdoor_of_propScore_netheorem — CATE-level backdoor identification (per-arm overlap form). The conditional ATE equals the adjusted-outcome functional under consistency, unconfoundedness, arm-wise outcome integrability, and the single one-sided requirement that the d-arm propensity score is a.s. nonzero (P[D=d | σ(X)] ≠ 0):hypothesesIsFiniteMeasure P.μhcons :P.Consistencyhunconf :P.CondIndepCF (RegimedVar.ofFactual S.dVar) S.cfBundle (RegimedVar.ofFactual S.xVar) P.μhY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μd :h_ne :∀ᵐ ω ∂P.μ, S.propScore d ω ≠ 0conclusionS.CATE d =ᵐ[P.μ] S.adjustedCE dProof (Lean source)
theorem cate_backdoor_of_propScore_ne [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hcons : P.Consistency) (hunconf : P.CondIndepCF (RegimedVar.ofFactual S.dVar) S.cfBundle (RegimedVar.ofFactual S.xVar) P.μ) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) (d : Bool) (h_ne : ∀ᵐ ω ∂P.μ, S.propScore d ω ≠ 0) : S.CATE d =ᵐ[P.μ] S.adjustedCE d := by -- Rewrite `adjustedCE d = condExpRatio S.xVar (factualY * indD d) (indD d) P.μ`. have hratio_def : S.adjustedCE d = S.xVar.condExpRatio (fun ω => S.factualY ω * S.dVar.indicator d ω) (S.dVar.indicator d) P.μ := by funext ω unfold POBackdoorSystem.adjustedCE POBackdoorSystem.propScore POBackdoorSystem.sigmaX POBackdoorSystem.factualX POVar.condExpRatio POVar.condExpGiven rfl rw [hratio_def] -- Apply `condExpRatio_eq_of_mul` to reduce to (hprod) and (hne). refine (S.xVar.condExpRatio_eq_of_mul (g := fun ω => S.factualY ω * S.dVar.indicator d ω) (h := S.dVar.indicator d) (target := S.CATE d) ?_ ?_).symm · -- (hprod): μ[Y·1_{D=d}|σX] =ᵐ μ[1_{D=d}|σX] · CATE d. -- Integrability prerequisites. have hindD_integrable : Integrable (S.dVar.indicator d) P.μ := S.dVar.integrable_indicator d (measurableSet_singleton d) have hYofD_integrable : Integrable (S.YofD d) P.μ := by cases d · exact hY0 · exact hY1 have hYofD_bdd_integrable_aux : Integrable (fun ω => S.YofD d ω * S.dVar.indicator d ω) P.μ := by exact S.dVar.integrable_mul_indicator d (measurableSet_singleton d) hYofD_integrable have hYtimesInd_integrable : Integrable (fun ω => S.factualY ω * S.dVar.indicator d ω) P.μ := by exact S.dVar.integrable_mul_indicator d (measurableSet_singleton d) (S.integrable_factualY_of_consistency hcons hY1 hY0) -- Step 1: μ[Y·1_{D=d}|σX] =ᵐ μ[Y(d)·1_{D=d}|σX]. have hstep1 : S.xVar.condExpGiven (fun ω => S.factualY ω * S.dVar.indicator d ω) P.μ =ᵐ[P.μ] S.xVar.condExpGiven (fun ω => S.YofD d ω * S.dVar.indicator d ω) P.μ := by have hvw : S.yVar.v ≠ S.dVar.v := Ne.symm S.hDY have hfm := POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hcons S.yVar S.dVar d hvw -- `S.factualY = S.yVar.factual` and `S.YofD d = S.yVar.cfUnder S.dVar d` by def. change S.xVar.condExpGiven (fun ω => S.yVar.factual ω * S.dVar.indicator d ω) P.μ =ᵐ[P.μ] S.xVar.condExpGiven (fun ω => S.yVar.cfUnder S.dVar d ω * S.dVar.indicator d ω) P.μ rw [hfm] refine hstep1.trans ?_ -- Project unconfoundedness onto the `d`-th coordinate of the bundle. -- The bundle has two components: index 0 = YofD true, index 1 = YofD false. let ψ : (∀ i : Fin S.cfBundle.n, S.cfBundle.type i) → ℝ := fun f => match d with | true => f (0 : Fin 2) | false => f (1 : Fin 2) have hψ_meas : Measurable ψ := by let instCf : ∀ a : Fin 2, MeasurableSpace (S.cfBundle.type a) := fun a => S.cfBundle.inst a cases d with | true => exact measurable_pi_apply (0 : Fin 2) | false => exact measurable_pi_apply (1 : Fin 2) have hYofD_eq : S.YofD d = ψ ∘ S.cfBundle.jointValue := by funext ω; cases d <;> rfl have hCI : CondIndepFun S.sigmaX S.sigmaX_le S.factualD (S.YofD d) P.μ := by have hproj := hunconf.project (ψ := ψ) hψ_meas rw [hYofD_eq]; exact hproj -- Apply factorization with u := indD d (as a function of factualD) and v := YofD d. -- Use the plain pointwise product: indD d ω * YofD d ω. have hindMul_swap : (fun ω => S.YofD d ω * S.dVar.indicator d ω) = (fun ω => S.dVar.indicator d ω * S.YofD d ω) := by funext ω; exact mul_comm _ _ rw [hindMul_swap] -- Apply via an auxiliary lemma that takes the (u, v) shapes matching our data. -- Use `condExp_mul_of_condIndep` with: -- f = factualD, g = YofD d, u = (fun b => if b = d then 1 else 0), v = id. -- `u (factualD ω) = indD d ω` and `id (YofD d ω) = YofD d ω` by rfl. -- Set-indicator packaging: `u b := ({d} : Set Bool).indicator 1 b`, which -- satisfies `u (S.factualD ω) = S.dVar.indicator d ω`. let u : Bool → ℝ := ({d} : Set Bool).indicator (fun _ => (1 : ℝ)) have hu_meas : Measurable u := measurable_const.indicator (MeasurableSet.singleton d) have hu_eq : (fun ω => u (S.factualD ω)) = S.dVar.indicator d := by funext ω unfold POVar.indicator by_cases h : S.factualD ω = d · have h1 : S.factualD ω ∈ ({d} : Set Bool) := h have h2 : ω ∈ S.dVar.event d := h rw [show u (S.factualD ω) = (1 : ℝ) from Set.indicator_of_mem h1 _, Set.indicator_of_mem h2] · have h1 : S.factualD ω ∉ ({d} : Set Bool) := h have h2 : ω ∉ S.dVar.event d := h rw [show u (S.factualD ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _, Set.indicator_of_notMem h2] have huMul_int : Integrable (fun ω => u (S.factualD ω) * S.YofD d ω) P.μ := by have hEq : (fun ω => u (S.factualD ω) * S.YofD d ω) = (fun ω => S.YofD d ω * S.dVar.indicator d ω) := by funext ω; rw [show u (S.factualD ω) = S.dVar.indicator d ω from congr_fun hu_eq ω]; ring rw [hEq]; exact hYofD_bdd_integrable_aux have hfact : P.μ[fun ω => u (S.factualD ω) * S.YofD d ω | S.sigmaX] =ᵐ[P.μ] P.μ[fun ω => u (S.factualD ω) | S.sigmaX] * P.μ[fun ω => S.YofD d ω | S.sigmaX] := by have := condExp_mul_of_condIndep (μ := P.μ) (m := S.sigmaX) S.sigmaX_le (f := S.factualD) (g := S.YofD d) S.measurable_factualD (S.measurable_YofD d) hCI (u := u) (v := id) hu_meas measurable_id (by rw [hu_eq]; exact hindD_integrable) hYofD_integrable huMul_int exact this -- Goal (after hindMul_swap): -- S.xVar.condExpGiven (indD d * YofD d) =ᵐ S.xVar.condExpGiven (indD d) * CATE d. -- Unfold condExpGiven/CATE to land on μ[·|σX] with matching argument shapes. unfold POVar.condExpGiven POBackdoorSystem.CATE POBackdoorSystem.sigmaX POBackdoorSystem.factualX have hfact_rw : (fun ω => u (S.factualD ω)) = S.dVar.indicator d := hu_eq have hprod_rw : (fun ω => u (S.factualD ω) * S.YofD d ω) = (fun ω => S.dVar.indicator d ω * S.YofD d ω) := by funext ω; rw [congr_fun hu_eq ω] rw [hprod_rw, hfact_rw] at hfact exact hfact · -- (hne): μ[1_{D=d}|σX] ≠ 0 a.s. — supplied directly as `h_ne`. -- `S.xVar.condExpGiven (S.dVar.indicator d) P.μ = S.propScore d` definitionally. have hEq : S.xVar.condExpGiven (S.dVar.indicator d) P.μ = S.propScore d := by unfold POVar.condExpGiven POBackdoorSystem.propScore POBackdoorSystem.sigmaX POBackdoorSystem.factualX rfl rw [hEq] exact h_ne -
measurable_factualDXlemma — The observed treatment-covariate pair is measurable.conclusionMeasurable S.factualDXProof (Lean source)
lemma measurable_factualDX : Measurable S.factualDX := S.measurable_factualD.prodMk S.measurable_factualX -
sigmaDX_lelemma — The joint treatment-covariate sigma-algebra is a sub-sigma-algebra of the ambient one.conclusionS.sigmaDX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaDX_le : S.sigmaDX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualDX.comap_le -
sigmaX_le_sigmaDXlemma — σ(X) ≤ σ(D, X): the covariate σ-algebra is coarser than the joint one.conclusionS.sigmaX ≤ S.sigmaDXProof (Lean source)
lemma sigmaX_le_sigmaDX : S.sigmaX ≤ S.sigmaDX := by -- `factualX = snd ∘ factualDX`, so `comap factualX ≤ comap factualDX`. have hfx : S.factualX = snd ∘ S.factualDX := rfl rw [POBackdoorSystem.sigmaX, POBackdoorSystem.sigmaDX, hfx, ← MeasurableSpace.comap_comp] exact MeasurableSpace.comap_mono measurable_snd.comap_le -
stronglyMeasurable_outcomeReglemma — The observed outcome regression is strongly measurable with respect to the joint treatment-covariate sigma-algebra.conclusionStronglyMeasurable[S.sigmaDX] S.outcomeRegProof (Lean source)
lemma stronglyMeasurable_outcomeReg : StronglyMeasurable[S.sigmaDX] S.outcomeReg := MeasureTheory.stronglyMeasurable_condExp -
exists_regFnlemma — The σ(D, X)-measurable outcomeReg factors through (D, X): there is a measurable value-space regression function r : Bool × γ → ℝ with outcomeReg = r ∘ factualDX. This is Doob–Dynkin (exists_eq_measurable_comp); r is the function an ML regressor of Y on (D, X) targets.conclusion∃ r : Bool × γ → ℝ, Measurable r ∧ S.outcomeReg = fun ω => r (S.factualDX ω)Proof (Lean source)
lemma exists_regFn : ∃ r : Bool × γ → ℝ, Measurable r ∧ S.outcomeReg = fun ω => r (S.factualDX ω) := by -- `sigmaDX = comap factualDX`, so `outcomeReg` is `comap factualDX`-measurable; -- Doob–Dynkin (`exists_eq_measurable_comp`) produces the value-space factorisation. have hmeas : Measurable[S.sigmaDX] S.outcomeReg := S.stronglyMeasurable_outcomeReg.measurable obtain ⟨r, hr_meas, hr_eq⟩ := Measurable.exists_eq_measurable_comp (f := S.factualDX) (g := S.outcomeReg) hmeas exact ⟨r, hr_meas, by funext ω; exact congrFun hr_eq ω⟩ -
measurable_regFnlemma — The value-space outcome regression is measurable.conclusionMeasurable S.regFnProof (Lean source)
lemma measurable_regFn : Measurable S.regFn := S.exists_regFn.choose_spec.1 -
outcomeReg_eq_regFnlemma — The observed outcome regression equals the value-space regression evaluated at each unit's observed treatment and covariate.conclusionS.outcomeReg = fun ω => S.regFn (S.factualDX ω)Proof (Lean source)
lemma outcomeReg_eq_regFn : S.outcomeReg = fun ω => S.regFn (S.factualDX ω) := S.exists_regFn.choose_spec.2 -
exists_propScoreLiftlemma — The σ(X)-measurable propensity propScore true factors through factualX: a measurable value-space propensity e : γ → ℝ with propScore true = e ∘ factualX (Doob–Dynkin). This is the value-space propensity an estimator learns.conclusion∃ e : γ → ℝ, Measurable e ∧ S.propScore true = fun ω => e (S.factualX ω)Proof (Lean source)
lemma exists_propScoreLift : ∃ e : γ → ℝ, Measurable e ∧ S.propScore true = fun ω => e (S.factualX ω) := by have hmeas : Measurable[S.sigmaX] (S.propScore true) := (MeasureTheory.stronglyMeasurable_condExp).measurable obtain ⟨e, he_meas, he_eq⟩ := Measurable.exists_eq_measurable_comp (f := S.factualX) (g := S.propScore true) hmeas exact ⟨e, he_meas, by funext ω; exact congrFun he_eq ω⟩ -
measurable_eLiftlemma — The value-space propensity representative is measurable.conclusionMeasurable S.eLiftProof (Lean source)
lemma measurable_eLift : Measurable S.eLift := S.exists_propScoreLift.choose_spec.1 -
propScore_true_eq_eLiftlemma — The treated-arm propensity score equals the value-space propensity evaluated at each unit's observed covariate.conclusionS.propScore true = fun ω => S.eLift (S.factualX ω)Proof (Lean source)
lemma propScore_true_eq_eLift : S.propScore true = fun ω => S.eLift (S.factualX ω) := S.exists_propScoreLift.choose_spec.2 -
regression_adjustment_of_assumptionstheorem — Regression-adjustment, packaged for identified systems. The same observable identity adjustedCE d =ᵐ E[Y|D=d,X], with the two regularity hypotheses of regression_adjustment discharged from the back-door Assumptions: integrability of the observed outcome from Assumptions.integrable_factualY, and overlap from propScore_ne_of_overlap. Lets callers in an identified context apply it with just hA.hypothesesconclusionS.adjustedCE d =ᵐ[P.μ] (fun ω => S.regFn (d, S.factualX ω))Proof (Lean source)
theorem regression_adjustment_of_assumptions [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.Assumptions) (d : Bool) : S.adjustedCE d =ᵐ[P.μ] (fun ω => S.regFn (d, S.factualX ω)) := S.regression_adjustment d hA.integrable_factualY (S.propScore_ne_of_overlap hA.overlap d)
ATT 6 core · 1 supporting This file identifies the average treatment effect on the treated from observed data under back-door assumptions, expressing the causal target through covariate-adjusted treated outcomes and an equivalent augmented invers ★ ATT_eq_adjustedATT★ adjustedATT_eq_aipwForm
This file identifies the average treatment effect on the treated from observed data under back-door assumptions, expressing the causal target through covariate-adjusted treated outcomes and an equivalent augmented inverse-probability weighted form.
It reuses POBackdoorSystem from the ATE file but weakens the overlap
requirement to the control arm. The public API includes ATTAssumptions,
ATT_eq_adjustedATT, and adjustedATT_eq_aipwForm, respectively packaging the
one-sided assumptions, the adjusted ATT identification theorem, and the AIPW
representation.
def propTreated reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Marginal probability of being treated, π_T = E[1_{D=1}] = P[D=1].
Definition (Lean source)
noncomputable def propTreated : ℝ :=
∫ ω, S.dVar.indicator true ω ∂P.μ
def ATT reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
ATT (Average Treatment Effect on the Treated): ATT = E[A · (Y(1) − Y(0))] / π_T.
def adjustedATT reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Adjusted ATT (observable, control-regression form): E[A · (Y − μ₀(X))] / π_T. Only the CONTROL regression μ₀(X) = adjustedCE false appears — the treated potential outcome is observed directly on {D = 1} via consistency (A · Y = A · Y(1)), so no treated regression μ₁(X) and hence no 0 < e(X) is needed. This is the standard ATT estimand and requires only one-sided overlap e(X) < 1. The AIPW form is recovered as a corollary (adjustedATT_eq_aipwForm).
structure ATTAssumptions reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
Backdoor assumptions for ATT identification. These are the standard ATT conditions, with overlap required on only one side — every covariate stratum keeps a positive chance of the control arm (e(X) < 1) — which is strictly weaker than the two-sided overlap the ATE needs, because on the treated the outcome is observed directly.
Definition (Lean source)
parameters
fields
Consistency (SUTVA): on `{D = d}`, the observed outcome equals `Y(d)`.
consistency :
P.Consistency
Unconfoundedness: `D ⟂ (Y(1), Y(0)) | X`, as conditional independence of the
realized `D` and the counterfactual bundle given `σ(X)`.
unconfoundedness :
P.CondIndepCF (RegimedVar.ofFactual S.dVar) S.cfBundle (RegimedVar.ofFactual S.xVar) P.μ
One-sided overlap (control common support): `P[D=1 | σ(X)] < 1` a.s. Only the
upper bound is needed for ATT — the treated arm is observed directly.
overlapControl :
∀ᵐ ω ∂P.μ, S.propScore true ω < 1
Regularity: the treated potential outcome `Y(1)` is integrable.
integrable_Y1 :
Integrable (S.YofD true) P.μ
Regularity: the control potential outcome `Y(0)` is integrable.
integrable_Y0 :
Integrable (S.YofD false) P.μ
Positivity of the marginal treatment probability `π_T = P[D=1]`.
propTreated_pos :
0 < S.propTreated
theorem ATT_eq_adjustedATT reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
ATT identification (one-sided overlap). Under consistency, unconfoundedness, one-sided overlap (e(X) < 1, the control arm), and positivity of the marginal treatment probability, the potential-outcome-level average treatment effect on the treated equals the observable adjusted-ATT functional:
Formal statement
hypotheses
conclusion
S.ATT = S.adjustedATT
Proof (Lean source)
theorem ATT_eq_adjustedATT [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(hA : S.ATTAssumptions) : S.ATT = S.adjustedATT := by
unfold POBackdoorSystem.ATT POBackdoorSystem.adjustedATT
congr 1
have hfalse := S.att_numerator_arm hA false
(S.cate_backdoor_control hA) (S.integrable_adjustedCE_control hA)
have hY1 : Integrable (fun ω => S.dVar.indicator true ω * S.YofD true ω) P.μ := by
have h := S.dVar.integrable_mul_indicator true (measurableSet_singleton true)
hA.integrable_Y1
exact h.congr (Filter.Eventually.of_forall (fun ω => by ring))
have hY0 : Integrable (fun ω => S.dVar.indicator true ω * S.YofD false ω) P.μ := by
have h := S.dVar.integrable_mul_indicator true (measurableSet_singleton true)
hA.integrable_Y0
exact h.congr (Filter.Eventually.of_forall (fun ω => by ring))
have hAfact : Integrable (fun ω => S.dVar.indicator true ω * S.factualY ω) P.μ := by
have h := S.dVar.integrable_mul_indicator true (measurableSet_singleton true)
(S.integrable_factualY_of_consistency
hA.consistency hA.integrable_Y1 hA.integrable_Y0)
exact h.congr (Filter.Eventually.of_forall (fun ω => by ring))
have hAdj0 : Integrable (fun ω => S.dVar.indicator true ω * S.adjustedCE false ω) P.μ := by
have h := S.dVar.integrable_mul_indicator true (measurableSet_singleton true)
(S.integrable_adjustedCE_control hA)
exact h.congr (Filter.Eventually.of_forall (fun ω => by ring))
-- On the treated set, consistency gives `A · Y = A · Y(1)`.
have hcons :
(fun ω => S.dVar.indicator true ω * S.factualY ω)
= (fun ω => S.dVar.indicator true ω * S.YofD true ω) := by
have hfm :=
POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn
hA.consistency S.yVar S.dVar true (Ne.symm S.hDY)
funext ω
have hω := congr_fun hfm ω
change S.dVar.indicator true ω * S.factualY ω
= S.dVar.indicator true ω * S.YofD true ω
rw [mul_comm (S.dVar.indicator true ω) (S.factualY ω),
mul_comm (S.dVar.indicator true ω) (S.YofD true ω)]
exact hω
calc
∫ ω, S.dVar.indicator true ω * (S.YofD true ω - S.YofD false ω) ∂P.μ
= ∫ ω, (S.dVar.indicator true ω * S.YofD true ω)
- (S.dVar.indicator true ω * S.YofD false ω) ∂P.μ := by
congr with ω
ring
_ = (∫ ω, S.dVar.indicator true ω * S.YofD true ω ∂P.μ)
- (∫ ω, S.dVar.indicator true ω * S.YofD false ω ∂P.μ) := by
exact MeasureTheory.integral_sub hY1 hY0
_ = (∫ ω, S.dVar.indicator true ω * S.factualY ω ∂P.μ)
- (∫ ω, S.dVar.indicator true ω * S.adjustedCE false ω ∂P.μ) := by
rw [← MeasureTheory.integral_congr_ae (Filter.EventuallyEq.of_eq hcons), hfalse]
_ = ∫ ω, (S.dVar.indicator true ω * S.factualY ω)
- (S.dVar.indicator true ω * S.adjustedCE false ω) ∂P.μ := by
exact (MeasureTheory.integral_sub hAfact hAdj0).symm
_ = ∫ ω, S.dVar.indicator true ω *
(S.factualY ω - S.adjustedCE false ω) ∂P.μ := by
congr with ω
ring
theorem adjustedATT_eq_aipwForm reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
AIPW corollary. Under the ATT identification assumptions — consistency, unconfoundedness, one-sided control-arm overlap, and a positive marginal treatment probability, provided the observed inverse-propensity-weighted correction term is integrable, the adjustedATT functional equals its augmented inverse-propensity-weighted (AIPW) form:
Formal statement
hypotheses
IsFiniteMeasure P.μ
hA :
S.ATTAssumptions
hIPW :
Integrable (fun ω => (1 - S.dVar.indicator true ω) * (S.propScore true ω / (1 - S.propScore true ω)) * (S.factualY ω - S.adjustedCE false ω)) P.μ
Proof (Lean source)
theorem adjustedATT_eq_aipwForm [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(hA : S.ATTAssumptions)
(hIPW : Integrable (fun ω =>
(1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω)) P.μ) :
S.adjustedATT
= ((∫ ω,
S.dVar.indicator true ω * (S.factualY ω - S.adjustedCE false ω)
- (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω)
∂P.μ))
/ S.propTreated := by
let W : P.Ω → ℝ := fun ω => S.propScore true ω / (1 - S.propScore true ω)
let R : P.Ω → ℝ := fun ω => S.factualY ω - S.adjustedCE false ω
have hW_sm : StronglyMeasurable[S.sigmaX] W := by
unfold W POBackdoorSystem.propScore
exact ((MeasureTheory.stronglyMeasurable_condExp
(μ := P.μ) (m := S.sigmaX) (f := S.dVar.indicator true)).measurable.div
(measurable_const.sub
(MeasureTheory.stronglyMeasurable_condExp
(μ := P.μ) (m := S.sigmaX) (f := S.dVar.indicator true)).measurable)).stronglyMeasurable
have hfalse_indicator : ∀ ω, 1 - S.dVar.indicator true ω = S.dVar.indicator false ω := by
intro ω
have hsum := S.dVar.indicator_add_indicator_not ω
linarith
have hIPW_weighted : Integrable
(fun ω => W ω * (S.dVar.indicator false ω * R ω)) P.μ := by
refine hIPW.congr ?_
refine Filter.Eventually.of_forall (fun ω => ?_)
unfold W R
change (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω)
= S.propScore true ω / (1 - S.propScore true ω)
* (S.dVar.indicator false ω * (S.factualY ω - S.adjustedCE false ω))
rw [hfalse_indicator ω]
ring
have hIPW_zero :
∫ ω, (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω) ∂P.μ = 0 := by
have hweighted_zero :=
S.weighted_false_residual_integral_zero hA W hW_sm hIPW_weighted
calc
∫ ω, (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω) ∂P.μ
= ∫ ω, W ω * (S.dVar.indicator false ω * R ω) ∂P.μ := by
apply MeasureTheory.integral_congr_ae
refine Filter.Eventually.of_forall (fun ω => ?_)
unfold W R
change (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω)
= S.propScore true ω / (1 - S.propScore true ω)
* (S.dVar.indicator false ω * (S.factualY ω - S.adjustedCE false ω))
rw [hfalse_indicator ω]
ring
_ = 0 := hweighted_zero
have htreated_int :
Integrable (fun ω => S.dVar.indicator true ω *
(S.factualY ω - S.adjustedCE false ω)) P.μ := by
have hYind_int : Integrable (fun ω => S.dVar.indicator true ω * S.factualY ω) P.μ := by
have h := S.dVar.integrable_mul_indicator true (measurableSet_singleton true)
(S.integrable_factualY_of_consistency
hA.consistency hA.integrable_Y1 hA.integrable_Y0)
exact h.congr (Filter.Eventually.of_forall (fun ω => by ring))
have hAdjind_int : Integrable
(fun ω => S.dVar.indicator true ω * S.adjustedCE false ω) P.μ := by
have h :=
S.dVar.integrable_mul_indicator true (measurableSet_singleton true)
(S.integrable_adjustedCE_control hA)
exact h.congr (Filter.Eventually.of_forall (fun ω => by ring))
exact (hYind_int.sub hAdjind_int).congr
(Filter.Eventually.of_forall (fun ω => by
change S.dVar.indicator true ω * S.factualY ω
- S.dVar.indicator true ω * S.adjustedCE false ω
= S.dVar.indicator true ω * (S.factualY ω - S.adjustedCE false ω)
ring))
have hnumer :
∫ ω,
S.dVar.indicator true ω * (S.factualY ω - S.adjustedCE false ω)
- (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω) ∂P.μ
= ∫ ω, S.dVar.indicator true ω *
(S.factualY ω - S.adjustedCE false ω) ∂P.μ := by
calc
∫ ω,
S.dVar.indicator true ω * (S.factualY ω - S.adjustedCE false ω)
- (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω) ∂P.μ
= (∫ ω, S.dVar.indicator true ω *
(S.factualY ω - S.adjustedCE false ω) ∂P.μ)
- ∫ ω, (1 - S.dVar.indicator true ω)
* (S.propScore true ω / (1 - S.propScore true ω))
* (S.factualY ω - S.adjustedCE false ω) ∂P.μ := by
exact MeasureTheory.integral_sub htreated_int hIPW
_ = ∫ ω, S.dVar.indicator true ω *
(S.factualY ω - S.adjustedCE false ω) ∂P.μ := by
rw [hIPW_zero, sub_zero]
unfold POBackdoorSystem.adjustedATT
congr 1
exact hnumer.symm
1 supporting declaration (lemmas, instances)
-
propScore_false_nelemma — Under one-sided overlap (e(X) < 1), the control propensity score P[D=0 | σ(X)] = 1 - e(X) is a.s. nonzero.hypothesesconclusion∀ᵐ ω ∂P.μ, S.propScore false ω ≠ 0Proof (Lean source)
lemma ATTAssumptions.propScore_false_ne [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.ATTAssumptions) : ∀ᵐ ω ∂P.μ, S.propScore false ω ≠ 0 := by filter_upwards [S.propScore_false_ae, hA.overlapControl] with ω hf hlt rw [hf] intro h linarith
CSDID 19 core · 13 supporting This file develops the potential-outcome setup for Callaway-Sant'Anna group-time treatment effects. ★ POCSDIDSystem★ att_csdid
Staggered-Adoption Difference-in-Differences
This file develops the potential-outcome setup for Callaway-Sant'Anna group-time treatment effects. It encodes treatment cohorts, never-treated comparisons, and the assumptions needed to identify the average treatment effect for a cohort at a time period.
It extends two-period DID to a finite horizon with first-treated cohorts and a never-treated comparison group. Periods are zero-indexed, so admissible group-time effects use a cohort after the first period and an outcome period no earlier than that cohort.
The central definitions are regOf, regNT, cohortEvent,
neverTreatedEvent, and the group-time estimand ATT; the main theorem
att_csdid proves the observable group-time DID contrast under the
Callaway-Sant'Anna assumptions.
structure POCSDIDSystem reviewed
⚑ flagged
Causalean.PO
A staggered-adoption DID system has a binary treatment variable at each of T periods, where at least two periods are observed, together with a real outcome variable at each period, such that the treatment nodes are pairwise distinct across periods and likewise for the outcome nodes, and no treatment node coincides with any outcome node.
def dVar reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The treatment at a period is packaged as a binary potential-outcome variable.
def yVar reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The outcome at a period is packaged as a real-valued potential-outcome variable.
def factualD reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The factual treatment at a period is the observed treatment value for that period.
def factualY reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The factual outcome at a period is the observed outcome value for that period.
def dEvent reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The period-specific treatment event contains units with the chosen observed treatment value.
def dTargetUpTo reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The standalone target set contains the treatment nodes from periods before the cutoff.
Definition (Lean source)
def dTargetUpTo (S : POCSDIDSystem P) : ℕ → Finset P.V
| 0 => ∅
| k + 1 =>
if h : k < S.T then insert (S.D ⟨k, h⟩) (S.dTargetUpTo k)
else S.dTargetUpTo k
def regUpToAux reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The recursive auxiliary builds a treatment-path regime over the first periods and records its target set.
Definition (Lean source)
noncomputable def regUpToAux (S : POCSDIDSystem P) (b : Fin S.T → Bool) :
(k : ℕ) → k ≤ S.T →
{ r : Regime P.V P.X // r.target = S.dTargetUpTo k }
| 0, _ => ⟨Regime.empty, by simp [dTargetUpTo, Regime.empty]⟩
| k + 1, h =>
have hk : k < S.T := h
let pair := S.regUpToAux b k (le_of_lt hk)
let r_rec : Regime P.V P.X := pair.1
have hrec : r_rec.target = S.dTargetUpTo k := pair.2
let v := S.D ⟨k, hk⟩
have hv_not : v ∉ r_rec.target := by
rw [hrec]
intro hmem
rcases (S.dTargetUpTo_mem_iff k (le_of_lt hk) _).mp hmem with
⟨i, hi, heq⟩
have hFin : (⟨k, hk⟩ : Fin S.T) = i := S.hDinj heq
have hval : (k : ℕ) = i.val := by
have := congrArg val hFin; simpa using this
omega
let r_new := Regime.sqcup
(Regime.single v ((S.hDbool ⟨k, hk⟩).symm (b ⟨k, hk⟩))) r_rec
(Regime.single_disjoint_of_not_mem _ _ hv_not)
⟨r_new, by
show r_new.target = S.dTargetUpTo (k + 1)
simp only [r_new, Regime.sqcup_target, Regime.single_target,
dTargetUpTo, hk, ↓reduceDIte]
rw [hrec]
ext w; simp [Finset.mem_insert, v]⟩
def regimeBy reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
A full-horizon regime fixes every period's treatment according to a chosen treatment path.
def regOf reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The cohort regime leaves periods before the cohort untreated and treats all later periods.
def regNT reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The never-treated regime fixes every period's treatment to untreated.
def YofCohort reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The cohort potential outcome is the period outcome under the treatment path for that cohort.
def YofNT reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The never-treated potential outcome is the period outcome under the never-treated path.
def predFin reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The predecessor of an admissible cohort is the immediately preceding period.
Definition (Lean source)
def predFin (g : Fin S.T) (_hg : 1 ≤ g.val) : Fin S.T :=
⟨g.val - 1, lt_of_le_of_lt (Nat.sub_le _ _) g.isLt⟩
def cohortEvent reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The cohort event contains units untreated just before the cohort period and treated at the cohort period.
Definition (Lean source)
def cohortEvent (g : Fin S.T) (hg : 1 ≤ g.val) : Set P.Ω :=
S.dEvent (S.predFin g hg) false ∩ S.dEvent g true
def neverTreatedEvent reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The never-treated event contains units untreated in every period.
def ATT reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The group-time ATT is the cohort mean contrast between cohort and never-treated potential outcomes.
Definition (Lean source)
noncomputable def ATT (g t : Fin S.T) (hg : 1 ≤ g.val) : ℝ :=
eventCondExp P.μ (S.cohortEvent g hg)
(fun ω => S.YofCohort t g ω - S.YofNT t ω)
structure Assumptions reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
The Callaway-Sant'Anna assumptions combine consistency of the underlying potential-outcome system: no unit is treated at period zero and once treated, a unit remains treated in every later period (irreversible adoption); pre-treatment outcomes do not anticipate future treatment; each cohort's mean untreated trend matches the never-treated group's mean untreated trend; each cohort and the never-treated group occur with positive, finite probability; and the cohort and never-treated potential outcomes are integrable.
Definition (Lean source)
parameters
S :
fields
Consistency of the underlying PO system.
consistency :
P.Consistency
Irreversibility, base case: `D_0 = 0` almost surely.
irreversibilityBase :
∀ᵐ ω ∂P.μ, S.factualD ⟨0, lt_of_lt_of_le Nat.zero_lt_two S.hT⟩ ω = false
Irreversibility, absorbing: `D_s = 1 ⟹ D_{s+1} = 1` almost surely.
irreversibilityStep :
No anticipation: pre-treatment outcomes are unaffected by future treatment.
noAnticipation :
∀ (g s : Fin S.T)
if
s.val < g.val
then
∀ᵐ ω ∂P.μ, S.YofCohort s g ω = S.YofNT s ω
Never-treated parallel trends (long-difference form).
parallelTrends :
∀ (g t : Fin S.T) (hg : 1 ≤ g.val) (_hgt : g.val ≤ t.val),
eventCondExp P.μ (S.cohortEvent g hg) (fun ω => S.YofNT t ω - S.YofNT (S.predFin g hg) ω)
= eventCondExp P.μ S.neverTreatedEvent (fun ω => S.YofNT t ω - S.YofNT (S.predFin g hg) ω)
Positivity of cohorts.
posCohort :
∀ (g : Fin S.T) (hg : 1 ≤ g.val),
P.μ (S.cohortEvent g hg) ≠ 0 ∧ P.μ (S.cohortEvent g hg) ≠ ⊤
Positivity of the never-treated event.
posNT :
P.μ S.neverTreatedEvent ≠ 0 ∧ P.μ S.neverTreatedEvent ≠ ⊤
Integrability of `Y_t(g)` for every cohort-period pair.
intYofCohort :
∀ g t : Fin S.T, Integrable (S.YofCohort t g) P.μ
Integrability of `Y_t(∞)`.
intYofNT :
∀ t : Fin S.T, Integrable (S.YofNT t) P.μ
theorem att_csdid reviewed
⚑ flagged
Causalean.PO.POCSDIDSystem
Callaway--Sant'Anna group-time DID identification of ATT(g, t). Under the group-time assumptions — consistency, no-anticipation, and group-time parallel trends, for a treatment cohort g that starts treatment no earlier than period 1 and a calendar period t no earlier than g, the group-time average treatment effect on the treated equals the difference between the cohort-g mean outcome change from the period before g to period t and the corresponding mean outcome change for the never-treated group:
Formal statement
hypotheses
conclusion
S.ATT g t hg
= eventCondExp P.μ (S.cohortEvent g hg) (fun ω => S.factualY t ω - S.factualY (S.predFin g hg) ω)
- eventCondExp P.μ S.neverTreatedEvent (fun ω => S.factualY t ω - S.factualY (S.predFin g hg) ω)
Proof (Lean source)
theorem att_csdid (hA : S.Assumptions) (g t : Fin S.T)
(hg : 1 ≤ g.val) (hgt : g.val ≤ t.val) :
S.ATT g t hg
= eventCondExp P.μ (S.cohortEvent g hg)
(fun ω => S.factualY t ω - S.factualY (S.predFin g hg) ω)
- eventCondExp P.μ S.neverTreatedEvent
(fun ω => S.factualY t ω - S.factualY (S.predFin g hg) ω) := by
have hPredLtG : (S.predFin g hg).val < g.val := by
have : g.val - 1 < g.val :=
sub_lt (lt_of_lt_of_le Nat.zero_lt_one hg) Nat.zero_lt_one
simpa [predFin] using this
have hAE : (fun ω => S.YofCohort t g ω - S.YofNT t ω)
=ᵐ[P.μ] fun ω =>
(S.YofCohort t g ω - S.YofCohort (S.predFin g hg) g ω) -
(S.YofNT t ω - S.YofNT (S.predFin g hg) ω) := by
refine (hA.noAnticipation g (S.predFin g hg) hPredLtG).mono (fun ω hω => ?_)
change S.YofCohort t g ω - S.YofNT t ω
= (S.YofCohort t g ω - S.YofCohort (S.predFin g hg) g ω) -
(S.YofNT t ω - S.YofNT (S.predFin g hg) ω)
rw [hω]
ring
have hATT_split :
S.ATT g t hg
= eventCondExp P.μ (S.cohortEvent g hg)
(fun ω => S.YofCohort t g ω - S.YofCohort (S.predFin g hg) g ω)
- eventCondExp P.μ (S.cohortEvent g hg)
(fun ω => S.YofNT t ω - S.YofNT (S.predFin g hg) ω) := by
unfold ATT
rw [eventCondExp_congr_ae P.μ (S.cohortEvent g hg) (ae_restrict_of_ae hAE)]
exact eventCondExp_sub P.μ (S.cohortEvent g hg)
((hA.intYofCohort g t).sub (hA.intYofCohort g (S.predFin g hg))).integrableOn
((hA.intYofNT t).sub (hA.intYofNT (S.predFin g hg))).integrableOn
have h_first :
eventCondExp P.μ (S.cohortEvent g hg)
(fun ω => S.YofCohort t g ω - S.YofCohort (S.predFin g hg) g ω)
= eventCondExp P.μ (S.cohortEvent g hg)
(fun ω => S.factualY t ω - S.factualY (S.predFin g hg) ω) := by
unfold eventCondExp
rw [MeasureTheory.integral_congr_ae]
rw [EventuallyEq, MeasureTheory.ae_restrict_iff' (S.measurableSet_cohortEvent g hg)]
filter_upwards [S.factualY_eq_YofCohort_on_cohortEvent hA g t hg,
S.factualY_eq_YofCohort_on_cohortEvent hA g (S.predFin g hg) hg] with ω ht hpred hω
rw [ht hω, hpred hω]
have h_pt : eventCondExp P.μ (S.cohortEvent g hg)
(fun ω => S.YofNT t ω - S.YofNT (S.predFin g hg) ω)
= eventCondExp P.μ S.neverTreatedEvent
(fun ω => S.YofNT t ω - S.YofNT (S.predFin g hg) ω) :=
hA.parallelTrends g t hg hgt
have h_second :
eventCondExp P.μ S.neverTreatedEvent
(fun ω => S.YofNT t ω - S.YofNT (S.predFin g hg) ω)
= eventCondExp P.μ S.neverTreatedEvent
(fun ω => S.factualY t ω - S.factualY (S.predFin g hg) ω) := by
unfold eventCondExp
rw [MeasureTheory.integral_congr_ae]
rw [EventuallyEq, MeasureTheory.ae_restrict_iff' S.measurableSet_neverTreatedEvent]
filter_upwards [S.factualY_eq_YofNT_on_NT hA t,
S.factualY_eq_YofNT_on_NT hA (S.predFin g hg)] with ω ht hpred hω
rw [ht hω, hpred hω]
rw [hATT_split, h_first, h_pt, h_second]
13 supporting declarations (lemmas, instances)
-
measurable_factualDlemma — The observed treatment at each period is measurable.Proof (Lean source)
lemma measurable_factualD (s : Fin S.T) : Measurable (S.factualD s) := (S.dVar s).measurable_factual -
measurable_factualYlemma — The observed outcome at each period is measurable.Proof (Lean source)
lemma measurable_factualY (s : Fin S.T) : Measurable (S.factualY s) := (S.yVar s).measurable_factual -
measurableSet_dEventlemma — Each period-specific treatment event is measurable.Proof (Lean source)
lemma measurableSet_dEvent (s : Fin S.T) (b : Bool) : MeasurableSet (S.dEvent s b) := (S.dVar s).measurableSet_event _ (measurableSet_singleton _) -
dTargetUpTo_mem_ifflemma — Membership in the target set is exactly being a treatment node before the cutoff.hypothesesS :conclusion∀ (k : ℕ) (_ : k ≤ S.T) (v : P.V),v ∈ S.dTargetUpTo k↔ ∃ i : Fin S.T, i.val < k ∧ v = S.D i | 0, _, v => by simp [dTargetUpTo] | k+ 1, h, v => by have hk : k < S.TProof (Lean source)
lemma dTargetUpTo_mem_iff (S : POCSDIDSystem P) : ∀ (k : ℕ) (_ : k ≤ S.T) (v : P.V), v ∈ S.dTargetUpTo k ↔ ∃ i : Fin S.T, i.val < k ∧ v = S.D i | 0, _, v => by simp [dTargetUpTo] | k + 1, h, v => by have hk : k < S.T := h simp only [dTargetUpTo, hk, ↓reduceDIte, Finset.mem_insert] constructor · rintro (rfl | hmem) · exact ⟨⟨k, hk⟩, Nat.lt_succ_self _, rfl⟩ · rcases (S.dTargetUpTo_mem_iff k (le_of_lt hk) v).mp hmem with ⟨i, hi, rfl⟩ exact ⟨i, Nat.lt_succ_of_lt hi, rfl⟩ · rintro ⟨i, hi, rfl⟩ rcases Nat.lt_succ_iff_lt_or_eq.mp hi with hi' | hi' · exact inr ((S.dTargetUpTo_mem_iff k (le_of_lt hk) _).mpr ⟨i, hi', rfl⟩) · left have : (⟨k, hk⟩ : Fin S.T) = i := by apply Fin.ext; simp [hi'] rw [this] -
regimeBy_target_eqlemma — The target of a full-horizon treatment-path regime is the full set of treatment nodes.Proof (Lean source)
lemma regimeBy_target_eq (S : POCSDIDSystem P) (b : Fin S.T → Bool) : (S.regimeBy b).target = S.dTargetUpTo S.T := (S.regUpToAux b S.T (le_refl _)).2 -
Y_notin_dTargetUpTolemma — An outcome node is not among the treatment targets before any cutoff.Proof (Lean source)
lemma Y_notin_dTargetUpTo (t : Fin S.T) : ∀ k, k ≤ S.T → S.Y t ∉ S.dTargetUpTo k := by intro k hk hmem rcases (S.dTargetUpTo_mem_iff k hk _).mp hmem with ⟨i, _, heq⟩ exact (S.hDY i t) heq.symm -
Y_notin_regimeBylemma — An outcome node is not targeted by any full-horizon treatment-path regime. -
yVar_v_notin_regOf_targetlemma — The outcome variable at a period is not targeted by the cohort regime.Proof (Lean source)
lemma yVar_v_notin_regOf_target (t g : Fin S.T) : (S.yVar t).v ∉ (S.regOf g).target := S.Y_notin_regimeBy t _ -
yVar_v_notin_regNT_targetlemma — The outcome variable at a period is not targeted by the never-treated regime.Proof (Lean source)
lemma yVar_v_notin_regNT_target (t : Fin S.T) : (S.yVar t).v ∉ S.regNT.target := S.Y_notin_regimeBy t _ -
measurable_YofCohortlemma — Cohort potential outcomes are measurable.Proof (Lean source)
lemma measurable_YofCohort (t g : Fin S.T) : Measurable (S.YofCohort t g) := (S.yVar t).measurable_cf _ -
measurable_YofNTlemma — Never-treated potential outcomes are measurable.Proof (Lean source)
-
measurableSet_cohortEventlemma — Each cohort event is measurable.Proof (Lean source)
lemma measurableSet_cohortEvent (g : Fin S.T) (hg : 1 ≤ g.val) : MeasurableSet (S.cohortEvent g hg) := (S.measurableSet_dEvent _ _).inter (S.measurableSet_dEvent _ _) -
measurableSet_neverTreatedEventlemma — The never-treated event is measurable.conclusionMeasurableSet S.neverTreatedEventProof (Lean source)
lemma measurableSet_neverTreatedEvent : MeasurableSet S.neverTreatedEvent := MeasurableSet.iInter (fun s => S.measurableSet_dEvent s _)
DID 13 core · 6 supporting This file formalizes two-period difference-in-differences identification of the average treatment effect on the treated. ★ PODIDSystem★ att_did
Two-Period Difference-in-Differences
This file formalizes two-period difference-in-differences identification of the average treatment effect on the treated. It packages the treatment and outcome variables, the parallel-trends assumptions, and the resulting observable contrast.
The proof works at the event-conditional-mean level: it needs consistency, no
anticipation, parallel trends, positivity of treated and control groups, and
integrability of the counterfactual outcomes that enter the DID contrast. The
main theorem att_did identifies the treated-group mean counterfactual contrast
with the observed treated-minus-control difference in outcome changes.
structure PODIDSystem reviewed
⚑ flagged
Causalean.PO
A two-period DID system packages a treatment node whose value space is identified with the booleans, together with a pre-period outcome node and a post-period outcome node each of whose value spaces is identified with the real line; the treatment node is required to be distinct from the pre-period outcome node and distinct from the post-period outcome node.
def dVar reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The treatment node is packaged as a binary potential-outcome variable.
def y0Var reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The pre-period outcome node is packaged as a real-valued potential-outcome variable.
Definition (Lean source)
def y0Var : POVar P ℝ := ⟨S.Y₀, S.hY0real⟩
def y1Var reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The post-period outcome node is packaged as a real-valued potential-outcome variable.
Definition (Lean source)
def y1Var : POVar P ℝ := ⟨S.Y₁, S.hY1real⟩
def Y0ofD reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The pre-period potential outcome is evaluated under the intervention that fixes treatment.
def Y1ofD reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The post-period potential outcome is evaluated under the intervention that fixes treatment.
def factualD reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The factual treatment is the observed binary treatment value.
Definition (Lean source)
noncomputable def factualD : P.Ω → Bool := S.dVar.factual
def factualY₀ reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The factual pre-period outcome is the observed pre-period outcome value.
Definition (Lean source)
noncomputable def factualY₀ : P.Ω → ℝ := S.y0Var.factual
def factualY₁ reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The factual post-period outcome is the observed post-period outcome value.
Definition (Lean source)
noncomputable def factualY₁ : P.Ω → ℝ := S.y1Var.factual
def dEvent reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The treatment event contains the units whose observed treatment equals the chosen arm.
def ATT reviewed
⚑ flagged
Causalean.PO.PODIDSystem
The ATT is the treated-group mean difference between treated and untreated post-period potential outcomes.
Definition (Lean source)
noncomputable def ATT : ℝ :=
eventCondExp P.μ (S.dEvent true) (fun ω => S.Y1ofD true ω - S.Y1ofD false ω)
structure Assumptions reviewed
⚑ flagged
Causalean.PO.PODIDSystem
Assumptions for two-period difference-in-differences identification of the ATT (def:po-did-assumptions). In words: the observed outcomes coincide with the realized-arm potential outcomes; in the pre-period the treated and control groups have the same potential outcome regardless of treatment; and absent treatment the two groups would have changed in parallel between the two periods. The treated group and the control group each occur with positive probability, and the control pre-period outcome, the control post-period outcome, and the treated post-period outcome are integrable, so the group-conditional means are well-defined and finite.
Definition (Lean source)
parameters
S :
fields
Consistency (SUTVA): the observed outcome equals the potential outcome of
the realized treatment arm.
consistency :
P.Consistency
No anticipation: in the pre-period the potential outcome does not depend on
the (future) treatment, so `Y₀(1) = Y₀(0)` a.s.
Parallel trends: the average untreated change from the pre- to the
post-period is the same in the treated group as in the control group.
parallelTrends :
The treated group has positive probability, so its group-mean is defined.
(Finiteness `μ ≠ ⊤` is automatic: `P.μ` is a probability measure.)
posTrue_ne_zero :
P.μ (S.dEvent true) ≠ 0
The control group has positive probability, so its group-mean is defined.
posFalse_ne_zero :
P.μ (S.dEvent false) ≠ 0
Integrability of the control pre-period potential outcome `Y₀(0)`.
intY0ofD_false :
Integrable (S.Y0ofD false) P.μ
Integrability of the control post-period potential outcome `Y₁(0)`.
intY1ofD_false :
Integrable (S.Y1ofD false) P.μ
Integrability of the treated post-period potential outcome `Y₁(1)`.
intY1ofD_true :
Integrable (S.Y1ofD true) P.μ
theorem att_did reviewed
⚑ flagged
Causalean.PO.PODIDSystem
Under the two-period DID assumptions — consistency, no-anticipation, parallel trends, and positive-probability, integrable treatment and control groups, the average treatment effect on the treated equals the difference between the treated group's mean pre-to-post outcome change and the control group's mean pre-to-post outcome change.
Formal statement
hypotheses
hA :
S.Assumptions
conclusion
S.ATT
= eventCondExp P.μ (S.dEvent true) (fun ω => S.factualY₁ ω - S.factualY₀ ω)
- eventCondExp P.μ (S.dEvent false) (fun ω => S.factualY₁ ω - S.factualY₀ ω)
Proof (Lean source)
theorem att_did (hA : S.Assumptions) :
S.ATT
= eventCondExp P.μ (S.dEvent true)
(fun ω => S.factualY₁ ω - S.factualY₀ ω)
- eventCondExp P.μ (S.dEvent false)
(fun ω => S.factualY₁ ω - S.factualY₀ ω) := by
-- Step 1: by no anticipation, `Y₁(1) - Y₁(0)` rewrites a.e. as
-- `(Y₁(1) - Y₀(1)) - (Y₁(0) - Y₀(0))`.
have hAE : (fun ω => S.Y1ofD true ω - S.Y1ofD false ω)
=ᵐ[P.μ] fun ω =>
(S.Y1ofD true ω - S.Y0ofD true ω) -
(S.Y1ofD false ω - S.Y0ofD false ω) := by
refine hA.noAnticipation.mono (fun ω hω => ?_)
change S.Y1ofD true ω - S.Y1ofD false ω
= (S.Y1ofD true ω - S.Y0ofD true ω) - (S.Y1ofD false ω - S.Y0ofD false ω)
rw [hω]; ring
-- Step 2: split via additivity. Use the `eventCondExp` definition and
-- `integral_congr_ae` + `integral_sub`.
have hATT_split :
S.ATT
= eventCondExp P.μ (S.dEvent true)
(fun ω => S.Y1ofD true ω - S.Y0ofD true ω)
- eventCondExp P.μ (S.dEvent true)
(fun ω => S.Y1ofD false ω - S.Y0ofD false ω) := by
unfold ATT
rw [eventCondExp_congr_ae P.μ (S.dEvent true) (ae_restrict_of_ae hAE)]
-- `Y0ofD true` is integrable via a.e. equality with `Y0ofD false`.
have hY0true_int : Integrable (S.Y0ofD true) P.μ :=
hA.intY0ofD_false.congr (hA.noAnticipation.mono (fun _ h => h.symm))
exact eventCondExp_sub P.μ (S.dEvent true)
(hA.intY1ofD_true.sub hY0true_int).integrableOn
(hA.intY1ofD_false.sub hA.intY0ofD_false).integrableOn
-- Step 3: on `dEvent true`, consistency gives
-- `Y₁(1) - Y₀(1) = factualY₁ - factualY₀`.
have h_first :
eventCondExp P.μ (S.dEvent true)
(fun ω => S.Y1ofD true ω - S.Y0ofD true ω)
= eventCondExp P.μ (S.dEvent true)
(fun ω => S.factualY₁ ω - S.factualY₀ ω) :=
(eventCondExp_congr_on P.μ (S.measurableSet_dEvent true)
(fun ω hω => (S.factualDiff_eq_cfDiff_on_dEvent hA.consistency true ω hω).symm))
-- Step 4: parallel trends rewrites the second term to condition on `D=0`.
have h_pt : eventCondExp P.μ (S.dEvent true)
(fun ω => S.Y1ofD false ω - S.Y0ofD false ω)
= eventCondExp P.μ (S.dEvent false)
(fun ω => S.Y1ofD false ω - S.Y0ofD false ω) := hA.parallelTrends
-- Step 5: on `dEvent false`, consistency gives
-- `Y₁(0) - Y₀(0) = factualY₁ - factualY₀`.
have h_second :
eventCondExp P.μ (S.dEvent false)
(fun ω => S.Y1ofD false ω - S.Y0ofD false ω)
= eventCondExp P.μ (S.dEvent false)
(fun ω => S.factualY₁ ω - S.factualY₀ ω) :=
eventCondExp_congr_on P.μ (S.measurableSet_dEvent false)
(fun ω hω => (S.factualDiff_eq_cfDiff_on_dEvent hA.consistency false ω hω).symm)
rw [hATT_split, h_first, h_pt, h_second]
6 supporting declarations (lemmas, instances)
-
measurable_Y0ofDlemma — The pre-period potential outcome under a fixed treatment arm is measurable.Proof (Lean source)
-
measurable_Y1ofDlemma — The post-period potential outcome under a fixed treatment arm is measurable.Proof (Lean source)
-
measurable_factualDlemma — The observed treatment is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualY₀lemma — The observed pre-period outcome is measurable.conclusionMeasurable S.factualY₀Proof (Lean source)
lemma measurable_factualY₀ : Measurable S.factualY₀ := S.y0Var.measurable_factual -
measurable_factualY₁lemma — The observed post-period outcome is measurable.conclusionMeasurable S.factualY₁Proof (Lean source)
lemma measurable_factualY₁ : Measurable S.factualY₁ := S.y1Var.measurable_factual -
measurableSet_dEventlemma — Each observed treatment-arm event is measurable.Proof (Lean source)
lemma measurableSet_dEvent (d : Bool) : MeasurableSet (S.dEvent d) := S.dVar.measurableSet_event _ (measurableSet_singleton _)
Frontdoor 24 core · 15 supporting This file formalizes classical frontdoor identification for a binary treatment, finite mediator, and real outcome in the potential-outcome framework. ★ POFrontdoorSystem★ EofY_eq_frontdoorTerm★ ate_frontdoor
Frontdoor Average Treatment Effect
This file formalizes classical frontdoor identification for a binary treatment, finite mediator, and real outcome in the potential-outcome framework. It defines the frontdoor subsystem, assumptions, observable adjustment functional, and the proof equating that functional with the average treatment effect.
The proof uses event-conditional means, full mediation, two exchangeability assumptions, and composition consistency to relate the two-variable counterfactual outcome through the mediator to the single-treatment potential outcome.
structure POFrontdoorSystem reviewed
⚑ flagged
Causalean.PO
A frontdoor system packages, within an ambient potential-outcome system, a binary treatment A, a finite discrete mediator M valued in a finite type, and a real-valued outcome Y, where the treatment, mediator, and outcome are pairwise distinct variables.
Definition (Lean source)
parameters
P :
β :
fields
A :
P.V
M :
P.V
Y :
P.V
hAbool :
P.X A ≃ᵐ Bool
hMequiv :
P.X M ≃ᵐ β
hYreal :
P.X Y ≃ᵐ ℝ
hAM :
A ≠ M
hAY :
A ≠ Y
hMY :
M ≠ Y
def aVar reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The treatment node is packaged as a binary potential-outcome variable.
def mVar reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The mediator node is packaged as a potential-outcome variable with finite mediator values.
Definition (Lean source)
def mVar : POVar P β := ⟨S.M, S.hMequiv⟩
def yVar reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The outcome node is packaged as a real-valued potential-outcome variable.
Definition (Lean source)
def yVar : POVar P ℝ := ⟨S.Y, S.hYreal⟩
def YofA reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The treatment-arm potential outcome fixes treatment to the chosen arm.
Definition (Lean source)
noncomputable def YofA (a : Bool) : P.Ω → ℝ := S.yVar.cfUnder S.aVar a
def MofA reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The treatment-arm potential mediator fixes treatment to the chosen arm.
def regimeAM reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The joint treatment-mediator regime fixes treatment and mediator simultaneously.
def YofAM reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The two-variable potential outcome fixes both treatment and mediator.
def factualA reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The factual treatment is the observed treatment assignment for each unit.
Definition (Lean source)
noncomputable def factualA : P.Ω → Bool := S.aVar.factual
def factualM reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The factual mediator is the observed mediator value for each unit.
Definition (Lean source)
noncomputable def factualM : P.Ω → β := S.mVar.factual
def factualY reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The factual outcome is the observed outcome for each unit.
Definition (Lean source)
noncomputable def factualY : P.Ω → ℝ := S.yVar.factual
def aEvent reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The event {A = a}.
def mEvent reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The event {M = m}.
def mUnderA reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
M(a) as a RegimedVar.
Definition (Lean source)
def mBundle reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
Bundle [M(true), M(false)], used to state A ⊥ (M(1), M(0)).
Definition (Lean source)
noncomputable def mBundle : POCFBundle P :=
POCFBundle.cons (S.mUnderA true) <|
POCFBundle.cons (S.mUnderA false) <|
POCFBundle.nil P
def pA reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
P(A = a).
def pMgivenA reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
P(M = m | A = a), event-conditional probability.
Definition (Lean source)
noncomputable def pMgivenA (m : β) (a : Bool) : ℝ :=
eventCondExp P.μ (S.aEvent a) (S.mVar.indicator m)
def EYgivenAM reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
E[Y | A = a, M = m].
Definition (Lean source)
noncomputable def EYgivenAM (a : Bool) (m : β) : ℝ :=
eventCondExp P.μ (S.aEvent a ∩ S.mEvent m) S.factualY
def frontdoorTerm reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
The frontdoor-adjusted functional φ(a) at treatment a:
def ATE reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
Target parameter E[Y(1) - Y(0)].
def frontdoorATE reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
Observable (frontdoor-adjusted) ATE.
structure Assumptions reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
Frontdoor identifying assumptions. Bundles, for a frontdoor system, consistency of the underlying potential-outcome system, the full-mediation exclusion restriction that the two-treatment-and-mediator outcome does not depend on the treatment arm, treatment–mediator exchangeability, mediator–outcome exchangeability within treatment arms, positivity of each treatment arm, positivity of the mediator within the support of its counterfactual under a treatment arm, cross-world independence of the counterfactual mediator from the full-mediation outcome, and integrability of the treatment-arm and joint treatment–mediator potential outcomes.
Definition (Lean source)
parameters
S :
fields
Consistency axiom for the ambient PO system.
consistency :
P.Consistency
**Full mediation / exclusion restriction:** `Y(a,m) = Y(a',m)` a.s. for all
`a, a' ∈ {0,1}` and `m ∈ β`.
fullMediation :
∀ (a a' : Bool) (m : β), S.YofAM a m =ᵐ[P.μ] S.YofAM a' m
**Treatment–mediator exchangeability:** `A ⊥ (M(1), M(0))`. Equivalent
(for binary `A`) to `M(a) ⊥ A` for each `a`.
exch_AM :
P.IndepCF (RegimedVar.ofFactual S.aVar) S.mBundle P.μ
**Mediator–outcome exchangeability within treatment arms:** for mediator
values in the support of `M(a)`, and each treatment arm `a'`, the conditional
law of `Y(m)` (= any `Y(a,m)` by full mediation) on `{A = a'} ∩ {M = m}`
equals its conditional law on `{A = a'}`. Stated at the `eventCondExp` level
(discrete form, matching Manski/LATE style), and gated by positive `M(a)` mass
so zero-probability mediator cells need no exchangeability assumption.
exch_MY :
∀ (a : Bool) (m : β)
if
0 < P.μ ({ω | S.MofA a ω = m})
then
∀ a' : Bool,
eventCondExp P.μ (S.aEvent a' ∩ S.mEvent m) (S.YofAM true m)
= eventCondExp P.μ (S.aEvent a') (S.YofAM true m)
**Positivity (treatment):** `P(A = a) > 0`.
posA :
∀ a : Bool, 0 < P.μ (S.aEvent a)
**Positivity (mediator within support of `M(a)`):** if `P(M(a) = m) > 0`,
then for every treatment arm `a'` we have `P(A=a', M=m) > 0`. Stated on the
`ENNReal`-valued measure for convenience.
posAM :
**Joint mediator–outcome independence across worlds:** `M(a) ⊥ Y(1, m)`
as `IndepFun`. This is required for the drop-of-conditioning step
E[Y(m) · 1_{M(a)=m}] = E[Y(m)] · P(M(a) = m)
used in the frontdoor proof sketch. It is not
derivable from the other four assumptions in the bare PO framework: under a
graphical frontdoor DAG it would follow from d-separation (no directed path
from the counterfactual mediator `M(a)` to the full-mediation outcome
`Y(1, m)`), but in the bare PO setting it must be stated explicitly.
Cross-world independence `M(a) ⟂ Y(1, m)`. In Pearl's graphical frontdoor
this follows from d-separation; here we state it directly as a primitive
PO assumption. A future graphical-derivation file under `SCM/ID/` could
derive this from the three Pearl frontdoor graph conditions via the
SWIG/d-separation infrastructure in `Causalean/Graph/`.
Integrability of each `Y(a)`.
integrable_YofA :
∀ a : Bool, Integrable (S.YofA a) P.μ
Integrability of each `Y(a,m)`.
integrable_YofAM :
∀ (a : Bool) (m : β), Integrable (S.YofAM a m) P.μ
theorem EofY_eq_frontdoorTerm reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
Frontdoor identification (individual regime). Under the frontdoor identifying assumption bundle, for each treatment arm a, the mean potential outcome under arm a equals the frontdoor functional frontdoorTerm(a), built from the mediator distribution given a and the outcome regression on mediator and treatment.
Formal statement
Proof (Lean source)
theorem EofY_eq_frontdoorTerm (hA : S.Assumptions) (a : Bool) :
∫ ω, S.YofA a ω ∂P.μ = S.frontdoorTerm a := by
-- Shorthands.
set mSet : β → Set P.Ω := fun m => {ω | S.MofA a ω = m} with hmSet_def
have hmSet_meas : ∀ m, MeasurableSet (mSet m) := fun m =>
S.measurable_MofA a (MeasurableSet.singleton m)
have hpA_ne_top : P.μ (S.aEvent a) ≠ ⊤ := measure_ne_top _ _
have hpA_ne_zero : P.μ (S.aEvent a) ≠ 0 := (hA.posA a).ne'
have hpA_toReal_pos : 0 < (P.μ (S.aEvent a)).toReal := by
rw [ENNReal.toReal_pos_iff]; exact ⟨hA.posA a, lt_top_iff_ne_top.mpr hpA_ne_top⟩
have hpA_toReal_ne_zero : (P.μ (S.aEvent a)).toReal ≠ 0 := hpA_toReal_pos.ne'
-- ───────────────────────────────────────────────────────────────────────────
-- (A) Mediator-marginal identity: μ(mSet m).toReal = pMgivenA m a.
-- ───────────────────────────────────────────────────────────────────────────
-- (A.1) Independence: factualA ⊥ MofA a (from exch_AM component projection).
have hInd_AMa : IndepFun S.factualA (S.MofA a) P.μ := by
cases a with
| true => exact hA.exch_AM.component (0 : Fin 2)
| false => exact hA.exch_AM.component (1 : Fin 2)
-- (A.2) Independence on preimage sets: μ(aEvent a ∩ mSet m) = μ(aEvent a) * μ(mSet m).
have hIndepMeas : ∀ m,
P.μ (S.aEvent a ∩ mSet m) = P.μ (S.aEvent a) * P.μ (mSet m) := by
intro m
have h := hInd_AMa.measure_inter_preimage_eq_mul
(s := {a}) (t := {m}) (measurableSet_singleton _) (measurableSet_singleton _)
-- `aEvent a = factualA ⁻¹' {a}` and `mSet m = MofA a ⁻¹' {m}` both by rfl.
exact h
-- (A.3) Consistency set identity: aEvent a ∩ mSet m = aEvent a ∩ mEvent m.
have hConsist_set :
∀ m, S.aEvent a ∩ mSet m = S.aEvent a ∩ S.mEvent m := by
intro m
ext ω
refine ⟨?_, ?_⟩
· rintro ⟨hA_ω, hMofA_ω⟩
refine ⟨hA_ω, ?_⟩
have h_eq := MofA_eq_factualM_on_aEvent hA.consistency a hA_ω
change S.factualM ω = m
rw [← h_eq]; exact hMofA_ω
· rintro ⟨hA_ω, hM_ω⟩
refine ⟨hA_ω, ?_⟩
have h_eq := MofA_eq_factualM_on_aEvent hA.consistency a hA_ω
change S.MofA a ω = m
rw [h_eq]; exact hM_ω
-- (A.4) indM m equals set indicator of mEvent m.
have hIndM : ∀ m, S.mVar.indicator m = (S.mEvent m).indicator (fun _ => (1:ℝ)) :=
fun m => S.mVar.indicator_eq_event_indicator m
-- (A.5) Evaluate pMgivenA m a in closed form.
have hpM_val : ∀ m,
S.pMgivenA m a =
(P.μ (S.aEvent a ∩ S.mEvent m)).toReal / (P.μ (S.aEvent a)).toReal := by
intro m
unfold pMgivenA eventCondExp
rw [hIndM]
rw [MeasureTheory.setIntegral_indicator (S.measurableSet_mEvent m)]
rw [MeasureTheory.setIntegral_one_eq_measureReal]
rfl
-- (A.6) Mediator-marginal identity.
have hMarginal : ∀ m, (P.μ (mSet m)).toReal = S.pMgivenA m a := by
intro m
rw [hpM_val m]
have h₁ : (P.μ (S.aEvent a ∩ mSet m)).toReal
= (P.μ (S.aEvent a)).toReal * (P.μ (mSet m)).toReal := by
rw [hIndepMeas m]
exact ENNReal.toReal_mul
have h₂ : (P.μ (S.aEvent a ∩ S.mEvent m)).toReal
= (P.μ (S.aEvent a)).toReal * (P.μ (mSet m)).toReal := by
rw [← hConsist_set m]; exact h₁
rw [h₂]
field_simp
-- ───────────────────────────────────────────────────────────────────────────
-- (D) Inner integral: ∫ YofAM true m = ∑ a', EYgivenAM a' m · pA a'.
-- ───────────────────────────────────────────────────────────────────────────
have hInner : ∀ m : β, 0 < P.μ (mSet m) →
∫ ω, S.YofAM true m ω ∂P.μ
= ∑ a' : Bool, S.EYgivenAM a' m * S.pA a' := by
intro m hm_pos
-- Tower over Bool partition by A.
rw [integral_eq_sum_eventCondExp_aEvent (S := S) _ (hA.integrable_YofAM true m)]
refine Finset.sum_congr rfl (fun a' _ => ?_)
-- Use exch_MY to pass to aEvent a' ∩ mEvent m.
rw [← hA.exch_MY a m hm_pos a']
-- Inside the event aEvent a' ∩ mEvent m, YofAM true m = factualY a.e.
-- First, full mediation: YofAM true m =ᵐ[μ] YofAM a' m.
-- Then, consistency on aEvent a' ∩ mEvent m: YofAM a' m = factualY.
have hYeq : ∀ ω ∈ S.aEvent a' ∩ S.mEvent m,
S.YofAM a' m ω = S.factualY ω :=
fun ω hω => YofAM_eq_factualY_on_aMEvent hA.consistency a' m hω
-- eventCondExp (aEvent a' ∩ mEvent m) (YofAM true m)
-- = eventCondExp (aEvent a' ∩ mEvent m) (YofAM a' m) [full mediation a.e.]
-- = eventCondExp (aEvent a' ∩ mEvent m) factualY [consistency on event]
have hcongr_ae :
eventCondExp P.μ (S.aEvent a' ∩ S.mEvent m) (S.YofAM true m)
= eventCondExp P.μ (S.aEvent a' ∩ S.mEvent m) (S.YofAM a' m) := by
unfold eventCondExp
congr 1
refine MeasureTheory.integral_congr_ae ?_
exact (Filter.EventuallyEq.filter_mono (hA.fullMediation true a' m)
MeasureTheory.ae_restrict_le)
have hcongr_event :
eventCondExp P.μ (S.aEvent a' ∩ S.mEvent m) (S.YofAM a' m)
= eventCondExp P.μ (S.aEvent a' ∩ S.mEvent m) S.factualY := by
unfold eventCondExp
congr 1
refine MeasureTheory.setIntegral_congr_fun
((S.measurableSet_aEvent a').inter (S.measurableSet_mEvent m)) ?_
exact hYeq
rw [hcongr_ae, hcongr_event]
-- Now the goal is EYgivenAM a' m * pA a' = eventCondExp ... factualY * μ(aEvent a').toReal.
unfold EYgivenAM pA
ring
-- ───────────────────────────────────────────────────────────────────────────
-- (B,C) ∫ YofA a = ∑ m, (∫ YofAM true m) · μ(mSet m).toReal.
-- Uses composition + full mediation on the slice {MofA a = m}, and drop of
-- conditioning from exch_AM.
-- ───────────────────────────────────────────────────────────────────────────
have hOuter : ∀ m : β,
∫ ω in mSet m, S.YofA a ω ∂P.μ
= (P.μ (mSet m)).toReal * ∫ ω, S.YofAM true m ω ∂P.μ := by
intro m
-- Step (B): on mSet m, YofA a = YofAM a m (composition), and
-- YofAM a m =ᵐ YofAM true m (full mediation), so on mSet m,
-- YofA a = YofAM true m a.e. (viewing full mediation as an a.e. equality
-- of the full functions, which restricts to mSet m).
have hB : ∫ ω in mSet m, S.YofA a ω ∂P.μ
= ∫ ω in mSet m, S.YofAM true m ω ∂P.μ := by
-- Use a.e. equality on mSet m: YofA a =ᵐ[μ.restrict (mSet m)] YofAM true m.
refine MeasureTheory.integral_congr_ae ?_
-- On mSet m (a pointwise event): YofA a = YofAM a m.
-- Off mSet m we need nothing, but we produce a restrict-a.e. statement via
-- indicator/filter reasoning. Simplest: combine pointwise composition
-- identity (on mSet m) with a.e. full mediation, restricted.
have h_comp_on : ∀ ω ∈ mSet m, S.YofA a ω = S.YofAM a m ω := by
intro ω hω
exact (YofAM_eq_YofA_on_MofA_event hA.consistency a m hω).symm
-- YofAM a m =ᵐ[μ] YofAM true m.
have h_fm := (hA.fullMediation a true m).symm -- YofAM true m =ᵐ YofAM a m
-- Combine: for almost every ω in mSet m, YofA a ω = YofAM true m ω.
have h_fm_restrict : S.YofAM a m =ᵐ[P.μ.restrict (mSet m)] S.YofAM true m := by
exact (hA.fullMediation a true m).filter_mono MeasureTheory.ae_restrict_le
-- YofA a =ᵐ[restrict] YofAM a m (pointwise on mSet m ⇒ a.e. on restrict).
have h_comp_ae :
S.YofA a =ᵐ[P.μ.restrict (mSet m)] S.YofAM a m := by
rw [EventuallyEq, MeasureTheory.ae_restrict_iff' (hmSet_meas m)]
filter_upwards with ω hω using h_comp_on ω hω
exact h_comp_ae.trans h_fm_restrict
rw [hB]
-- Step (C): drop-of-conditioning for YofAM true m using indep_Y_M.
-- mSet m = (MofA a) ⁻¹' {m}, so IndepFun gives the preimage integral identity.
have hdrop :
∫ ω in (S.MofA a) ⁻¹' {m}, id (S.YofAM true m ω) ∂P.μ
= (P.μ ((S.MofA a) ⁻¹' {m})).toReal
* ∫ ω, id (S.YofAM true m ω) ∂P.μ :=
(hA.indep_Y_M a m).integral_restrict_preimage_eq_mul
(S.measurable_MofA a).aemeasurable (S.measurable_YofAM true m).aemeasurable
(measurableSet_singleton m) ((S.measurable_MofA a) (measurableSet_singleton m))
measurable_id.aestronglyMeasurable
have hpre : mSet m = (S.MofA a) ⁻¹' {m} := rfl
rw [hpre]
exact hdrop
-- ───────────────────────────────────────────────────────────────────────────
-- Main chain: combine (i) partition, (B,C) drop + marginal, (D) inner.
-- ───────────────────────────────────────────────────────────────────────────
rw [integral_eq_sum_integral_MofA (S := S) _ (hA.integrable_YofA a) a]
-- Now the goal is ∑ m, ∫ in {MofA a = m}, YofA a = frontdoorTerm a.
-- Rewrite the LHS sum using hOuter, hMarginal, hInner.
have hStep : ∀ m : β,
∫ ω in mSet m, S.YofA a ω ∂P.μ
= S.pMgivenA m a * ∑ a' : Bool, S.EYgivenAM a' m * S.pA a' := by
intro m
by_cases hm_pos : 0 < P.μ (mSet m)
· rw [hOuter m, hInner m hm_pos, hMarginal m]
· have hm_zero : P.μ (mSet m) = 0 := le_antisymm (not_lt.mp hm_pos) bot_le
rw [hOuter m, ← hMarginal m, hm_zero]
simp
have hLHS :
∑ m : β, ∫ ω in mSet m, S.YofA a ω ∂P.μ
= ∑ m : β, S.pMgivenA m a * ∑ a' : Bool, S.EYgivenAM a' m * S.pA a' :=
Finset.sum_congr rfl (fun m _ => hStep m)
rw [hLHS]
-- Remaining: ∑ m, pMgivenA m a * (∑ a', EYgivenAM a' m * pA a') = frontdoorTerm a.
unfold frontdoorTerm
refine Finset.sum_congr rfl (fun m _ => ?_)
-- pMgivenA m a * (EYgivenAM true m * pA true + EYgivenAM false m * pA false)
-- = (EYgivenAM true m * pA true + EYgivenAM false m * pA false) * pMgivenA m a.
rw [Fintype.sum_bool]
ring
theorem ate_frontdoor reviewed
⚑ flagged
Causalean.PO.POFrontdoorSystem
Frontdoor identification of the ATE. Under the frontdoor identifying assumption bundle, the average treatment effect equals the frontdoor estimand frontdoorATE, the difference of the frontdoor functional evaluated at the two treatment arms.
Formal statement
hypotheses
hA :
S.Assumptions
conclusion
S.ATE = S.frontdoorATE
Proof (Lean source)
theorem ate_frontdoor (hA : S.Assumptions) : S.ATE = S.frontdoorATE := by
unfold ATE frontdoorATE
rw [integral_sub (hA.integrable_YofA true) (hA.integrable_YofA false)]
rw [EofY_eq_frontdoorTerm S hA true, EofY_eq_frontdoorTerm S hA false]
15 supporting declarations (lemmas, instances)
-
measurable_YofAlemma — Treatment-arm potential outcomes are measurable.Proof (Lean source)
lemma measurable_YofA (a : Bool) : Measurable (S.YofA a) := S.yVar.measurable_cfUnder S.aVar a -
measurable_MofAlemma — Treatment-arm potential mediators are measurable.Proof (Lean source)
-
measurable_YofAMlemma — Joint treatment-mediator potential outcomes are measurable.Proof (Lean source)
-
measurable_factualAlemma — The observed treatment is measurable.conclusionMeasurable S.factualAProof (Lean source)
lemma measurable_factualA : Measurable S.factualA := S.aVar.measurable_factual -
measurable_factualMlemma — The observed mediator is measurable.conclusionMeasurable S.factualMProof (Lean source)
lemma measurable_factualM : Measurable S.factualM := S.mVar.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_aEventlemma — The factual treatment event for a treatment arm is measurable.Proof (Lean source)
lemma measurableSet_aEvent (a : Bool) : MeasurableSet (S.aEvent a) := S.aVar.measurableSet_event _ (measurableSet_singleton _) -
measurableSet_mEventlemma — The factual mediator event for a mediator value is measurable.Proof (Lean source)
lemma measurableSet_mEvent (m : β) : MeasurableSet (S.mEvent m) := S.mVar.measurableSet_event _ (measurableSet_singleton _) -
MofA_eq_factualM_on_aEventlemma — On the event {A = a}, M(a)(ω) = factualM ω. Single-target consistency.hypothesesconclusionS.MofA a ω = S.factualM ωProof (Lean source)
lemma MofA_eq_factualM_on_aEvent (hC : P.Consistency) (a : Bool) {ω : P.Ω} (hω : ω ∈ S.aEvent a) : S.MofA a ω = S.factualM ω := POVar.cf_eq_factual_on_event hC S.mVar S.aVar a (Ne.symm S.hAM) hω -
YofAM_eq_factualY_on_aMEventlemma — On the event {A = a} ∩ {M = m}, Y(a,m)(ω) = factualY ω. Multi-target consistency via cf_eq_factual_of_factualAgrees.hypothesesconclusionS.YofAM a m ω = S.factualY ωProof (Lean source)
lemma YofAM_eq_factualY_on_aMEvent (hC : P.Consistency) (a : Bool) (m : β) {ω : P.Ω} (hω : ω ∈ S.aEvent a ∩ S.mEvent m) : S.YofAM a m ω = S.factualY ω := by -- The target set of `regimeAM a m` is `{A, M}`; `Y ∉ {A, M}` since `hAY, hMY`. have h_notmem : S.yVar.v ∉ (S.regimeAM a m).target := by simp only [regimeAM, Regime.sqcup_target, Regime.single_target, Finset.singleton_union, yVar, Finset.mem_insert, mem_singleton, not_or] exact ⟨S.hAY.symm, S.hMY.symm⟩ -- On `{A=a} ∩ {M=m}`, `ω` factually agrees with `regimeAM a m`, by combining -- the per-variable factual equalities `aVar.factual ω = a`, `mVar.factual ω = m`. have hAgrees : P.FactualAgrees (S.regimeAM a m) ω := POSystem.factualAgrees_sqcup _ (S.aVar.factualAgrees_single a hω.1) (S.mVar.factualAgrees_single m hω.2) exact POVar.cf_eq_factual_of_factualAgrees hC S.yVar (S.regimeAM a m) h_notmem ω hAgrees -
integrable_factualY_of_consistency_integrable_YofAMlemma — The observed outcome is integrable when all joint treatment-mediator potential outcomes are integrable and consistency holds.hypotheseshC :P.ConsistencyhY :∀ (a : Bool) (m : β), Integrable (S.YofAM a m) P.μconclusionIntegrable S.factualY P.μProof (Lean source)
lemma integrable_factualY_of_consistency_integrable_YofAM (hC : P.Consistency) (hY : ∀ (a : Bool) (m : β), Integrable (S.YofAM a m) P.μ) : Integrable S.factualY P.μ := by let cell : Bool → β → P.Ω → ℝ := fun a m ω => S.YofAM a m ω * S.aVar.indicator a ω * S.mVar.indicator m ω have hcell_int : ∀ a m, Integrable (cell a m) P.μ := by intro a m have hA_int : Integrable (fun ω => S.YofAM a m ω * S.aVar.indicator a ω) P.μ := S.aVar.integrable_mul_indicator a (measurableSet_singleton a) (hY a m) simpa [cell, mul_assoc] using S.mVar.integrable_mul_indicator m (measurableSet_singleton m) hA_int have hsum_int : Integrable (fun ω => ∑ a : Bool, ∑ m : β, cell a m ω) P.μ := by have hsum_beta : ∀ a, Integrable (fun ω => ∑ m : β, cell a m ω) P.μ := by intro a have hsum_finset : ∀ s : Finset β, Integrable (fun ω => s.sum fun m => cell a m ω) P.μ := by intro s refine Finset.induction_on s ?base ?step · simp · intro m s hms hs simp only [Finset.sum_insert hms] exact (hcell_int a m).add hs simpa using hsum_finset Finset.univ have htrue : Integrable (fun ω => ∑ m : β, cell true m ω) P.μ := hsum_beta true have hfalse : Integrable (fun ω => ∑ m : β, cell false m ω) P.μ := hsum_beta false simp only [Fintype.sum_bool] exact htrue.add hfalse refine hsum_int.congr (Filter.Eventually.of_forall ?_) intro ω have hA_indicator : ∀ a, S.aVar.indicator a ω = if S.factualA ω = a then 1 else 0 := by intro a by_cases hωa : S.factualA ω = a · simp [S.aVar.indicator_apply_eq_one hωa, hωa] · simp [S.aVar.indicator_apply_eq_zero hωa, hωa] have hM_indicator : ∀ m, S.mVar.indicator m ω = if S.factualM ω = m then 1 else 0 := by intro m by_cases hωm : S.factualM ω = m · simp [S.mVar.indicator_apply_eq_one hωm, hωm] · simp [S.mVar.indicator_apply_eq_zero hωm, hωm] change (∑ a : Bool, ∑ m : β, cell a m ω) = S.factualY ω rw [Fintype.sum_bool] cases hAω : S.factualA ω · simp only [hA_indicator, hAω, Bool.false_eq_true, ↓reduceIte, mul_zero, hM_indicator, mul_ite, mul_one, ite_self, Finset.sum_const_zero, Finset.sum_ite_eq, Finset.mem_univ, zero_add, cell] exact YofAM_eq_factualY_on_aMEvent hC false (S.factualM ω) (show ω ∈ S.aEvent false ∩ S.mEvent (S.factualM ω) from ⟨hAω, rfl⟩) · simp only [hA_indicator, hAω, ↓reduceIte, mul_one, hM_indicator, mul_ite, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, Bool.true_eq_false, ite_self, Finset.sum_const_zero, add_zero, cell] exact YofAM_eq_factualY_on_aMEvent hC true (S.factualM ω) (show ω ∈ S.aEvent true ∩ S.mEvent (S.factualM ω) from ⟨hAω, rfl⟩) -
integrable_factualYlemma — Compatibility projection for older call sites: factual outcome integrability is derived from consistency plus integrability of the finite Y(a,m) cells.Proof (Lean source)
lemma integrable_factualY (hA : S.Assumptions) : Integrable S.factualY P.μ := S.integrable_factualY_of_consistency_integrable_YofAM hA.consistency hA.integrable_YofAM -
YofAM_eq_YofA_on_MofA_eventlemma — Composition lemma (def:po-consistency, composition clause): on the event {M(a) = m}, Y(a, m)(ω) = Y(a)(ω).hypothesesconclusionS.YofAM a m ω = S.YofA a ωProof (Lean source)
lemma YofAM_eq_YofA_on_MofA_event (hC : P.Consistency) (a : Bool) (m : β) {ω : P.Ω} (hω : S.MofA a ω = m) : S.YofAM a m ω = S.YofA a ω := by -- Disjointness of the two single-target regimes. have hdisj : (Regime.single S.A (S.hAbool.symm a)).Disjoint (Regime.single S.M (S.hMequiv.symm m)) := Regime.single_disjoint_single S.hAM _ _ -- `Y ∉ {A} ∪ {M}`. have hY_notmem : _root_.Disjoint ({S.Y} : Finset P.V) ((Regime.single S.A (S.hAbool.symm a)).target ∪ (Regime.single S.M (S.hMequiv.symm m)).target) := by simp only [Regime.single_target, Finset.singleton_union, Finset.disjoint_singleton_left, Finset.mem_insert, mem_singleton, not_or] exact ⟨fun h => S.hAY h.symm, fun h => S.hMY h.symm⟩ -- `IntermediateAgrees`: under `{A ← a}`, `M` evaluates to `hMequiv.symm m`. have hInter : P.IntermediateAgrees (Regime.single S.A (S.hAbool.symm a)) (Regime.single S.M (S.hMequiv.symm m)) ω := by intro v hv have hvM : v = S.M := Finset.mem_singleton.mp hv subst hvM -- `MofA a ω = m` ⇒ `hMequiv (P.eval r₁ ω M) = m` ⇒ `P.eval r₁ ω M = hMequiv.symm m`. have hM : S.hMequiv (P.eval (Regime.single S.A (S.hAbool.symm a)) ω S.M) = m := hω change P.eval (Regime.single S.A (S.hAbool.symm a)) ω S.M = S.hMequiv.symm m exact S.hMequiv.eq_symm_apply.mpr hM -- Apply `hC.composition`. have hComp := hC.composition (Regime.single S.A (S.hAbool.symm a)) (Regime.single S.M (S.hMequiv.symm m)) hdisj {S.Y} hY_notmem ω hInter -- Extract the `Y`-coordinate. have hYcoord : P.eval (Regime.single S.A (S.hAbool.symm a) |>.sqcup (Regime.single S.M (S.hMequiv.symm m)) hdisj) ω S.Y = P.eval (Regime.single S.A (S.hAbool.symm a)) ω S.Y := by simpa [POSystem.poVariable] using congrFun hComp ⟨S.Y, mem_singleton_self S.Y⟩ -- Push through `yVar.equiv`. change S.yVar.equiv (P.eval _ ω S.Y) = S.yVar.equiv (P.eval _ ω S.Y) exact congrArg S.yVar.equiv hYcoord -
integral_eq_sum_integral_MofAlemma — Partition of ∫ f along fibers of MofA a (finite codomain β).hypothesesconclusion∫ ω, f ω ∂P.μ = ∑ m : β, ∫ ω in {ω' | S.MofA a ω' = m}, f ω ∂P.μProof (Lean source)
lemma integral_eq_sum_integral_MofA (f : P.Ω → ℝ) (hf : Integrable f P.μ) (a : Bool) : ∫ ω, f ω ∂P.μ = ∑ m : β, ∫ ω in {ω' | S.MofA a ω' = m}, f ω ∂P.μ := by -- Sets `{ω | MofA a ω = m}` for `m : β` are the fibers of `MofA a`. set s : β → Set P.Ω := fun m => {ω | S.MofA a ω = m} with hs have hmeas : ∀ m, MeasurableSet (s m) := fun m => S.measurable_MofA a (MeasurableSet.singleton m) have hdisj : Pairwise (onFun Disjoint s) := by intro m₁ m₂ hne refine Set.disjoint_left.mpr ?_ intro ω hω₁ hω₂ apply hne simp only [Set.mem_setOf_eq, s] at hω₁ hω₂ exact hω₁ ▸ hω₂ have hcov : ⋃ m, s m = univ := by refine Set.eq_univ_of_forall (fun ω => ?_) exact Set.mem_iUnion.mpr ⟨S.MofA a ω, rfl⟩ have hintOn : ∀ m, IntegrableOn f (s m) P.μ := fun m => hf.integrableOn have hsplit : ∫ ω in ⋃ m, s m, f ω ∂P.μ = ∑ m : β, ∫ ω in s m, f ω ∂P.μ := MeasureTheory.integral_iUnion_fintype hmeas hdisj hintOn rw [← setIntegral_univ, ← hcov, hsplit] -
integral_eq_sum_eventCondExp_aEventlemma — Bool-partition tower identity for eventCondExp.hypothesesg :P.Ω → ℝhg :Integrable g P.μconclusion∫ ω, g ω ∂P.μ = ∑ a' : Bool, eventCondExp P.μ (S.aEvent a') g * (P.μ (S.aEvent a')).toRealProof (Lean source)
lemma integral_eq_sum_eventCondExp_aEvent (g : P.Ω → ℝ) (hg : Integrable g P.μ) : ∫ ω, g ω ∂P.μ = ∑ a' : Bool, eventCondExp P.μ (S.aEvent a') g * (P.μ (S.aEvent a')).toReal := by -- Rewrite each RHS term as a set integral. have hterm : ∀ a' : Bool, eventCondExp P.μ (S.aEvent a') g * (P.μ (S.aEvent a')).toReal = ∫ ω in S.aEvent a', g ω ∂P.μ := by intro a' unfold eventCondExp by_cases h0 : (P.μ (S.aEvent a')).toReal = 0 · -- Both sides are 0. rw [h0, mul_zero] have hμ0 : P.μ (S.aEvent a') = 0 := by rcases (ENNReal.toReal_eq_zero_iff _).mp h0 with h | h · exact h · exact absurd h (measure_ne_top _ _) exact (MeasureTheory.setIntegral_measure_zero g hμ0).symm · field_simp -- Swap the sum to set-integrals. have hsum : ∑ a' : Bool, eventCondExp P.μ (S.aEvent a') g * (P.μ (S.aEvent a')).toReal = ∑ a' : Bool, ∫ ω in S.aEvent a', g ω ∂P.μ := by exact Finset.sum_congr rfl (fun a' _ => hterm a') rw [hsum] -- Now prove `∫ g = ∑ a', ∫ in aEvent a', g`. have hmeas : ∀ a' : Bool, MeasurableSet (S.aEvent a') := S.measurableSet_aEvent have hdisj : Pairwise (onFun Disjoint (fun a' : Bool => S.aEvent a')) := by intro a₁ a₂ hne refine Set.disjoint_left.mpr ?_ intro ω hω₁ hω₂ apply hne show a₁ = a₂ have h1 : S.factualA ω = a₁ := hω₁ have h2 : S.factualA ω = a₂ := hω₂ exact h1.symm.trans h2 have hcov : ⋃ a' : Bool, S.aEvent a' = univ := by refine Set.eq_univ_of_forall (fun ω => ?_) exact Set.mem_iUnion.mpr ⟨S.factualA ω, rfl⟩ have hintOn : ∀ a' : Bool, IntegrableOn g (S.aEvent a') P.μ := fun _ => hg.integrableOn have hsplit : ∫ ω in ⋃ a' : Bool, S.aEvent a', g ω ∂P.μ = ∑ a' : Bool, ∫ ω in S.aEvent a', g ω ∂P.μ := MeasureTheory.integral_iUnion_fintype hmeas hdisj hintOn rw [← setIntegral_univ, ← hcov, hsplit]
LATE 22 core · 13 supporting This file formalizes the binary-instrument local average treatment effect in the potential-outcome framework. ★ POIVSystem★ late_wald
Instrumental Variables LATE
This file formalizes the binary-instrument local average treatment effect in
the potential-outcome framework. It defines the IV subsystem POIVSystem,
potential treatments DofZ, potential outcomes YofD, the complier event,
event-conditional observable means, the IV assumption bundle, and the target
LATE.
The proof surface decomposes the Wald argument into public identities:
first_stage_identity, reduced_form_identity, pointwise_monotonicity, and
event_conditioning_identity. The theorem late_wald assembles these pieces
to identify the observable Wald ratio with the complier average treatment
effect.
structure POIVSystem reviewed
⚑ flagged
Causalean.PO
A binary instrumental-variables subsystem (def:po-iv-system) records, within an ambient potential-outcome system, an instrument, a treatment, and an outcome, where the three nodes are required to be pairwise distinct.
def zVar reviewed
⚑ flagged
Causalean.PO.POIVSystem
Instrument packaged as a POVar valued in Bool.
def dVar reviewed
⚑ flagged
Causalean.PO.POIVSystem
Treatment packaged as a POVar valued in Bool.
def yVar reviewed
⚑ flagged
Causalean.PO.POIVSystem
Outcome packaged as a POVar valued in ℝ.
Definition (Lean source)
def yVar : POVar P ℝ := ⟨S.Y, S.hYreal⟩
def instrumentRegime reviewed
⚑ flagged
Causalean.PO.POIVSystem
Regime fixing instrument to z.
def treatmentRegime reviewed
⚑ flagged
Causalean.PO.POIVSystem
Regime fixing treatment to d.
def DofZ reviewed
⚑ flagged
Causalean.PO.POIVSystem
The potential treatment under an instrument value is the treatment that would be observed if the instrument were fixed to that value.
def YofD reviewed
⚑ flagged
Causalean.PO.POIVSystem
The potential outcome under a treatment value is the outcome that would be observed if treatment were fixed to that value.
Definition (Lean source)
noncomputable def YofD (d : Bool) : P.Ω → ℝ :=
S.yVar.cfUnder S.dVar d
def factualZ reviewed
⚑ flagged
Causalean.PO.POIVSystem
Factual instrument Z.
Definition (Lean source)
noncomputable def factualZ : P.Ω → Bool := S.zVar.factual
def factualD reviewed
⚑ flagged
Causalean.PO.POIVSystem
Factual treatment D.
Definition (Lean source)
noncomputable def factualD : P.Ω → Bool := S.dVar.factual
def factualY reviewed
⚑ flagged
Causalean.PO.POIVSystem
Factual outcome Y.
Definition (Lean source)
noncomputable def factualY : P.Ω → ℝ := S.yVar.factual
def complierEvent reviewed
⚑ flagged
Causalean.PO.POIVSystem
Complier event {ω | D(1)(ω) = 1 ∧ D(0)(ω) = 0} -- def:po-late.
def zEvent reviewed
⚑ flagged
Causalean.PO.POIVSystem
Set {ω | Z(ω) = z}.
def YofDofZ reviewed
⚑ flagged
Causalean.PO.POIVSystem
Y composed with D(z): 1_{D(z)=1} Y(1) + 1_{D(z)=0} Y(0).
def condExpDZ reviewed
⚑ flagged
Causalean.PO.POIVSystem
E[D | Z = z], the event-level conditional expectation of the (0/1-coded) factual treatment on {Z = z}. Uses the shared PO conditioning tool eventCondExp (definitionally (∫_A g)/μ(A)).
Definition (Lean source)
noncomputable def condExpDZ (z : Bool) : ℝ :=
eventCondExp P.μ (S.zEvent z) (fun ω => ((S.factualD ω).toNat : ℝ))
def condExpYZ reviewed
⚑ flagged
Causalean.PO.POIVSystem
E[Y | Z = z], the event-level conditional expectation of the factual outcome on {Z = z}, via the shared PO conditioning tool eventCondExp.
Definition (Lean source)
noncomputable def condExpYZ (z : Bool) : ℝ :=
eventCondExp P.μ (S.zEvent z) S.factualY
def dUnderZ reviewed
⚑ flagged
Causalean.PO.POIVSystem
Regimed variable for D(z) (treatment under instrument set to z).
Definition (Lean source)
def yUnderD reviewed
⚑ flagged
Causalean.PO.POIVSystem
Regimed variable for Y(d) (outcome under treatment set to d).
Definition (Lean source)
def yUnderD (d : Bool) : RegimedVar P ℝ :=
⟨S.yVar, Regime.single S.D (S.hDbool.symm d)⟩
def cfBundle reviewed
⚑ flagged
Causalean.PO.POIVSystem
Counterfactual bundle (D(1), D(0), Y(1), Y(0)).
Definition (Lean source)
noncomputable def cfBundle : POCFBundle P :=
POCFBundle.cons (S.dUnderZ true) <|
POCFBundle.cons (S.dUnderZ false) <|
POCFBundle.cons (S.yUnderD true) <|
POCFBundle.cons (S.yUnderD false) <|
POCFBundle.nil P
structure Assumptions reviewed
⚑ flagged
Causalean.PO.POIVSystem
Classical binary-instrument IV assumptions (def:po-iv-assumptions). Bundles consistency (SUTVA): the observed treatment and outcome equal the realized potential treatment and outcome, instrument exogeneity: the instrument is independent of the full counterfactual bundle of potential treatments and outcomes, monotonicity (no defiers): turning the instrument on never moves a unit out of treatment, and relevance: the complier event has positive probability.
Definition (Lean source)
parameters
S :
fields
Consistency (SUTVA): the observed `D`/`Y` equal the realized potential
treatment/outcome (`D = D(Z)`, `Y = Y(D)`). Links observed data to the
counterfactuals. (Exclusion — `Z` affects `Y` only through `D` — is built
into the `Y(d)` interface: outcomes carry no `z` argument, see the type
docstring above.)
consistency :
P.Consistency
Instrument independence (random/ignorable instrument): the instrument is
independent of the full counterfactual bundle, `Z ⟂ (D(1), D(0), Y(1), Y(0))`.
Phrased as independence of the factual instrument from the counterfactual
bundle. This is the IV exogeneity condition.
instrumentIndep :
P.IndepCF (RegimedVar.ofFactual S.zVar) S.cfBundle P.μ
Monotonicity (no defiers): turning the instrument on never moves a unit out
of treatment — `D(1) ≥ D(0)` a.s. On `Bool` this is `D(0)=1 → D(1)=1`. Rules
out defiers so the IV ratio identifies the complier effect.
Relevance (non-trivial first stage): the complier event `C = {D(1)=1, D(0)=0}`
has positive probability, so the instrument actually shifts treatment for a
positive mass of units (the LATE denominator is non-zero).
relevance :
0 < (P.μ S.complierEvent).toReal
def LATE reviewed
⚑ flagged
Causalean.PO.POIVSystem
Local Average Treatment Effect -- def:po-late.
Definition (Lean source)
noncomputable def LATE : ℝ :=
eventCondExp P.μ S.complierEvent (fun ω => S.YofD true ω - S.YofD false ω)
theorem late_wald reviewed
⚑ flagged
Causalean.PO.POIVSystem
Wald identification of LATE (prop:po-late). Under the binary- instrument LATE identifying assumption bundle, when the event {Z=1} has positive probability, the event {Z=0} has positive probability, and the potential outcomes under treatment and under control are integrable, the Wald ratio (E[Y|Z=1] − E[Y|Z=0]) / (E[D|Z=1] − E[D|Z=0]) equals the local average treatment effect LATE.
Formal statement
hypotheses
hA :
S.Assumptions
hZ1 :
0 < (P.μ (S.zEvent true)).toReal
hZ0 :
0 < (P.μ (S.zEvent false)).toReal
hY1 :
Integrable (S.YofD true) P.μ
hY0 :
Integrable (S.YofD false) P.μ
Proof (Lean source)
theorem late_wald (hA : S.Assumptions)
(hZ1 : 0 < (P.μ (S.zEvent true)).toReal)
(hZ0 : 0 < (P.μ (S.zEvent false)).toReal)
(hY1 : Integrable (S.YofD true) P.μ)
(hY0 : Integrable (S.YofD false) P.μ) :
(S.condExpYZ true - S.condExpYZ false) /
(S.condExpDZ true - S.condExpDZ false)
= S.LATE := by
rw [S.first_stage_identity hA hZ1 hZ0]
rw [S.reduced_form_identity hA hZ1 hZ0 hY1 hY0]
have heq : ∀ᵐ ω ∂P.μ, S.YofDofZ true ω - S.YofDofZ false ω
= (S.YofD true ω - S.YofD false ω) *
S.complierEvent.indicator (fun _ => (1:ℝ)) ω := S.pointwise_monotonicity hA
rw [MeasureTheory.integral_congr_ae heq]
rw [S.event_conditioning_identity]
have hC : (P.μ S.complierEvent).toReal ≠ 0 := ne_of_gt hA.relevance
field_simp
13 supporting declarations (lemmas, instances)
-
measurable_DofZlemma — The potential treatment under a fixed instrument value is measurable.Proof (Lean source)
lemma measurable_DofZ (z : Bool) : Measurable (S.DofZ z) := S.dVar.measurable_cfUnder S.zVar z -
measurable_factualZlemma — The factual instrument is measurable.conclusionMeasurable S.factualZProof (Lean source)
lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The factual treatment is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_YofDlemma — The potential outcome under a fixed treatment value is measurable.Proof (Lean source)
lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurableSet_complierEventlemma — The complier event is measurable.conclusionMeasurableSet S.complierEvent -
measurableSet_zEventlemma — The factual instrument event is measurable.Proof (Lean source)
lemma measurableSet_zEvent (z : Bool) : MeasurableSet (S.zEvent z) := S.zVar.measurableSet_event _ (measurableSet_singleton _) -
DofZ_eq_factualD_on_zEventlemma — On zEvent z, the counterfactual treatment D(z) equals the factual D. Pointwise specialization of Consistency.factual with r = instrumentRegime z, Y = {D}.hypothesesconclusionS.DofZ z ω = S.factualD ωProof (Lean source)
lemma DofZ_eq_factualD_on_zEvent (hA : S.Assumptions) (z : Bool) {ω : P.Ω} (hω : ω ∈ S.zEvent z) : S.DofZ z ω = S.factualD ω := POVar.cf_eq_factual_on_event hA.consistency S.dVar S.zVar z S.hZD.symm hω -
factualY_eq_YofD_factualDlemma — Factual Y equals the counterfactual Y(factualD ω). Pointwise specialization of Consistency.factual with r = treatmentRegime (factualD ω), Y = {Y}.hypotheseshA :S.Assumptionsω :P.ΩconclusionS.factualY ω = S.YofD (S.factualD ω) ωProof (Lean source)
lemma factualY_eq_YofD_factualD (hA : S.Assumptions) (ω : P.Ω) : S.factualY ω = S.YofD (S.factualD ω) ω := POVar.factual_eq_cfUnder_self_selected hA.consistency S.yVar S.dVar S.hDY.symm ω -
first_stage_identitytheorem — Step 1 of rem:po-late: first-stage identity. E[D | Z=1] - E[D | Z=0] = P(C).hypothesesProof (Lean source)
theorem first_stage_identity (hA : S.Assumptions) (hZ1 : 0 < (P.μ (S.zEvent true)).toReal) (hZ0 : 0 < (P.μ (S.zEvent false)).toReal) : S.condExpDZ true - S.condExpDZ false = (P.μ S.complierEvent).toReal := by -- Step 1: `condExpDZ z = ∫ (DofZ z ω).toNat ∂μ`. have hμne_zero : ∀ z, 0 < (P.μ (S.zEvent z)).toReal → P.μ (S.zVar.event z) ≠ 0 := fun z hZ h => absurd hZ (by simp [show S.zEvent z = S.zVar.event z from rfl, h]) have hμne_top : ∀ z, P.μ (S.zVar.event z) ≠ ⊤ := fun _ => measure_ne_top _ _ have hCE : ∀ z (_hZ : 0 < (P.μ (S.zEvent z)).toReal), S.condExpDZ z = ∫ ω, ((S.DofZ z ω).toNat : ℝ) ∂P.μ := by intro z hZ -- `h_proj` on the bundle `jointValue`: indices 0,1 are `D(1),D(0)`. let h_proj : (∀ i : Fin S.cfBundle.n, S.cfBundle.type i) → ℝ := fun f => ((cond z ((f (0 : Fin 4)) : Bool) ((f (1 : Fin 4)) : Bool)).toNat : ℝ) have hh_meas : Measurable h_proj := by let instCf : ∀ a : Fin 4, MeasurableSpace (S.cfBundle.type a) := fun a => S.cfBundle.inst a change Measurable fun f : ∀ i : Fin S.cfBundle.n, S.cfBundle.type i => ((cond z ((f (0 : Fin 4)) : Bool) ((f (1 : Fin 4)) : Bool)).toNat : ℝ) cases z · exact (by fun_prop : Measurable fun n : ℕ => (n : ℝ)).comp ((by fun_prop : Measurable Bool.toNat).comp (measurable_pi_apply (1 : Fin 4))) · exact (by fun_prop : Measurable fun n : ℕ => (n : ℝ)).comp ((by fun_prop : Measurable Bool.toNat).comp (measurable_pi_apply (0 : Fin 4))) have h_cons : ∀ ω ∈ S.zVar.event z, ((S.factualD ω).toNat : ℝ) = h_proj (S.cfBundle.jointValue ω) := by intro ω hω rw [← S.DofZ_eq_factualD_on_zEvent hA z hω] change ((S.DofZ z ω).toNat : ℝ) = ((cond z ((S.cfBundle.jointValue ω (0 : Fin 4)) : Bool) ((S.cfBundle.jointValue ω (1 : Fin 4)) : Bool)).toNat : ℝ) cases z <;> rfl have hbridge : S.condExpDZ z = eventCondExp P.μ (S.zVar.event z) (fun ω => ((S.factualD ω).toNat : ℝ)) := rfl rw [hbridge, POSystem.eventCondExp_of_consistency_IndepCF hA.instrumentIndep (a := S.zVar) hh_meas (measurableSet_singleton z) (ae_restrict_of_forall_mem (S.measurableSet_zEvent z) h_cons) (hμne_zero z hZ) (hμne_top z)] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω change ((cond z ((S.cfBundle.jointValue ω (0 : Fin 4)) : Bool) ((S.cfBundle.jointValue ω (1 : Fin 4)) : Bool)).toNat : ℝ) = ((S.DofZ z ω).toNat : ℝ) cases z <;> rfl rw [hCE true hZ1, hCE false hZ0] -- Step 2: fold the two integrals into `∫ ((DofZ true).toNat - (DofZ false).toNat) ∂μ`. have hDbdd : ∀ z, ∀ ω, |((S.DofZ z ω).toNat : ℝ)| ≤ 1 := fun z ω => by cases S.DofZ z ω <;> simp have hDint : ∀ z, Integrable (fun ω => ((S.DofZ z ω).toNat : ℝ)) P.μ := fun z => (MeasureTheory.integrable_const (1:ℝ)).mono' ((by fun_prop : Measurable (fun n : ℕ => (n : ℝ))).comp ((by fun_prop : Measurable Bool.toNat).comp (S.measurable_DofZ z)) |>.aestronglyMeasurable) (Filter.Eventually.of_forall (hDbdd z)) rw [← MeasureTheory.integral_sub (hDint true) (hDint false)] -- Step 3: under monotonicity, `(DofZ true).toNat - (DofZ false).toNat = 1_C a.s.`. have hInd : ∀ᵐ ω ∂P.μ, ((S.DofZ true ω).toNat : ℝ) - ((S.DofZ false ω).toNat : ℝ) = S.complierEvent.indicator (fun _ => (1:ℝ)) ω := by refine hA.monotonicity.mono (fun ω hω => ?_) by_cases h1 : S.DofZ true ω = true · by_cases h0 : S.DofZ false ω = true · have hnC : ω ∉ S.complierEvent := by intro ⟨_, h0'⟩; rw [h0] at h0'; exact Bool.noConfusion h0' simp [h1, h0, Set.indicator_of_notMem hnC] · have h0' : S.DofZ false ω = false := Bool.not_eq_true _ |>.mp h0 have hC : ω ∈ S.complierEvent := ⟨h1, h0'⟩ simp [h1, h0', Set.indicator_of_mem hC] · have h1' : S.DofZ true ω = false := Bool.not_eq_true _ |>.mp h1 by_cases h0 : S.DofZ false ω = true · exfalso; rw [hω h0] at h1'; exact Bool.noConfusion h1'.symm · have h0' : S.DofZ false ω = false := Bool.not_eq_true _ |>.mp h0 have hnC : ω ∉ S.complierEvent := by intro ⟨h1'', _⟩; rw [h1'] at h1''; exact Bool.false_ne_true h1'' simp [h1', h0', Set.indicator_of_notMem hnC] rw [MeasureTheory.integral_congr_ae hInd] rw [MeasureTheory.integral_indicator_const (1:ℝ) S.measurableSet_complierEvent] simp [MeasureTheory.measureReal_def] -
reduced_form_identitytheorem — Step 2 of rem:po-late: reduced-form identity. E[Y | Z=1] - E[Y | Z=0] = E[Y(D(1)) - Y(D(0))].hypotheseshA :S.AssumptionshZ1 :0 < (P.μ (S.zEvent true)).toRealhZ0 :0 < (P.μ (S.zEvent false)).toRealhY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μProof (Lean source)
theorem reduced_form_identity (hA : S.Assumptions) (hZ1 : 0 < (P.μ (S.zEvent true)).toReal) (hZ0 : 0 < (P.μ (S.zEvent false)).toReal) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) : S.condExpYZ true - S.condExpYZ false = ∫ ω, (S.YofDofZ true ω - S.YofDofZ false ω) ∂P.μ := by -- Measurability and integrability of `YofDofZ z`. have hYDZ_meas : ∀ z, Measurable (S.YofDofZ z) := fun z => by unfold YofDofZ exact Measurable.ite (S.measurable_DofZ z (MeasurableSet.singleton true)) (S.measurable_YofD true) (S.measurable_YofD false) have hYDZ_bdd : ∀ z, ∀ ω, |S.YofDofZ z ω| ≤ |S.YofD true ω| + |S.YofD false ω| := fun z ω => by have h1 := abs_nonneg (S.YofD true ω) have h0 := abs_nonneg (S.YofD false ω) unfold YofDofZ; cases S.DofZ z ω <;> simp [h1, h0] have hYDZ_int : ∀ z, Integrable (S.YofDofZ z) P.μ := fun z => (hY1.norm.add hY0.norm).mono' (hYDZ_meas z).aestronglyMeasurable (Filter.Eventually.of_forall (hYDZ_bdd z)) -- Step 1: `condExpYZ z = ∫ YofDofZ z ω ∂μ`. have hμne_zero : ∀ z, 0 < (P.μ (S.zEvent z)).toReal → P.μ (S.zVar.event z) ≠ 0 := fun z hZ h => absurd hZ (by simp [show S.zEvent z = S.zVar.event z from rfl, h]) have hμne_top : ∀ z, P.μ (S.zVar.event z) ≠ ⊤ := fun _ => measure_ne_top _ _ have hCE : ∀ z (_hZ : 0 < (P.μ (S.zEvent z)).toReal), S.condExpYZ z = ∫ ω, S.YofDofZ z ω ∂P.μ := by intro z hZ -- `h_proj` on the bundle: indices 0,1 are `D(1),D(0)`; 2,3 are `Y(1),Y(0)`. let h_proj : (∀ i : Fin S.cfBundle.n, S.cfBundle.type i) → ℝ := fun f => if ((cond z ((f (0 : Fin 4)) : Bool) ((f (1 : Fin 4)) : Bool)) : Bool) then ((f (2 : Fin 4)) : ℝ) else ((f (3 : Fin 4)) : ℝ) have hh_meas : Measurable h_proj := by let instCf : ∀ a : Fin 4, MeasurableSpace (S.cfBundle.type a) := fun a => S.cfBundle.inst a change Measurable fun f : ∀ i : Fin S.cfBundle.n, S.cfBundle.type i => if ((cond z ((f (0 : Fin 4)) : Bool) ((f (1 : Fin 4)) : Bool)) : Bool) then ((f (2 : Fin 4)) : ℝ) else ((f (3 : Fin 4)) : ℝ) cases z · refine Measurable.ite ?_ ?_ ?_ · exact (by fun_prop : Measurable fun f : ∀ i : Fin S.cfBundle.n, S.cfBundle.type i => ((f (1 : Fin 4)) : Bool)) (MeasurableSet.singleton true) · exact measurable_pi_apply (2 : Fin 4) · exact measurable_pi_apply (3 : Fin 4) · refine Measurable.ite ?_ ?_ ?_ · exact (by fun_prop : Measurable fun f : ∀ i : Fin S.cfBundle.n, S.cfBundle.type i => ((f (0 : Fin 4)) : Bool)) (MeasurableSet.singleton true) · exact measurable_pi_apply (2 : Fin 4) · exact measurable_pi_apply (3 : Fin 4) have h_cons : ∀ ω ∈ S.zVar.event z, S.factualY ω = h_proj (S.cfBundle.jointValue ω) := by intro ω hω rw [S.factualY_eq_YofD_factualD hA ω, ← S.DofZ_eq_factualD_on_zEvent hA z hω] have hJV0 : (S.cfBundle.jointValue ω (0 : Fin 4) : Bool) = S.DofZ true ω := rfl have hJV1 : (S.cfBundle.jointValue ω (1 : Fin 4) : Bool) = S.DofZ false ω := rfl have hJV2 : (S.cfBundle.jointValue ω (2 : Fin 4) : ℝ) = S.YofD true ω := rfl have hJV3 : (S.cfBundle.jointValue ω (3 : Fin 4) : ℝ) = S.YofD false ω := rfl change S.YofD (S.DofZ z ω) ω = if ((cond z ((S.cfBundle.jointValue ω (0 : Fin 4)) : Bool) ((S.cfBundle.jointValue ω (1 : Fin 4)) : Bool)) : Bool) then ((S.cfBundle.jointValue ω (2 : Fin 4)) : ℝ) else ((S.cfBundle.jointValue ω (3 : Fin 4)) : ℝ) rw [hJV0, hJV1, hJV2, hJV3] cases z <;> cases S.DofZ _ ω <;> simp have hbridge : S.condExpYZ z = eventCondExp P.μ (S.zVar.event z) S.factualY := rfl rw [hbridge, POSystem.eventCondExp_of_consistency_IndepCF hA.instrumentIndep (a := S.zVar) hh_meas (measurableSet_singleton z) (ae_restrict_of_forall_mem (S.measurableSet_zEvent z) h_cons) (hμne_zero z hZ) (hμne_top z)] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω change (if ((cond z ((S.cfBundle.jointValue ω (0 : Fin 4)) : Bool) ((S.cfBundle.jointValue ω (1 : Fin 4)) : Bool)) : Bool) then ((S.cfBundle.jointValue ω (2 : Fin 4)) : ℝ) else ((S.cfBundle.jointValue ω (3 : Fin 4)) : ℝ)) = S.YofDofZ z ω unfold YofDofZ cases z <;> rfl rw [hCE true hZ1, hCE false hZ0] rw [← MeasureTheory.integral_sub (hYDZ_int true) (hYDZ_int false)] -
pointwise_monotonicitytheorem — Step 3 of rem:po-late: pointwise monotonicity identity. Y(D(1)) - Y(D(0)) = (Y(1) - Y(0)) · 1_C almost surely.hypotheseshA :S.AssumptionsProof (Lean source)
theorem pointwise_monotonicity (hA : S.Assumptions) : ∀ᵐ ω ∂P.μ, S.YofDofZ true ω - S.YofDofZ false ω = (S.YofD true ω - S.YofD false ω) * S.complierEvent.indicator (fun _ => (1:ℝ)) ω := by refine hA.monotonicity.mono (fun ω hω => ?_) unfold YofDofZ complierEvent rcases hD1 : S.DofZ true ω <;> rcases hD0 : S.DofZ false ω <;> simp_all [indicator] -
event_conditioning_identitytheorem — Step 4 of rem:po-late: event-conditioning identity. E[(Y(1) - Y(0)) · 1_C] = P(C) · LATE.Proof (Lean source)
theorem event_conditioning_identity : ∫ ω, (S.YofD true ω - S.YofD false ω) * S.complierEvent.indicator (fun _ => (1:ℝ)) ω ∂P.μ = (P.μ S.complierEvent).toReal * S.LATE := by unfold LATE eventCondExp have hC : MeasurableSet S.complierEvent := S.measurableSet_complierEvent have h_rw : (fun ω => (S.YofD true ω - S.YofD false ω) * S.complierEvent.indicator (fun _ => (1:ℝ)) ω) = S.complierEvent.indicator (fun ω => S.YofD true ω - S.YofD false ω) := by funext ω by_cases hω : ω ∈ S.complierEvent · simp [Set.indicator_of_mem hω] · simp [Set.indicator_of_notMem hω] rw [h_rw, MeasureTheory.integral_indicator hC] by_cases hμ : (P.μ S.complierEvent).toReal = 0 · rw [hμ, zero_mul] have hμ0 : P.μ S.complierEvent = 0 := by have hne : P.μ S.complierEvent ≠ ⊤ := measure_ne_top _ _ exact (ENNReal.toReal_eq_zero_iff _).mp hμ |>.resolve_right hne have hrest : P.μ.restrict S.complierEvent = 0 := by rw [MeasureTheory.Measure.restrict_eq_zero]; exact hμ0 simp [hrest] · field_simp