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 · 37 supporting This file proves backdoor identification for the average treatment effect in the potential-outcome framework. ★ conditionalMeanOutcome_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 conditionalMeanOutcome_backdoor_of_propScore_ne,
which isolates the per-arm assumptions, conditionalMeanOutcome_backdoor,
which discharges nonvanishing from two-sided overlap, ate_backdoor, 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)
The treatment variable used in backdoor adjustment represents the treatment in a binary-treatment system on the two possible arms.
Definition (Lean source)
The outcome variable used in backdoor adjustment represents the outcome in a binary-treatment system on the real line.
Definition (Lean source)
The covariate variable used for adjustment is the covariate specified by the backdoor system with its original measurable value space.
Definition (Lean source)
The arm-specific potential outcome in a backdoor system records each unit's outcome if treatment were set to the selected arm, rather than merely conditioning on units observed in that arm.
Definition (Lean source)
The factual treatment in a backdoor system records each unit's realized treatment arm.
Definition (Lean source)
The factual outcome in a backdoor system records each unit's observed real-valued response.
Definition (Lean source)
The factual covariate in a backdoor system records the observed adjustment value for each unit.
Definition (Lean source)
The information set used for backdoor adjustment in a binary-treatment system is exactly the σ-algebra generated by the observed covariate.
Definition (Lean source)
The regimed outcome variable in a backdoor system pairs the outcome with an intervention that fixes treatment to the selected arm, making that arm available to counterfactual-independence statements.
Definition (Lean source)
The counterfactual bundle used in the unconfoundedness assumption for a backdoor system collects both treated and untreated potential outcomes, so joint exchangeability covers both ATE arms.
Definition (Lean source)
The arm-specific propensity score in a backdoor system is the conditional treatment-arm probability given the adjustment covariates; the selected arm determines which overlap condition is relevant.
Definition (Lean source)
The arm-specific conditional mean potential outcome in a backdoor system averages the potential outcome given the adjustment covariates for the selected treatment arm.
Definition (Lean source)
The average treatment effect in a binary-treatment backdoor system averages each unit's treated-minus-untreated potential-outcome contrast.
Definition (Lean source)
The observable arm-specific adjustment functional in a backdoor system divides the covariate-conditional outcome contribution of an arm by its propensity, with the selected arm determining both quantities.
Definition (Lean source)
The observable adjusted ATE functional in a backdoor system averages the treated-minus-control contrast of the two adjusted conditional means.
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).
Conditional-mean backdoor identification. In a binary-treatment backdoor system, 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, the arm-specific conditional mean potential outcome equals the adjusted-outcome functional:
Formal statement
Proof (Lean source)
Integrated backdoor ATE identification. In a binary-treatment backdoor system, 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 two arm-specific conditional-mean backdoor identities over the covariate distribution.
Formal statement
Proof (Lean source)
The observable treatment–covariate state in a backdoor system pairs each unit's realized arm with its adjustment covariate.
Definition (Lean source)
The information set for observed outcome regression in a backdoor system is generated jointly by realized treatment and covariates.
Definition (Lean source)
The observable outcome regression in a backdoor system is the conditional mean of observed outcomes given realized treatment and covariates.
Definition (Lean source)
The value-space outcome regression for a backdoor system maps each treatment–covariate cell to its observable conditional mean outcome, which is the object a regression learner estimates.
Definition (Lean source)
The value-space propensity function for a backdoor system maps each covariate value to its treated-arm probability, matching the nuisance function estimated from observed data.
Definition (Lean source)
Regression-adjustment identification (observable). In a binary-treatment backdoor system, the adjustment functional for an arm equals the value-space outcome regression evaluated at that arm for the selected treatment arm when the observed outcome is integrable and the arm has almost-surely nonzero conditional probability given covariates:
Formal statement
Proof (Lean source)
37 supporting declarations (lemmas, instances)
-
measurable_YofDlemma — In a backdoor system, the potential outcome under a fixed arm is measurable, so its conditional mean and population mean are well-defined.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 — Observed treatment in a backdoor system is measurable, so treatment-arm events can be used for conditioning and adjustment.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — Observed outcome in a backdoor system is measurable, so its conditional regressions are valid random variables.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_factualXlemma — The adjustment covariate in a backdoor system is measurable, so it generates the information set used for adjustment.hypothesesconclusionMeasurable S.factualXProof (Lean source)
@[fun_prop] lemma measurable_factualX : Measurable S.factualX := S.xVar.measurable_factual -
sigmaX_lelemma — The covariate information set in a backdoor system is contained in the full observable σ-algebra, so covariate-measurable nuisance functions are valid random variables.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 in a backdoor system is measurable using only the information it generates, which licenses conditioning on that covariate.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 -
conditionalMeanOutcome_eqlemma — For an arm in a backdoor system, the arm-specific conditional mean potential outcome equals the conditional expectation of that arm's potential outcome given the covariate σ-algebra.hypothesesconclusionS.conditionalMeanOutcome d = P.μ[S.YofD d | S.sigmaX]Proof (Lean source)
@[causal_defs_simps] lemma conditionalMeanOutcome_eq (d : Bool) : S.conditionalMeanOutcome d = P.μ[S.YofD d | S.sigmaX] := rfl -
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 for a treatment arm uses only covariate information in the backdoor system, as required for adjustment.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 for a treatment arm in a backdoor system is a measurable random variable on the full 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 for a treatment arm in a backdoor system has a finite population mean, because it is a conditional probability.hypothesesconclusionIntegrable (S.propScore d) P.μProof (Lean source)
@[fun_prop] lemma integrable_propScore (d : Bool) : Integrable (S.propScore d) P.μ := MeasureTheory.integrable_condExp -
stronglyMeasurable_conditionalMeanOutcome_sigmaXlemma — In a backdoor system, the conditional mean potential outcome for an arm is strongly measurable for the covariate σ-algebra.hypothesesconclusionStronglyMeasurable[S.sigmaX] (S.conditionalMeanOutcome d)Proof (Lean source)
@[fun_prop] lemma stronglyMeasurable_conditionalMeanOutcome_sigmaX (d : Bool) : StronglyMeasurable[S.sigmaX] (S.conditionalMeanOutcome d) := MeasureTheory.stronglyMeasurable_condExp -
measurable_conditionalMeanOutcomelemma — In a backdoor system, the conditional mean potential outcome for an arm is a measurable random variable on the sample space.hypothesesconclusionMeasurable (S.conditionalMeanOutcome d)Proof (Lean source)
@[fun_prop] lemma measurable_conditionalMeanOutcome (d : Bool) : Measurable (S.conditionalMeanOutcome d) := ((MeasureTheory.stronglyMeasurable_condExp (μ := P.μ) (m := S.sigmaX) (f := S.YofD d)).measurable).mono S.sigmaX_le le_rfl -
integrable_conditionalMeanOutcomelemma — In a backdoor system, the conditional mean potential outcome for an arm has a finite population mean whenever represented as a conditional expectation.hypothesesconclusionIntegrable (S.conditionalMeanOutcome d) P.μProof (Lean source)
@[fun_prop] lemma integrable_conditionalMeanOutcome (d : Bool) : Integrable (S.conditionalMeanOutcome 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 backdoor assumptions guarantee that the observed outcome in the system has a finite population mean, by consistency and armwise integrability.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 -
conditionalMeanOutcome_backdoor_of_propScore_netheorem — Per-arm backdoor identification. In a binary-treatment backdoor system, the arm-specific conditional mean potential outcome equals the adjusted-outcome functional when factual consistency, conditional independence of that arm's potential outcome from treatment given covariates, integrability of both potential outcomes, and nonzero propensity for the selected arm hold for that treatment arm:hypothesesγ :sharedType u_1IsFiniteMeasure P.μhcons :P.Consistencyd :hunconf :CondIndepFun S.sigmaX S.sigmaX_le S.factualD (S.YofD d) P.μhY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μh_ne :∀ᵐ ω ∂P.μ, S.propScore d ω ≠ 0conclusionS.conditionalMeanOutcome d =ᵐ[P.μ] S.adjustedCE dProof (Lean source)
theorem conditionalMeanOutcome_backdoor_of_propScore_ne [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hcons : P.Consistency) (d : Bool) (hunconf : CondIndepFun S.sigmaX S.sigmaX_le S.factualD (S.YofD d) P.μ) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) (h_ne : ∀ᵐ ω ∂P.μ, S.propScore d ω ≠ 0) : S.conditionalMeanOutcome 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.conditionalMeanOutcome d) ?_ ?_).symm · -- (hprod): μ[Y·1_{D=d}|σX] =ᵐ μ[1_{D=d}|σX] · conditionalMeanOutcome 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 ?_ -- 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) hunconf (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) * conditionalMeanOutcome d. -- Unfold the definitions to land on μ[·|σX] with matching argument shapes. unfold POVar.condExpGiven POBackdoorSystem.conditionalMeanOutcome 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 -
conditionalMeanOutcome_backdoor_of_condIndepCF_of_propScore_netheorem — Backdoor identification from the traditional two-arm exchangeability bundle. Under factual consistency, joint conditional independence of treatment from both potential outcomes, integrability of both arms, for a treatment arm with nonzero propensity, the arm-specific conditional mean equals the adjusted-outcome functional.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.conditionalMeanOutcome d =ᵐ[P.μ] S.adjustedCE dProof (Lean source)
theorem conditionalMeanOutcome_backdoor_of_condIndepCF_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.conditionalMeanOutcome d =ᵐ[P.μ] S.adjustedCE d := by have hCI : CondIndepFun S.sigmaX S.sigmaX_le S.factualD (S.YofD d) P.μ := by cases d · exact hunconf.component (1 : Fin 2) · exact hunconf.component (0 : Fin 2) exact S.conditionalMeanOutcome_backdoor_of_propScore_ne hcons d hCI hY1 hY0 h_ne -
measurable_factualDXlemma — The observed treatment–covariate state in a backdoor system is measurable, so it can generate the information set for outcome regression.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 information set in a backdoor system is contained in the full observable σ-algebra, so observed outcome regression is well-defined.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 state in a backdoor system is measurable using only its jointly generated information.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 — Observed treatment in a backdoor system is available in the joint treatment–covariate information set.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 in a backdoor system is available in the joint treatment–covariate information set.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 — The covariate information set in a backdoor system is coarser than the joint treatment–covariate information set, enabling conditional-expectation tower arguments between adjustment and outcome regression.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 in a backdoor system depends measurably only on realized treatment and covariates, so it is a genuine regression nuisance.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 in a backdoor system is a measurable random variable on the full 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 selected value-space outcome regression for a backdoor system is measurable, so evaluating it at observed or counterfactual arms remains valid.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 selected value-space propensity for a backdoor system is measurable, so it can be evaluated at the observed covariate.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 · 7 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.
The treated share of the population in a binary-treatment backdoor system is the population mean of the treated-arm indicator; it is the normalizing probability for effects conditional on treatment.
Definition (Lean source)
The average treatment effect on the treated in a binary-treatment backdoor system averages individual treatment effects over treated units: ATT = E[A · (Y(1) − Y(0))] / π_T.
Definition (Lean source)
The observable adjusted ATT functional in a binary-treatment backdoor system averages, among treated units, observed outcomes minus the adjusted control regression. It is the 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)
The standard ATT conditions for a binary-treatment backdoor system require factual consistency, conditional independence of treatment from the untreated potential outcome given covariates, one-sided control-arm overlap, integrability of the treated and untreated potential outcomes, and a positive marginal treatment probability.
Definition (Lean source)
Consistency (SUTVA): on {D = d}, the observed outcome equals Y(d).
One-sided unconfoundedness: D ⟂ Y(0) | X. Independence from Y(1) is
unnecessary because that potential outcome is observed among treated units.
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). In a binary-treatment backdoor system, under consistency, unconfoundedness, one-sided overlap (e(X) < 1, the control arm), and integrability of both potential outcomes, together with 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. In a binary-treatment backdoor system, under the ATT identification assumptions — consistency, unconfoundedness, one-sided control-arm overlap, integrable potential outcomes, 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)
7 supporting declarations (lemmas, instances)
-
ofFullUnconfoundednesstheorem — Traditional two-arm exchangeability is sufficient for the one-sided ATT identification conditions in a backdoor system: retaining consistency, control-arm overlap, integrability of both potential outcomes, and a nonempty treated population, it projects exchangeability onto the untreated potential outcome actually missing among treated units.hypothesesγ :sharedType u_1IsFiniteMeasure P.μconsistency :P.Consistencyunconfoundedness :P.CondIndepCF (RegimedVar.ofFactual S.dVar) S.cfBundle (RegimedVar.ofFactual S.xVar) P.μoverlapControl :∀ᵐ ω ∂P.μ, S.propScore true ω < 1integrable_Y1 :Integrable (S.YofD true) P.μintegrable_Y0 :Integrable (S.YofD false) P.μpropTreated_pos :0 < S.propTreatedconclusionS.ATTAssumptions where consistencyProof (Lean source)
theorem ATTAssumptions.ofFullUnconfoundedness [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (consistency : P.Consistency) (unconfoundedness : P.CondIndepCF (RegimedVar.ofFactual S.dVar) S.cfBundle (RegimedVar.ofFactual S.xVar) P.μ) (overlapControl : ∀ᵐ ω ∂P.μ, S.propScore true ω < 1) (integrable_Y1 : Integrable (S.YofD true) P.μ) (integrable_Y0 : Integrable (S.YofD false) P.μ) (propTreated_pos : 0 < S.propTreated) : S.ATTAssumptions where consistency := consistency unconfoundedness := unconfoundedness.component (1 : Fin 2) overlapControl := overlapControl integrable_Y1 := integrable_Y1 integrable_Y0 := integrable_Y0 propTreated_pos := propTreated_pos -
integrable_YofDlemma — The ATT assumptions make either treatment arm in the backdoor system integrable, so both arm means needed for the treated effect are finite.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 — The ATT assumptions ensure that the observed outcome in the backdoor system has a finite mean, using consistency to select between the two integrable potential outcomes.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 adjustment functional for a treatment arm depends measurably only on covariate information in the backdoor system, so it is a valid covariate regression.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 adjustment functional for a treatment arm in a backdoor system is a measurable random variable on the full 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 — The ATT assumptions make the control-arm adjustment functional in the backdoor system integrable, allowing its treated-group weighted mean to enter the ATT formula.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.conditionalMeanOutcome false) P.μ := by fun_prop exact hcate_int.congr (S.conditionalMeanOutcome_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.
The period-specific treatment variable in a staggered-adoption DID system records treated status at the selected period, with that period locating the unit on the adoption path.
Definition (Lean source)
The period-specific outcome variable in a staggered-adoption DID system records the real-valued response at the selected period, with that period fixing the outcome date.
Definition (Lean source)
The observed treatment path at one date in a staggered-adoption DID system records each unit's realized treatment status at the selected period.
Definition (Lean source)
The observed outcome at one date in a staggered-adoption DID system records each unit's realized response at the selected period.
Definition (Lean source)
The period-specific treatment group in a staggered-adoption DID system collects units whose observed treatment matches the selected status at a chosen period, with the status distinguishing treated from untreated units.
The partial treatment-path target for a staggered-adoption DID system starts with no intervened treatment nodes and adds exactly the treatment nodes strictly before each later cutoff, preventing regimes from overwriting outcomes or future treatment assignments.
Definition (Lean source)
The partial treatment-path regime with its target certificate for a staggered-adoption DID system and a proposed treatment path intervenes nowhere at the initial cutoff and extends the regime one period at a time while certifying that exactly the past treatment nodes are targeted.
Definition (Lean source)
The full-horizon treatment regime for a staggered-adoption DID system fixes every period's treatment to the prescribed path, where the path may represent a cohort or perpetual non-treatment.
The cohort treatment regime in a staggered-adoption DID system keeps units untreated before adoption and treated from adoption onward, with the cohort period marking the first treated date.
Definition (Lean source)
The never-treated comparison regime in a staggered-adoption DID system keeps treatment off throughout the observation horizon.
Definition (Lean source)
The cohort-path potential outcome in a staggered-adoption DID system records the outcome under adoption at the cohort date, evaluated at the outcome period for the selected cohort.
Definition (Lean source)
The never-treated potential outcome in a staggered-adoption DID system records the outcome had treatment remained off throughout at the selected outcome period.
Definition (Lean source)
The baseline period for a treatment cohort in a staggered-adoption DID system is the date immediately before adoption; the cohort date and its noninitial-period condition ensure that date exists.
Definition (Lean source)
The first-treated cohort in a staggered-adoption DID system consists of units untreated immediately before the cohort date and treated at that date; the date and its noninitial-period condition make this transition observable.
The never-treated comparison group in a staggered-adoption DID system contains exactly the units untreated in every observed period.
Definition (Lean source)
The group-time average treatment effect on the treated in a staggered-adoption DID system compares cohort-path and never-treated potential outcomes within the first-treated cohort, for the cohort date, outcome date, and valid baseline condition.
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. In a staggered-adoption DID system, the group-time average treatment effect on the treated equals the cohort's mean outcome change minus the corresponding never-treated mean change under irreversible adoption, consistency, no anticipation, group-time parallel trends, positive cohort and comparison-group probabilities, and integrable potential outcomes, for the selected treatment cohort which is not the initial period and the selected outcome period which is no earlier than treatment:
Formal statement
Proof (Lean source)
13 supporting declarations (lemmas, instances)
-
measurable_factualDlemma — In a staggered-adoption DID system, treatment at a selected period is measurable, so adoption histories define valid events.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 — In a staggered-adoption DID system, the outcome at a selected period is measurable, so cohort-time means are well-defined.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 — In a staggered-adoption DID system, a treatment status at a selected period defines a measurable group event.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⟩, 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 — In a staggered-adoption DID system, the potential outcome for a cohort path at an outcome date is measurable, so cohort-time effects can be averaged.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 — In a staggered-adoption DID system, the never-treated potential outcome at a selected date is measurable, so it supplies a valid comparison mean.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 — In a staggered-adoption DID system, the first-treated cohort at a valid date forms a measurable event suitable for cohort means.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 group in a staggered-adoption DID system is measurable, so it can supply the comparison-group conditional means.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.
The treatment variable used in two-period DID represents the system's treatment as the treated and control arms.
Definition (Lean source)
The baseline outcome variable in a two-period DID system records the real-valued outcome before treatment.
Definition (Lean source)
The follow-up outcome variable in a two-period DID system records the real-valued outcome after treatment.
Definition (Lean source)
The baseline potential outcome in a two-period DID system records what each unit's pre-period outcome would be under the selected arm; the arm is useful for stating and testing no anticipation.
Definition (Lean source)
The follow-up potential outcome in a two-period DID system records what each unit's post-period outcome would be under the selected arm, with that arm defining the causal contrast of interest.
Definition (Lean source)
The observed treatment assignment in a two-period DID system records whether each unit belongs to the treated or control group.
Definition (Lean source)
The observed baseline outcome in a two-period DID system records each unit's pre-treatment response.
Definition (Lean source)
The observed follow-up outcome in a two-period DID system records each unit's post-treatment response.
Definition (Lean source)
The observed treatment group in a two-period DID system collects the units assigned to the selected arm, with the arm distinguishing treated from control units.
Definition (Lean source)
The average treatment effect on the treated in a two-period DID system is the treated-group mean difference between treated and untreated follow-up potential outcomes.
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).
In a two-period DID system, under the identifying 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 — In a two-period DID system, the baseline potential outcome under a fixed arm is measurable, so group-conditional baseline means are well-defined.Proof (Lean source)
@[fun_prop] lemma measurable_Y0ofD (d : Bool) : Measurable (S.Y0ofD d) := S.y0Var.measurable_cfUnder S.dVar d -
measurable_Y1ofDlemma — In a two-period DID system, the follow-up potential outcome under a fixed arm is measurable, so group-conditional follow-up means are well-defined.Proof (Lean source)
@[fun_prop] lemma measurable_Y1ofD (d : Bool) : Measurable (S.Y1ofD d) := S.y1Var.measurable_cfUnder S.dVar d -
measurable_factualDlemma — Treatment assignment in a two-period DID system is measurable, so treated and control groups form valid conditioning events.Proof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualY₀lemma — The observed baseline outcome in a two-period DID system is measurable, so its treated and control means can enter the DID contrast.Proof (Lean source)
@[fun_prop] lemma measurable_factualY₀ : Measurable S.factualY₀ := S.y0Var.measurable_factual -
measurable_factualY₁lemma — The observed follow-up outcome in a two-period DID system is measurable, so its treated and control means can enter the DID contrast.Proof (Lean source)
@[fun_prop] lemma measurable_factualY₁ : Measurable S.factualY₁ := S.y1Var.measurable_factual -
measurableSet_dEventlemma — In a two-period DID system, membership in either observed treatment arm defines a measurable event suitable for group means.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)
The treatment variable used by frontdoor adjustment represents the system's treatment as the treated and control arms.
Definition (Lean source)
The mediator variable used by frontdoor adjustment represents the system's mediator on its finite support, enabling the adjustment sum over mediator levels.
Definition (Lean source)
The outcome variable used by frontdoor adjustment represents the system's outcome on the real line.
Definition (Lean source)
The treatment-specific potential outcome in a frontdoor system records each unit's outcome if treatment were set to the selected arm, with that arm defining the total-effect contrast.
Definition (Lean source)
The treatment-specific potential mediator in a frontdoor system records the mediator value induced by setting treatment to the selected arm, with that arm indexing the first frontdoor link.
Definition (Lean source)
The joint treatment–mediator intervention in a frontdoor system sets treatment and mediator simultaneously, at the selected arm and mediator level.
Definition (Lean source)
The joint treatment–mediator potential outcome in a frontdoor system records the response under simultaneous intervention at the selected treatment arm and mediator level; full mediation compares these outcomes across arms.
Definition (Lean source)
The factual treatment in a frontdoor system records each unit's observed treatment arm.
Definition (Lean source)
The factual mediator in a frontdoor system records each unit's observed mediator level.
Definition (Lean source)
The factual outcome in a frontdoor system records each unit's observed real-valued response.
Definition (Lean source)
The observed treatment group in a frontdoor system collects units whose realized treatment matches the selected arm, with that arm indexing probabilities and conditional means.
Definition (Lean source)
The observed mediator cell in a frontdoor system collects units whose realized mediator matches the selected level, with that level indexing the finite frontdoor sum.
Definition (Lean source)
The regimed mediator in a frontdoor system pairs the mediator with an intervention fixing treatment to the selected arm, so mediator exchangeability can be stated across treatment worlds.
Definition (Lean source)
The counterfactual mediator bundle for a frontdoor system collects mediator responses under both treatment arms, allowing one joint treatment–mediator exchangeability assumption.
Definition (Lean source)
The observed treatment-arm probability in a frontdoor system measures the population share receiving the selected arm, with that arm weighting mediator-specific outcome means.
Definition (Lean source)
The mediator distribution within a treatment arm in a frontdoor system is the conditional probability of the selected mediator cell, for the mediator level and observed treatment arm used in adjustment.
Definition (Lean source)
The observed treatment–mediator cell mean in a frontdoor system averages outcomes among units in the selected joint cell, indexed by treatment arm and mediator level.
Definition (Lean source)
The frontdoor-adjusted mean under a treatment arm in a frontdoor system averages treatment-weighted outcome regressions over the arm-specific mediator distribution, with the arm entering through that distribution.
The average treatment effect in a frontdoor system averages each unit's treated-minus-control potential-outcome contrast.
Definition (Lean source)
The observable frontdoor-adjusted ATE in a frontdoor system contrasts the adjusted mean under treatment with the adjusted mean under control.
Definition (Lean source)
Frontdoor identifying assumptions. Bundles, for a frontdoor system, factual consistency of the underlying potential-outcome system, composition consistency for the nested treatment–mediator regimes, 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)
Factual consistency assumption for the ambient PO system.
Composition consistency assumption for nested treatment–mediator regimes.
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 normalizedRestrictedIntegral 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). In a frontdoor system, the mean potential outcome under the selected arm equals its frontdoor functional for the treatment arm, under the frontdoor identifying assumption bundle. The functional combines the arm-specific mediator distribution with the outcome regression on mediator and treatment.
Formal statement
Proof (Lean source)
Frontdoor identification of the ATE. In a frontdoor system, 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 — In a frontdoor system, the potential outcome under a treatment arm is measurable, so its population mean can define the total effect.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 — In a frontdoor system, the potential mediator under a treatment arm is measurable, so its distribution can weight the adjustment formula.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 — In a frontdoor system, the potential outcome under a treatment arm and mediator level is measurable, so joint-intervention means are well-defined.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 — Observed treatment in a frontdoor system is measurable, so treatment-arm events and probabilities are well-defined.hypothesesconclusionMeasurable S.factualAProof (Lean source)
@[fun_prop] lemma measurable_factualA : Measurable S.factualA := S.aVar.measurable_factual -
measurable_factualMlemma — The observed mediator in a frontdoor system is measurable, so mediator cells can be used in the adjustment formula.hypothesesconclusionMeasurable S.factualMProof (Lean source)
@[fun_prop] lemma measurable_factualM : Measurable S.factualM := S.mVar.measurable_factual -
measurable_factualYlemma — Observed outcome in a frontdoor system is measurable, so treatment–mediator cell means are valid.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_aEventlemma — In a frontdoor system, an observed treatment arm defines a measurable event suitable for probabilities and conditional means.hypothesesconclusionMeasurableSet (S.aEvent a)Proof (Lean source)
lemma measurableSet_aEvent (a : Bool) : MeasurableSet (S.aEvent a) := S.aVar.measurableSet_event _ (measurableSet_singleton _) -
measurableSet_mEventlemma — In a frontdoor system, an observed mediator level defines a measurable event suitable for cell probabilities and conditional means.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, Finset.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 — In a frontdoor system, consistency and integrability of every joint treatment–mediator potential outcome imply that the observed outcome has a finite population mean; the observed treatment–mediator cell selects one of the integrable counterfactuals.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.CompositionConsistencya :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.CompositionConsistency) (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, Finset.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 normalizedRestrictedIntegral.hypothesesconclusion∫ ω, g ω ∂P.μProof (Lean source)
lemma integral_eq_sum_eventCondExp_aEvent (g : P.Ω → ℝ) (hg : Integrable g P.μ) : ∫ ω, g ω ∂P.μ = ∑ a' : Bool, normalizedRestrictedIntegral P.μ (S.aEvent a') g * (P.μ (S.aEvent a')).toReal := by -- Rewrite each RHS term as a set integral. have hterm : ∀ a' : Bool, normalizedRestrictedIntegral P.μ (S.aEvent a') g * (P.μ (S.aEvent a')).toReal = ∫ ω in S.aEvent a', g ω ∂P.μ := by intro a' exact eventCondExp_mul_measure_toReal P.μ (S.aEvent a') (measure_ne_top _ _) g -- Swap the sum to set-integrals. have hsum : ∑ a' : Bool, normalizedRestrictedIntegral 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.
The binary instrument variable exposes the instrument node of an IV system on the zero-one scale used by the LATE model.
Definition (Lean source)
The binary treatment variable exposes the treatment node of an IV system on the zero-one scale used to define compliance types.
Definition (Lean source)
The real-valued outcome variable exposes the outcome node of an IV system on the scale over which treatment effects are averaged.
Definition (Lean source)
The instrument intervention fixes an IV system at one binary instrument value, defining the counterfactual world used for the first stage.
Definition (Lean source)
The treatment intervention fixes an IV system at one binary treatment value, defining the counterfactual world used for causal outcomes.
Definition (Lean source)
Potential treatment records what each unit in the IV system would choose under a fixed binary instrument value, which determines compliance type.
Definition (Lean source)
Potential outcome records what each unit in the IV system would experience under a fixed binary treatment value, the primitive contrast averaged by LATE.
Definition (Lean source)
The observed instrument extracts each unit's realized assignment from the IV system.
Definition (Lean source)
The observed treatment extracts each unit's realized uptake from the IV system.
Definition (Lean source)
The observed outcome extracts each unit's realized response from the IV system.
Definition (Lean source)
The complier population in a binary IV system consists of units induced into treatment by switching the instrument on and not treated when it is off.
An observed instrument cell selects units in the IV system whose realized instrument equals the chosen binary value.
Definition (Lean source)
Outcome under instrument-induced treatment selects each unit's treated or untreated potential outcome in the IV system according to uptake under the chosen instrument value.
Definition (Lean source)
The observed first-stage cell mean averages treatment uptake in the IV system among units receiving the selected instrument value.
Definition (Lean source)
The observed reduced-form cell mean averages outcomes in the IV system among units receiving the selected instrument value.
Definition (Lean source)
Treatment under an instrument intervention packages the treatment response in the IV system with the assignment value that generates it, enabling exogeneity statements about that counterfactual.
Definition (Lean source)
Outcome under a treatment intervention packages the potential response in the IV system with the treatment arm that generates it, enabling joint exogeneity statements.
Definition (Lean source)
The full LATE counterfactual bundle collects both potential treatments and both potential outcomes from the binary IV system, making instrument independence a single joint assumption.
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).
The local average treatment effect in a binary IV system is the mean treated- versus-untreated outcome contrast among compliers, with the zero convention when that population 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 — Potential treatment under a fixed instrument value is measurable, so the IV system admits probabilities and expectations involving treatment response to that value.Proof (Lean source)
@[fun_prop] lemma measurable_DofZ (z : Bool) : Measurable (S.DofZ z) := S.dVar.measurable_cfUnder S.zVar z -
measurable_factualZlemma — The observed instrument is measurable, making its assignment cells observable in the IV system.Proof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The observed treatment is measurable, so treatment-cell probabilities are defined for the IV system.Proof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable, so its population moments are defined for the IV system.Proof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_YofDlemma — Potential outcome under a fixed treatment value is measurable, permitting causal outcome averages in the IV system for that treatment arm.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 population is a measurable event, so the IV system assigns it a probability and supports complier-conditional outcome means. -
measurableSet_zEventlemma — Each observed instrument cell is measurable, allowing the IV system to condition observed moments on the selected assignment.hypothesesconclusionMeasurableSet (S.zEvent z)Proof (Lean source)
lemma measurableSet_zEvent (z : Bool) : MeasurableSet (S.zEvent z) := S.zVar.measurableSet_event _ (measurableSet_singleton _) -
YofDofZ_deflemma — Instrument-induced outcome equals the treated potential outcome when uptake occurs and the untreated potential outcome otherwise in the IV system under the selected instrument value.hypotheses -
DofZ_eq_factualD_on_zEventlemma — Consistency identifies potential treatment with observed treatment for an IV system satisfying the identifying assumptions, at an instrument value, and for a unit observed in that instrument cell.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 — Consistency identifies each observed outcome with the potential outcome under realized treatment for an IV system satisfying the identifying assumptions and the unit being evaluated.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 — The observed first-stage contrast equals the complier share under the binary-IV identifying assumptions when both instrument-on and instrument-off cells have positive probability. Monotonicity is needed to exclude cancellation by defiers.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 = normalizedRestrictedIntegral P.μ (S.zVar.event z) (fun ω => ((S.factualD ω).toNat : ℝ)) := rfl rw [hbridge, POSystem.eventCondExp_of_ae_eq_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 — The observed outcome contrast across instrument cells equals the population contrast between instrument-induced potential outcomes under the binary-IV identifying assumptions, positive instrument-on and instrument-off cells, and integrable treated and untreated potential outcomes.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 = normalizedRestrictedIntegral P.μ (S.zVar.event z) S.factualY := rfl rw [hbridge, POSystem.eventCondExp_of_ae_eq_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 — The instrument-induced outcome change equals the treatment effect on compliers and vanishes for everyone else, almost surely under the binary-IV identifying assumptions. This isolates the population whose effect survives in the reduced form.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 — The population mean of the complier-restricted treatment effect factors into the complier share times LATE for the binary IV system, converting the reduced-form numerator into the target estimand.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 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] simpa [mul_comm] using (eventCondExp_mul_measure_toReal P.μ S.complierEvent (measure_ne_top _ _) (fun ω => S.YofD true ω - S.YofD false ω)).symm