PO.ID.Exact
Exact (point) identification: back-door and front-door adjustment, IV/LATE, regression discontinuity, proximal inference, dynamic regimes, and related theorems.
ATE 25 core · 36 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].
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)
Given a binary-treatment backdoor system, the treatment potential-outcome variable is the system's treatment represented with the two treatment arms.
Definition (Lean source)
Given a binary-treatment backdoor system, the outcome potential-outcome variable is the system's real-valued outcome.
Definition (Lean source)
Given a binary-treatment backdoor system, the adjustment-covariate potential-outcome variable is its specified covariate.
Definition (Lean source)
Given a binary-treatment backdoor system and a treatment arm, the potential outcome under that arm assigns every unit its real-valued outcome if treatment were set to that arm.
Definition (Lean source)
Given a binary-treatment backdoor system, the factual treatment assigns every unit its observed treatment arm.
Definition (Lean source)
Given a binary-treatment backdoor system, the factual outcome assigns every unit its observed real-valued outcome.
Definition (Lean source)
Given a binary-treatment backdoor system, the factual covariate assigns every unit its observed adjustment-covariate value.
Definition (Lean source)
Given a binary-treatment backdoor system, the covariate σ-algebra is the σ-algebra on the sample space generated by the factual covariate.
Definition (Lean source)
Given a binary-treatment backdoor system and a treatment arm, the regimed outcome variable is the outcome variable under the regime fixing treatment to that arm.
Definition (Lean source)
Given a binary-treatment backdoor system, the counterfactual bundle contains the treated and untreated potential outcomes for unconfoundedness.
Definition (Lean source)
Given a binary-treatment backdoor system and a treatment arm, the propensity score assigns each unit the conditional probability of receiving that arm given the covariate σ-algebra.
Definition (Lean source)
Given a binary-treatment backdoor system and a treatment arm, the conditional mean potential outcome assigns each unit the conditional mean of that arm's potential outcome given the covariate.
Definition (Lean source)
Given a binary-treatment backdoor system, the average treatment effect is the population mean of the treated potential outcome minus the untreated potential outcome.
Definition (Lean source)
Given a binary-treatment backdoor system and a treatment arm, the adjusted conditional functional is the covariate-conditional mean of factual outcome times the indicator for that arm, divided by that arm's propensity score.
Definition (Lean source)
Given a binary-treatment backdoor system, the adjusted average treatment effect is the population mean of the adjusted conditional functional for treatment minus that for control.
Definition (Lean source)
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)
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.
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).
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).
Regularity: the control potential outcome Y(0) is integrable (so E[Y(0)]
is well-defined).
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
Proof (Lean source)
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
Proof (Lean source)
Given a binary-treatment backdoor system, the factual treatment--covariate pair assigns each unit its observed treatment arm and covariate value.
Definition (Lean source)
Given a binary-treatment backdoor system, the joint treatment--covariate σ-algebra is the σ-algebra on the sample space generated by the factual treatment--covariate pair.
Definition (Lean source)
Given a binary-treatment backdoor system, the outcome regression assigns each unit the conditional mean of the factual outcome given its factual treatment and covariate.
Definition (Lean source)
Given a binary-treatment backdoor system, the value-space outcome regression maps a treatment--covariate value to the corresponding conditional mean factual outcome.
Definition (Lean source)
Given a binary-treatment backdoor system, the value-space propensity representative maps each covariate value to the treated-arm propensity score at that value.
Definition (Lean source)
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
Proof (Lean source)
36 supporting declarations (lemmas, instances)
-
measurable_YofDlemma — Potential outcomes under fixed treatment arms are measurable.hypothesesconclusionMeasurable (S.YofD d)Proof (Lean source)
@[fun_prop] lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_factualDlemma — The observed treatment is measurable.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_factualXlemma — The observed covariate is measurable.hypothesesconclusionMeasurable S.factualXProof (Lean source)
@[fun_prop] 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.hypothesesconclusionS.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaX_le : S.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualX.comap_le -
measurable_factualX_sigmaXlemma — The observed covariate is measurable for the covariate sigma-algebra it generates.hypothesesconclusionMeasurable[S.sigmaX] S.factualXProof (Lean source)
@[fun_prop] lemma measurable_factualX_sigmaX : Measurable[S.sigmaX] S.factualX := comap_measurable S.factualX -
propScore_eqlemma — The propensity score at a treatment arm is the conditional expectation of that arm's treatment indicator given the covariate σ-algebra.hypothesesconclusionS.propScore d = P.μ[S.dVar.indicator d | S.sigmaX]Proof (Lean source)
@[causal_defs_simps] lemma propScore_eq (d : Bool) : S.propScore d = P.μ[S.dVar.indicator d | S.sigmaX] := rfl -
CATE_eqlemma — The conditional mean potential outcome at a treatment arm is the conditional expectation of that arm's potential outcome given the covariate σ-algebra.hypothesesconclusionS.CATE d = P.μ[S.YofD d | S.sigmaX] -
stronglyMeasurable_propScore_sigmaXlemma — The propensity score is strongly measurable for the covariate sigma-algebra: it is a conditional expectation given that sigma-algebra.hypothesesconclusionStronglyMeasurable[S.sigmaX] (S.propScore d)Proof (Lean source)
@[fun_prop] lemma stronglyMeasurable_propScore_sigmaX (d : Bool) : StronglyMeasurable[S.sigmaX] (S.propScore d) := MeasureTheory.stronglyMeasurable_condExp -
measurable_propScore_sigmaXlemma — The propensity score is measurable for the covariate sigma-algebra.hypothesesconclusionMeasurable[S.sigmaX] (S.propScore d)Proof (Lean source)
@[fun_prop] lemma measurable_propScore_sigmaX (d : Bool) : Measurable[S.sigmaX] (S.propScore d) := (MeasureTheory.stronglyMeasurable_condExp).measurable -
measurable_propScorelemma — The propensity score is measurable for the ambient sigma-algebra on the sample space.hypothesesconclusionMeasurable (S.propScore d)Proof (Lean source)
@[fun_prop] lemma measurable_propScore (d : Bool) : Measurable (S.propScore d) := (S.measurable_propScore_sigmaX d).mono S.sigmaX_le le_rfl -
integrable_propScorelemma — The propensity score is integrable: it is a conditional expectation.hypothesesconclusionIntegrable (S.propScore d) P.μProof (Lean source)
@[fun_prop] lemma integrable_propScore (d : Bool) : Integrable (S.propScore d) P.μ := MeasureTheory.integrable_condExp -
stronglyMeasurable_CATE_sigmaXlemma — The conditional mean potential outcome is strongly measurable for the covariate sigma-algebra.hypothesesconclusionStronglyMeasurable[S.sigmaX] (S.CATE d)Proof (Lean source)
@[fun_prop] lemma stronglyMeasurable_CATE_sigmaX (d : Bool) : StronglyMeasurable[S.sigmaX] (S.CATE d) := MeasureTheory.stronglyMeasurable_condExp -
measurable_CATElemma — The conditional mean potential outcome is measurable for the ambient sigma-algebra on the sample space.hypothesesconclusionMeasurable (S.CATE d)Proof (Lean source)
@[fun_prop] lemma measurable_CATE (d : Bool) : Measurable (S.CATE d) := ((MeasureTheory.stronglyMeasurable_condExp (μ := P.μ) (m := S.sigmaX) (f := S.YofD d)).measurable).mono S.sigmaX_le le_rfl -
integrable_CATElemma — The conditional mean potential outcome is integrable: it is a conditional expectation.hypothesesconclusionIntegrable (S.CATE d) P.μProof (Lean source)
@[fun_prop] lemma integrable_CATE (d : Bool) : Integrable (S.CATE d) P.μ := MeasureTheory.integrable_condExp -
adjustedCE_deflemma — The adjusted conditional functional at a treatment arm sends a unit to the conditional expectation, given the covariate σ-algebra, of the factual outcome times that arm's treatment indicator, divided by the propensity score of that arm.hypothesesconclusionS.adjustedCE d= fun ω => P.μ[fun ω' => S.factualY ω' * S.dVar.indicator d ω' | S.sigmaX] ω / S.propScore d ωProof (Lean source)
@[causal_defs_simps] lemma adjustedCE_def (d : Bool) : S.adjustedCE d = fun ω => P.μ[fun ω' => S.factualY ω' * S.dVar.indicator d ω' | S.sigmaX] ω / S.propScore d ω := rfl -
integrable_YofDlemma — Under the backdoor assumption bundle the potential outcome of either treatment arm is integrable.hypothesesconclusionIntegrable (S.YofD d) P.μProof (Lean source)
@[fun_prop] lemma Assumptions.integrable_YofD [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.Assumptions) (d : Bool) : Integrable (S.YofD d) P.μ := by cases d · exact hA.integrable_Y0 · exact hA.integrable_Y1 -
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.hypothesesγ :sharedType u_1hcons :P.ConsistencyhY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μconclusionIntegrable 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.μ := by fun_prop have hY0_ind : Integrable (fun ω => S.YofD false ω * S.dVar.indicator false ω) P.μ := by fun_prop have hsum_int : Integrable (fun ω => S.YofD true ω * S.dVar.indicator true ω + S.YofD false ω * S.dVar.indicator false ω) P.μ := by fun_prop 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)
@[fun_prop] 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] condexp_linearity 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] := by condexp_linearity [hindD_integrable true, hindD_integrable false] 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):hypothesesγ :sharedType u_1IsFiniteMeasure 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.μ := by fun_prop 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 fun_prop 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 := by fun_prop 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 fun_prop 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.hypothesesconclusionMeasurable S.factualDXProof (Lean source)
@[fun_prop] 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.hypothesesconclusionS.sigmaDX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaDX_le : S.sigmaDX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualDX.comap_le -
measurable_factualDX_sigmaDXlemma — The observed treatment-covariate pair is measurable for the joint sigma-algebra it generates.hypothesesconclusionMeasurable[S.sigmaDX] S.factualDXProof (Lean source)
@[fun_prop] lemma measurable_factualDX_sigmaDX : Measurable[S.sigmaDX] S.factualDX := comap_measurable S.factualDX -
measurable_factualD_sigmaDXlemma — The observed treatment is measurable for the joint treatment-covariate sigma-algebra.hypothesesconclusionMeasurable[S.sigmaDX] S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD_sigmaDX : Measurable[S.sigmaDX] S.factualD := measurable_fst.comp (comap_measurable S.factualDX) -
measurable_factualX_sigmaDXlemma — The observed covariate is measurable for the joint treatment-covariate sigma-algebra.hypothesesconclusionMeasurable[S.sigmaDX] S.factualXProof (Lean source)
@[fun_prop] lemma measurable_factualX_sigmaDX : Measurable[S.sigmaDX] S.factualX := measurable_snd.comp (comap_measurable S.factualDX) -
sigmaX_le_sigmaDXlemma — σ(X) ≤ σ(D, X): the covariate σ-algebra is coarser than the joint one.hypothesesconclusionS.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 comap_mono measurable_snd.comap_le -
stronglyMeasurable_outcomeReglemma — The observed outcome regression is strongly measurable with respect to the joint treatment-covariate sigma-algebra.hypothesesconclusionStronglyMeasurable[S.sigmaDX] S.outcomeRegProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_outcomeReg : StronglyMeasurable[S.sigmaDX] S.outcomeReg := MeasureTheory.stronglyMeasurable_condExp -
measurable_outcomeReglemma — The observed outcome regression is measurable for the ambient sigma-algebra on the sample space.hypothesesconclusionMeasurable S.outcomeRegProof (Lean source)
@[fun_prop] lemma measurable_outcomeReg : Measurable S.outcomeReg := (S.stronglyMeasurable_outcomeReg.measurable).mono S.sigmaDX_le le_rfl -
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.hypothesesProof (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 := by fun_prop 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.hypothesesconclusionMeasurable S.regFnProof (Lean source)
@[fun_prop] 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.hypothesesconclusionS.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.hypothesesProof (Lean source)
lemma exists_propScoreLift : ∃ e : γ → ℝ, Measurable e ∧ S.propScore true = fun ω => e (S.factualX ω) := by have hmeas : Measurable[S.sigmaX] (S.propScore true) := by fun_prop 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.hypothesesconclusionMeasurable S.eLiftProof (Lean source)
@[fun_prop] 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.hypothesesconclusionS.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 · 6 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.
Given a binary-treatment backdoor system, the marginal treatment probability is the population mean of the indicator for the treated arm.
Definition (Lean source)
Given a binary-treatment backdoor system, the average treatment effect on the treated is the population mean treatment effect weighted by the treated-arm indicator and divided by the marginal treatment probability. It is ATT = E[A · (Y(1) − Y(0))] / π_T.
Definition (Lean source)
Given a binary-treatment backdoor system, the adjusted average treatment effect on the treated is the treated-indicator-weighted population mean of factual outcome minus the adjusted control conditional functional, divided by the marginal treatment probability. It is the 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).
Definition (Lean source)
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)
Consistency (SUTVA): on {D = d}, the observed outcome equals Y(d).
Unconfoundedness: D ⟂ (Y(1), Y(0)) | X, as conditional independence of the
realized D and the counterfactual bundle given σ(X).
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.
Regularity: the treated potential outcome Y(1) is integrable.
Regularity: the control potential outcome Y(0) is integrable.
Positivity of the marginal treatment probability π_T = P[D=1].
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
Proof (Lean source)
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
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
integrable_YofDlemma — Under the ATT assumption bundle the potential outcome of either arm is integrable.hypothesesconclusionIntegrable (S.YofD d) P.μProof (Lean source)
@[fun_prop] lemma ATTAssumptions.integrable_YofD [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.ATTAssumptions) (d : Bool) : Integrable (S.YofD d) P.μ := by cases d · exact hA.integrable_Y0 · exact hA.integrable_Y1 -
integrable_factualYlemma — Under the ATT assumption bundle the observed outcome is integrable.hypothesesconclusionIntegrable S.factualY P.μProof (Lean source)
@[fun_prop] lemma ATTAssumptions.integrable_factualY [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.ATTAssumptions) : Integrable S.factualY P.μ := S.integrable_factualY_of_consistency hA.consistency hA.integrable_Y1 hA.integrable_Y0 -
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 -
stronglyMeasurable_adjustedCE_comaplemma — The backdoor adjustment functional is strongly measurable with respect to the covariate sigma-algebra.hypothesesconclusionStronglyMeasurable[S.sigmaX] (S.adjustedCE d)Proof (Lean source)
@[fun_prop] lemma stronglyMeasurable_adjustedCE_comap (d : Bool) : StronglyMeasurable[S.sigmaX] (S.adjustedCE d) := by unfold POBackdoorSystem.adjustedCE POBackdoorSystem.propScore exact ((MeasureTheory.stronglyMeasurable_condExp (μ := P.μ) (m := S.sigmaX) (f := fun ω' => S.factualY ω' * S.dVar.indicator d ω')).measurable.div (MeasureTheory.stronglyMeasurable_condExp (μ := P.μ) (m := S.sigmaX) (f := S.dVar.indicator d)).measurable).stronglyMeasurable -
measurable_adjustedCElemma — The backdoor adjustment functional is measurable for the ambient sigma-algebra on the sample space.hypothesesconclusionMeasurable (S.adjustedCE d)Proof (Lean source)
@[fun_prop] lemma measurable_adjustedCE (d : Bool) : Measurable (S.adjustedCE d) := (S.stronglyMeasurable_adjustedCE_comap d).mono S.sigmaX_le |>.measurable -
integrable_adjustedCE_controllemma — Under the ATT assumption bundle the control-arm backdoor adjustment functional is integrable.hypothesesconclusionIntegrable (S.adjustedCE false) P.μProof (Lean source)
@[fun_prop] lemma integrable_adjustedCE_control [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.ATTAssumptions) : Integrable (S.adjustedCE false) P.μ := by have hcate_int : Integrable (S.CATE false) P.μ := by fun_prop exact hcate_int.congr (S.cate_backdoor_control hA)
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.
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.
For a staggered-adoption DID system and a period, the binary treatment potential-outcome variable is the treatment node for that period.
Definition (Lean source)
For a staggered-adoption DID system and a period, the real-valued outcome potential-outcome variable is the outcome node for that period.
Definition (Lean source)
For a staggered-adoption DID system and a period, the factual treatment function assigns each unit its observed treatment at that period.
Definition (Lean source)
For a staggered-adoption DID system and a period, the factual outcome function assigns each unit its observed outcome at that period.
Definition (Lean source)
For a staggered-adoption DID system, a period, and a binary treatment value, the period-specific treatment event is the set of units whose observed treatment at that period equals that value.
For a staggered-adoption DID system, the treatment-target-set function maps each cutoff to the empty set at cutoff zero and the treatment nodes from periods strictly before the cutoff at every positive cutoff.
Definition (Lean source)
For a staggered-adoption DID system, a binary treatment path over all periods, a cutoff, and proof that the cutoff does not exceed the horizon, the partial treatment-path regime together with its target-set identity fixes treatments before the cutoff according to that path and has exactly the treatment nodes before the cutoff as its target.
Definition (Lean source)
For a staggered-adoption DID system and a binary treatment path over all periods, the full-horizon treatment regime fixes every period's treatment to the corresponding value on that path.
For a staggered-adoption DID system and a cohort period, the cohort treatment regime leaves all earlier periods untreated and fixes treatment to true in that cohort period and every later period.
Definition (Lean source)
For a staggered-adoption DID system, the never-treated regime fixes treatment to false in every period.
Definition (Lean source)
For a staggered-adoption DID system, an outcome period, and a cohort period, the cohort potential-outcome function assigns each unit its outcome at that period under the treatment path that begins in the cohort period.
Definition (Lean source)
For a staggered-adoption DID system and an outcome period, the never-treated potential-outcome function assigns each unit its outcome at that period under the regime that never treats.
Definition (Lean source)
For a staggered-adoption DID system, a cohort period, and proof that the cohort is not the first period, the predecessor period is the period immediately before that cohort.
Definition (Lean source)
For a staggered-adoption DID system, a cohort period, and proof that it is not the first period, the cohort event is the set of units untreated immediately before that period and treated in that period.
For a staggered-adoption DID system, the never-treated event is the set of units whose observed treatment is false in every period.
Definition (Lean source)
For a staggered-adoption DID system, a cohort period, an outcome period, and proof that the cohort is not the first period, the group-time average treatment effect on the treated is the cohort-event conditional mean of the period- difference between the cohort and never-treated potential outcomes.
Definition (Lean source)
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)
Consistency of the underlying PO system.
Irreversibility, base case: D_0 = 0 almost surely.
Irreversibility, absorbing: D_s = 1 ⟹ D_{s+1} = 1 almost surely.
No anticipation: pre-treatment outcomes are unaffected by future treatment.
Never-treated parallel trends (long-difference form).
Positivity of cohorts.
Positivity of the never-treated event.
Integrability of Y_t(g) for every cohort-period pair.
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
Proof (Lean source)
13 supporting declarations (lemmas, instances)
-
measurable_factualDlemma — The observed treatment at each period is measurable.hypothesesconclusionMeasurable (S.factualD s)Proof (Lean source)
@[fun_prop] 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.hypothesesconclusionMeasurable (S.factualY s)Proof (Lean source)
@[fun_prop] 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.hypothesesconclusionMeasurableSet (S.dEvent s b)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.hypothesesconclusionv ∈ 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.hypothesesconclusion(S.regimeBy b).target = S.dTargetUpTo S.TProof (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.hypothesesconclusionS.Y t ∉ S.dTargetUpTo kProof (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.hypothesesconclusionS.Y t ∉ (S.regimeBy b).target -
yVar_v_notin_regOf_targetlemma — The outcome variable at a period is not targeted by the cohort regime.hypothesesconclusion(S.yVar t).v ∉ (S.regOf g).targetProof (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.hypothesesconclusion(S.yVar t).v ∉ S.regNT.targetProof (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.hypothesesconclusionMeasurable (S.YofCohort t g)Proof (Lean source)
@[fun_prop] 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.hypothesesconclusionMeasurable (S.YofNT t)Proof (Lean source)
@[fun_prop] lemma measurable_YofNT (t : Fin S.T) : Measurable (S.YofNT t) := (S.yVar t).measurable_cf _ -
measurableSet_cohortEventlemma — Each cohort event is measurable.hypothesesconclusionMeasurableSet (S.cohortEvent g hg)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.Proof (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.
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.
For a two-period DID system, the binary treatment potential-outcome variable is its treatment node with values represented as false or true.
Definition (Lean source)
For a two-period DID system, the real-valued pre-period outcome potential-outcome variable is its pre-period outcome node.
Definition (Lean source)
For a two-period DID system, the real-valued post-period outcome potential-outcome variable is its post-period outcome node.
Definition (Lean source)
For a two-period DID system and a binary treatment arm, the pre-period potential-outcome function gives each unit's pre-period outcome when treatment is fixed to that arm.
Definition (Lean source)
For a two-period DID system and a binary treatment arm, the post-period potential-outcome function gives each unit's post-period outcome when treatment is fixed to that arm.
Definition (Lean source)
For a two-period DID system, the factual treatment function assigns each unit its observed binary treatment.
Definition (Lean source)
For a two-period DID system, the factual pre-period outcome function assigns each unit its observed pre-period outcome.
Definition (Lean source)
For a two-period DID system, the factual post-period outcome function assigns each unit its observed post-period outcome.
Definition (Lean source)
For a two-period DID system and a binary treatment arm, the treatment event is the set of units whose observed treatment equals that arm.
Definition (Lean source)
For a two-period DID system, the average treatment effect on the treated is the mean, conditional on observed treatment, of the difference between each treated unit's post-period potential outcomes under treatment and no treatment.
Definition (Lean source)
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)
Consistency (SUTVA): the observed outcome equals the potential outcome of the realized treatment arm.
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.
The treated group has positive probability, so its group-mean is defined.
(Finiteness μ ≠ ⊤ is automatic: P.μ is a probability measure.)
The control group has positive probability, so its group-mean is defined.
Integrability of the control pre-period potential outcome Y₀(0).
Integrability of the control post-period potential outcome Y₁(0).
Integrability of the treated post-period potential outcome Y₁(1).
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
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
measurable_Y0ofDlemma — The pre-period potential outcome under a fixed treatment arm is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_Y0ofD (d : Bool) : Measurable (S.Y0ofD d) := S.y0Var.measurable_cfUnder S.dVar d -
measurable_Y1ofDlemma — The post-period potential outcome under a fixed treatment arm is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_Y1ofD (d : Bool) : Measurable (S.Y1ofD d) := S.y1Var.measurable_cfUnder S.dVar d -
measurable_factualDlemma — The observed treatment is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualY₀lemma — The observed pre-period outcome is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualY₀ : Measurable S.factualY₀ := S.y0Var.measurable_factual -
measurable_factualY₁lemma — The observed post-period outcome is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualY₁ : Measurable S.factualY₁ := S.y1Var.measurable_factual -
measurableSet_dEventlemma — Each observed treatment-arm event is measurable.hypothesesconclusionMeasurableSet (S.dEvent d)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.
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)
For a frontdoor system, the binary treatment potential-outcome variable is its treatment node equipped with its binary value representation.
Definition (Lean source)
For a frontdoor system, the mediator potential-outcome variable is its mediator node equipped with its finite mediator-value representation.
Definition (Lean source)
For a frontdoor system, the real-valued outcome potential-outcome variable is its outcome node equipped with its real-valued representation.
Definition (Lean source)
For a frontdoor system and a treatment arm, the potential outcome assigns to each unit the real outcome it would have under that arm.
Definition (Lean source)
For a frontdoor system and a treatment arm, the potential mediator assigns to each unit the mediator value it would have under that arm.
Definition (Lean source)
For a frontdoor system, a treatment arm, and a mediator value, the joint treatment--mediator intervention regime fixes treatment and mediator simultaneously.
Definition (Lean source)
For a frontdoor system, a treatment arm, and a mediator value, the joint potential outcome assigns to each unit the outcome under simultaneously fixing treatment and mediator to those values.
Definition (Lean source)
For a frontdoor system, the factual treatment assigns each unit its observed binary treatment.
Definition (Lean source)
For a frontdoor system, the factual mediator assigns each unit its observed mediator value.
Definition (Lean source)
For a frontdoor system, the factual outcome assigns each unit its observed real outcome.
Definition (Lean source)
For a frontdoor system and a treatment arm, the treatment event is the set of units whose observed treatment equals that arm.
Definition (Lean source)
For a frontdoor system and a mediator value, the mediator event is the set of units whose observed mediator equals that value.
Definition (Lean source)
For a frontdoor system and a treatment arm, the mediator under that treatment regime is the mediator potential outcome represented together with the intervention that fixes treatment to that arm.
Definition (Lean source)
For a frontdoor system, the counterfactual mediator bundle consists of the mediator potential outcomes under treatment and control.
Definition (Lean source)
For a frontdoor system and a treatment arm, the treatment-arm probability is the probability that the observed treatment equals that arm.
Definition (Lean source)
For a frontdoor system, a mediator value, and a treatment arm, the conditional mediator probability is the event-conditional probability that the observed mediator equals that value given that observed treatment equals that arm.
Definition (Lean source)
For a frontdoor system, a treatment arm, and a mediator value, the conditional outcome mean is the event-conditional mean of the observed outcome among units with that observed treatment and mediator value.
Definition (Lean source)
For a frontdoor system and a treatment arm, the frontdoor-adjusted functional is the finite sum over mediator values of the treatment-probability-weighted conditional outcome means, weighted by the mediator distribution conditional on that arm.
For a frontdoor system, the average treatment effect is the population mean of the difference between each unit's potential outcome under treatment and under control.
Definition (Lean source)
For a frontdoor system, the observable frontdoor-adjusted average treatment effect is the frontdoor-adjusted functional under treatment minus that under control.
Definition (Lean source)
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)
Consistency axiom for the ambient PO system.
Full mediation / exclusion restriction: Y(a,m) = Y(a',m) a.s. for all
a, a' ∈ {0,1} and m ∈ β.
Treatment–mediator exchangeability: A ⊥ (M(1), M(0)). Equivalent
(for binary A) to M(a) ⊥ A for each a.
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.
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.
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/.
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)
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
Proof (Lean source)
15 supporting declarations (lemmas, instances)
-
measurable_YofAlemma — Treatment-arm potential outcomes are measurable.hypothesesconclusionMeasurable (S.YofA a)Proof (Lean source)
@[fun_prop] lemma measurable_YofA (a : Bool) : Measurable (S.YofA a) := S.yVar.measurable_cfUnder S.aVar a -
measurable_MofAlemma — Treatment-arm potential mediators are measurable.hypothesesconclusionMeasurable (S.MofA a)Proof (Lean source)
@[fun_prop] lemma measurable_MofA (a : Bool) : Measurable (S.MofA a) := S.mVar.measurable_cfUnder S.aVar a -
measurable_YofAMlemma — Joint treatment-mediator potential outcomes are measurable.hypothesesconclusionMeasurable (S.YofAM a m)Proof (Lean source)
@[fun_prop] lemma measurable_YofAM (a : Bool) (m : β) : Measurable (S.YofAM a m) := S.yVar.measurable_cf _ -
measurable_factualAlemma — The observed treatment is measurable.hypothesesconclusionMeasurable S.factualAProof (Lean source)
@[fun_prop] lemma measurable_factualA : Measurable S.factualA := S.aVar.measurable_factual -
measurable_factualMlemma — The observed mediator is measurable.hypothesesconclusionMeasurable S.factualMProof (Lean source)
@[fun_prop] lemma measurable_factualM : Measurable S.factualM := S.mVar.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_aEventlemma — The factual treatment event for a treatment arm is measurable.hypothesesconclusionMeasurableSet (S.aEvent a)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.hypothesesconclusionMeasurableSet (S.mEvent m)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.hypotheseshC :P.Consistencya :ω :P.Ωhω :ω ∈ S.aEvent aconclusionS.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.hypotheseshC :P.Consistencya :m :βω :P.Ωhω :ω ∈ S.aEvent a ∩ S.mEvent mconclusionS.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.hypothesesconclusionIntegrable S.factualY P.μProof (Lean source)
@[fun_prop] 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)(ω).hypotheseshC :P.Consistencya :m :βω :P.Ωhω :S.MofA a ω = mconclusionS.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.hypothesesconclusionProof (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 · 14 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.
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.
For a binary instrumental-variables system, the binary instrument potential-outcome variable is its instrument node with its binary representation.
Definition (Lean source)
For a binary instrumental-variables system, the binary treatment potential-outcome variable is its treatment node with its binary representation.
Definition (Lean source)
For a binary instrumental-variables system, the real-valued outcome potential-outcome variable is its outcome node with its real-valued representation.
Definition (Lean source)
For a binary instrumental-variables system and an instrument value, the instrument intervention regime fixes the instrument to that value.
Definition (Lean source)
For a binary instrumental-variables system and a treatment value, the treatment intervention regime fixes treatment to that value.
Definition (Lean source)
For a binary instrumental-variables system and an instrument value, the potential treatment assigns each unit the treatment it would take if the instrument were fixed to that value.
Definition (Lean source)
For a binary instrumental-variables system and a treatment value, the potential outcome assigns each unit the outcome it would have if treatment were fixed to that value.
Definition (Lean source)
For a binary instrumental-variables system, the factual instrument assigns each unit its observed binary instrument.
Definition (Lean source)
For a binary instrumental-variables system, the factual treatment assigns each unit its observed binary treatment.
Definition (Lean source)
For a binary instrumental-variables system, the factual outcome assigns each unit its observed real outcome.
Definition (Lean source)
For a binary instrumental-variables system, the complier event is the set of units that would take treatment when the instrument is on and would not take treatment when it is off.
For a binary instrumental-variables system and an instrument value, the instrument event is the set of units whose observed instrument equals that value.
Definition (Lean source)
For a binary instrumental-variables system and an instrument value, the outcome under the instrument-induced treatment assigns each unit its treated potential outcome if the instrument induces treatment and its untreated potential outcome otherwise.
Definition (Lean source)
For a binary instrumental-variables system and an instrument value, the conditional treatment mean is the event-conditional mean of observed treatment among units with that instrument value.
Definition (Lean source)
For a binary instrumental-variables system and an instrument value, the conditional outcome mean is the event-conditional mean of observed outcome among units with that instrument value.
Definition (Lean source)
For a binary instrumental-variables system and an instrument value, the treatment under the instrument regime is the potential treatment represented together with the intervention fixing the instrument to that value.
Definition (Lean source)
For a binary instrumental-variables system and a treatment value, the outcome under the treatment regime is the potential outcome represented together with the intervention fixing treatment to that value.
Definition (Lean source)
For a binary instrumental-variables system, the counterfactual bundle contains potential treatments under both instrument values and potential outcomes under both treatment values.
Definition (Lean source)
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)
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.)
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.
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).
For a binary instrumental-variables system, the local average treatment effect is the mean difference between treated and untreated potential outcomes among compliers, with value zero when the complier event has zero probability.
Definition (Lean source)
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
Proof (Lean source)
14 supporting declarations (lemmas, instances)
-
measurable_DofZlemma — The potential treatment under a fixed instrument value is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_DofZ (z : Bool) : Measurable (S.DofZ z) := S.dVar.measurable_cfUnder S.zVar z -
measurable_factualZlemma — The factual instrument is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The factual treatment is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.Proof (Lean source)
@[fun_prop] 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)
@[fun_prop] lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurableSet_complierEventlemma — The complier event is measurable. -
measurableSet_zEventlemma — The factual instrument event is measurable.hypothesesconclusionMeasurableSet (S.zEvent z)Proof (Lean source)
lemma measurableSet_zEvent (z : Bool) : MeasurableSet (S.zEvent z) := S.zVar.measurableSet_event _ (measurableSet_singleton _) -
YofDofZ_deflemma — The potential outcome under the treatment that an instrument value induces sends a unit to that unit's treated potential outcome when the induced treatment is one, and to its untreated potential outcome otherwise.hypotheses -
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}.hypothesesconclusionS.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).hypotheseshA :S.AssumptionsProof (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))].hypothesesProof (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.hypothesesProof (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.hypothesesProof (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