PO.ID.Exact.PartialLinear
Partially linear continuous-treatment identification: the potential-outcome setup, homogeneous dose-response restriction, Robinson residualization, and slope-identification theorem.
Setup 13 core · 13 supporting This file provides the potential-outcome substrate for the partially linear model with a real-valued treatment. ★ POPartialLinearSystem★ POPartialLinearModel★ causal_homogeneity
Partially Linear Model Setup
This file provides the potential-outcome substrate for the partially linear
model with a real-valued treatment. POPartialLinearSystem records the
treatment, outcome, and covariate nodes; packages them as dVar, yVar, and
xVar; defines potential outcomes YofD, factual maps, and the sigma-algebras
sigmaX and sigmaXD; and proves the measurability and inclusion lemmas used
by the identification proof.
POPartialLinearModel adds the homogeneous structural restriction
Y(d) = b(X) + theta * d + U, a conditional-mean backdoor assumption, and
consistency. Its two exported consequences are factualY_eq, the observed-data
regression form, and causal_homogeneity, the constant per-unit causal effect
identity.
Continuous-treatment backdoor subsystem. Inside a potential-outcome system, this bundles a real-valued treatment node D, a real-valued outcome node Y, and a covariate variable X taking values in an arbitrary measurable space, subject to the treatment, outcome, and covariate being pairwise distinct. This mirrors the binary backdoor subsystem but the treatment now ranges over the real line, as required by the partially linear model Y = g(X) + θ·D + noise.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the treatment variable is its treatment represented as a real-valued potential-outcome variable.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the outcome variable is its outcome represented as a real-valued potential-outcome variable.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the covariate variable is its covariate represented as a potential-outcome variable.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, a partially linear potential-outcome system based on them, and a real-valued treatment dose, the potential outcome at that dose assigns each unit the outcome it would have if treatment were set to that dose.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the observed treatment level assigns each unit its realized real-valued treatment.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the observed outcome assigns each unit its realized outcome.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the observed covariate assigns each unit its realized covariate value.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the covariate σ-algebra is the σ-algebra on the sample space generated by the observed covariate.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the joint observed covariate-and-treatment map assigns each unit the pair consisting of its observed covariate and observed treatment level.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome system based on them, the joint covariate-treatment σ-algebra is the σ-algebra on the sample space generated jointly by the observed covariate and treatment.
Definition (Lean source)
Partially linear model under the backdoor PO framework. On top of the PO substrate, this bundles a measurable covariate function b giving the nonparametric baseline, a homogeneous per-unit treatment effect θ, a measurable structural error term U, the structural restriction that every unit's dose-response is the straight line Y(d) = b(X) + θ·d + U with the same slope for everyone, the standard backdoor (unconfoundedness) assumption that the structural error has zero mean conditional on the observed covariate and treatment, and consistency: the observed outcome is the potential outcome at the realized treatment.
Definition (Lean source)
Causal reading of θ. Almost surely, for every pair of dose levels, the difference of the corresponding potential outcomes equals the slope θ times the difference of the doses, so θ is the constant per-unit causal effect of the treatment.
Formal statement
Proof (Lean source)
13 supporting declarations (lemmas, instances)
-
measurable_YofDlemma — The potential outcome under a fixed dose is measurable.hypothesesconclusionMeasurable (S.YofD d)Proof (Lean source)
@[fun_prop] lemma measurable_YofD (d : ℝ) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_factualDlemma — The factual treatment level is measurable.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_factualXlemma — The factual covariate is measurable.hypothesesconclusionMeasurable S.factualXProof (Lean source)
@[fun_prop] lemma measurable_factualX : Measurable S.factualX := S.xVar.measurable_factual -
sigmaX_lelemma — The covariate-generated sigma-algebra is a sub-sigma-algebra of the ambient space.hypothesesconclusionS.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaX_le : S.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualX.comap_le -
measurable_factualX_sigmaXlemma — The observed covariate is measurable for the covariate sigma-algebra it generates.hypothesesconclusionMeasurable[S.sigmaX] S.factualXProof (Lean source)
@[fun_prop] lemma measurable_factualX_sigmaX : Measurable[S.sigmaX] S.factualX := comap_measurable S.factualX -
measurable_factualXDlemma — The joint observed covariate-and-treatment map is measurable.hypothesesconclusionMeasurable S.factualXDProof (Lean source)
@[fun_prop] lemma measurable_factualXD : Measurable S.factualXD := S.measurable_factualX.prodMk S.measurable_factualD -
sigmaXD_lelemma — The joint covariate-treatment sigma-algebra is a sub-sigma-algebra of the ambient space.hypothesesconclusionS.sigmaXD ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaXD_le : S.sigmaXD ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualXD.comap_le -
measurable_factualXD_sigmaXDlemma — The observed covariate-treatment pair is measurable for the joint sigma-algebra it generates.hypothesesconclusionMeasurable[S.sigmaXD] S.factualXDProof (Lean source)
@[fun_prop] lemma measurable_factualXD_sigmaXD : Measurable[S.sigmaXD] S.factualXD := comap_measurable S.factualXD -
measurable_factualX_sigmaXDlemma — The observed covariate is measurable for the joint covariate-treatment sigma-algebra.hypothesesconclusionMeasurable[S.sigmaXD] S.factualXProof (Lean source)
@[fun_prop] lemma measurable_factualX_sigmaXD : Measurable[S.sigmaXD] S.factualX := measurable_fst.comp (comap_measurable S.factualXD) -
measurable_factualD_sigmaXDlemma — The observed treatment is measurable for the joint covariate-treatment sigma-algebra.hypothesesconclusionMeasurable[S.sigmaXD] S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD_sigmaXD : Measurable[S.sigmaXD] S.factualD := measurable_snd.comp (comap_measurable S.factualXD) -
sigmaX_le_sigmaXDlemma — The covariate σ-algebra is contained in the joint covariate-treatment σ-algebra.hypothesesconclusionS.sigmaX ≤ S.sigmaXDProof (Lean source)
lemma sigmaX_le_sigmaXD : S.sigmaX ≤ S.sigmaXD := by have h : S.factualX = fst ∘ S.factualXD := rfl unfold sigmaX sigmaXD rw [h, ← MeasurableSpace.comap_comp] exact comap_mono measurable_fst.comap_le -
factualY_eqlemma — The observed-data form of the structural model: almost surely Y = b(X) + θ·D + U. Obtained from the homogeneous dose-response evaluated at the realized treatment, using consistency Y = Y(D).hypothesesconclusionM.factualY =ᵐ[P.μ] fun ω => M.b (M.factualX ω) + M.θ * M.factualD ω + M.U ωProof (Lean source)
lemma factualY_eq : M.factualY =ᵐ[P.μ] fun ω => M.b (M.factualX ω) + M.θ * M.factualD ω + M.U ω := by filter_upwards [M.structural] with ω hω have hcons : M.yVar.factual ω = M.yVar.cfUnder M.dVar (M.dVar.factual ω) ω := POVar.factual_eq_cfUnder_self_selected M.consistency M.yVar M.dVar (Ne.symm M.hDY) ω have hstr := hω (M.factualD ω) simpa [POPartialLinearSystem.factualY, POPartialLinearSystem.YofD, POPartialLinearSystem.factualD, POPartialLinearSystem.factualX] using hcons.trans hstr
Identification 4 core · 6 supporting This file proves the population partialling-out bridge for the partially linear potential-outcome model. ★ robinson_estimand_eq_theta
Partialling-out identification
This file proves the population partialling-out bridge for the partially
linear potential-outcome model. It defines the covariate regressions mReg and
lReg, the treatment residual resid, and then proves the conditional
mean-zero and orthogonality identities that drive Robinson's identification
argument.
The important lemmas are condExp_U_sigmaX, condExp_resid_sigmaX,
integral_U_resid, lReg_eq, factualY_sub_lReg, and integral_partialled.
The main theorem robinson_estimand_eq_theta states that the population
Robinson ratio
E[(Y - lReg(X)) * (D - mReg(X))] / E[(D - mReg(X))^2] equals the structural
slope theta when the residual second moment is nonzero.
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome model based on them, the treatment regression assigns each unit the conditional mean of its observed treatment given the σ-algebra generated by the observed covariate.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome model based on them, the outcome regression assigns each unit the conditional mean of its observed outcome given the σ-algebra generated by the observed covariate.
Definition (Lean source)
For a potential-outcome system, a measurable covariate space, and a partially linear potential-outcome model based on them, the treatment residual assigns each unit its observed treatment minus its treatment regression given the observed covariate.
Definition (Lean source)
The causal bridge. Given that the factual treatment is integrable, the outcome regression on covariates is integrable, the structural error U is integrable, the squared treatment residual is integrable, and the product of the structural error and the treatment residual is integrable, provided also that the treatment has residual variation, i.e. E[(D − m₀(X))²] ≠ 0, the Robinson partialling-out estimand equals the structural treatment effect θ. This is what makes the partially linear DML estimator target the causal parameter.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
condExp_U_sigmaXlemma — The structural error has zero conditional mean given the covariate. Follows from the backdoor assumption E[U | σ(X,D)] = 0 by the tower property, since σ(X) ⊆ σ(X,D).hypothesesconclusionP.μ[M.U | M.sigmaX] =ᵐ[P.μ] 0Proof (Lean source)
lemma condExp_U_sigmaX : P.μ[M.U | M.sigmaX] =ᵐ[P.μ] 0 := by have htower : P.μ[P.μ[M.U | M.sigmaXD] | M.sigmaX] =ᵐ[P.μ] P.μ[M.U | M.sigmaX] := MeasureTheory.condExp_condExp_of_le M.sigmaX_le_sigmaXD M.sigmaXD_le have hinner : P.μ[P.μ[M.U | M.sigmaXD] | M.sigmaX] =ᵐ[P.μ] P.μ[(0 : P.Ω → ℝ) | M.sigmaX] := MeasureTheory.condExp_congr_ae M.backdoor refine htower.symm.trans (hinner.trans ?_) simp [MeasureTheory.condExp_zero] -
condExp_resid_sigmaXlemma — The treatment residual is conditionally mean-zero given the covariate: E[D − m₀(X) | σ(X)] = 0. Immediate from condExp_sub and idempotence of the conditional expectation.hypothesesγ :sharedType u_1hD :Integrable M.factualD P.μconclusionP.μ[M.resid | M.sigmaX] =ᵐ[P.μ] 0Proof (Lean source)
lemma condExp_resid_sigmaX (hD : Integrable M.factualD P.μ) : P.μ[M.resid | M.sigmaX] =ᵐ[P.μ] 0 := by have hresid_eq : M.resid = M.factualD - M.mReg := rfl rw [hresid_eq] have hsub : P.μ[M.factualD - M.mReg | M.sigmaX] =ᵐ[P.μ] P.μ[M.factualD | M.sigmaX] - P.μ[M.mReg | M.sigmaX] := by condexp_linearity [MeasureTheory.integrable_condExp (μ := P.μ) (m := M.sigmaX) (f := M.factualD)] have hidem : P.μ[M.mReg | M.sigmaX] =ᵐ[P.μ] M.mReg := by unfold mReg exact MeasureTheory.condExp_condExp_of_le le_rfl M.sigmaX_le refine hsub.trans ?_ have : P.μ[M.factualD | M.sigmaX] = M.mReg := rfl rw [this] filter_upwards [hidem] with ω hω simp [Pi.sub_apply, hω] -
integral_U_residlemma — Orthogonality of the structural error to the covariate-treatment residual: E[U·(D − m₀(X))] = 0. Since the residual is σ(X,D)-measurable and E[U | σ(X,D)] = 0, the product integrates to zero (pull the residual out of the conditional expectation, then integrate).hypothesesconclusion∫ ω, M.U ω * M.resid ω ∂P.μ = 0Proof (Lean source)
lemma integral_U_resid (hU : Integrable M.U P.μ) (hUV : Integrable (fun ω => M.U ω * M.resid ω) P.μ) : ∫ ω, M.U ω * M.resid ω ∂P.μ = 0 := by -- `resid = D − mReg` is `σ(X,D)`-strongly-measurable. have hD_sm : StronglyMeasurable[M.sigmaXD] M.factualD := by fun_prop have hmReg_sm : StronglyMeasurable[M.sigmaXD] M.mReg := by refine MeasureTheory.stronglyMeasurable_condExp.mono M.sigmaX_le_sigmaXD have hresid_sm : StronglyMeasurable[M.sigmaXD] M.resid := by have : M.resid = fun ω => M.factualD ω - M.mReg ω := rfl rw [this] exact hD_sm.sub hmReg_sm -- Rewrite `U·resid` as `resid·U` (integrable up to commutativity). have hVU_int : Integrable (fun ω => M.resid ω * M.U ω) P.μ := by simpa [mul_comm] using hUV -- `∫ U·resid = ∫ resid·U = ∫ μ[resid·U | σ(X,D)] = ∫ resid·μ[U|σ(X,D)] = ∫ resid·0 = 0`. have hpull : P.μ[fun ω => M.resid ω * M.U ω | M.sigmaXD] =ᵐ[P.μ] M.resid * P.μ[M.U | M.sigmaXD] := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := M.sigmaXD) hresid_sm hVU_int hU have hce_zero : P.μ[fun ω => M.resid ω * M.U ω | M.sigmaXD] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by refine hpull.trans ?_ filter_upwards [M.backdoor] with ω hω rw [Pi.mul_apply, hω, Pi.zero_apply, mul_zero] calc ∫ ω, M.U ω * M.resid ω ∂P.μ = ∫ ω, M.resid ω * M.U ω ∂P.μ := by simp_rw [mul_comm] _ = ∫ ω, P.μ[fun ω => M.resid ω * M.U ω | M.sigmaXD] ω ∂P.μ := by rw [MeasureTheory.integral_condExp M.sigmaXD_le] _ = ∫ _, (0 : ℝ) ∂P.μ := MeasureTheory.integral_congr_ae hce_zero _ = 0 := MeasureTheory.integral_zero _ _ -
lReg_eqlemma — The outcome regression decomposes as ℓ₀(X) = b(X) + θ·m₀(X). Apply the conditional expectation given σ(X) to the observed-data form Y = b(X) + θ·D + U: the covariate term is σ(X)-measurable, the treatment term contributes θ·m₀(X), and the error term vanishes by condExp_U_sigmaX.hypothesesγ :sharedType u_1hD :Integrable M.factualD P.μhbX :Integrable (fun ω => M.b (M.factualX ω)) P.μhU :Integrable M.U P.μconclusionM.lReg =ᵐ[P.μ] fun ω => M.b (M.factualX ω) + M.θ * M.mReg ωProof (Lean source)
lemma lReg_eq (hD : Integrable M.factualD P.μ) (hbX : Integrable (fun ω => M.b (M.factualX ω)) P.μ) (hU : Integrable M.U P.μ) : M.lReg =ᵐ[P.μ] fun ω => M.b (M.factualX ω) + M.θ * M.mReg ω := by have hbX_int : Integrable (fun ω => M.b (M.factualX ω)) P.μ := hbX have hθD_int : Integrable (fun ω => M.θ * M.factualD ω) P.μ := hD.const_mul M.θ -- σ(X)-strong-measurability of the covariate term. have hbX_sm : StronglyMeasurable[M.sigmaX] (fun ω => M.b (M.factualX ω)) := by change StronglyMeasurable[comap M.factualX inferInstance] (fun ω => M.b (M.factualX ω)) exact (M.b_meas.comp (comap_measurable M.factualX)).stronglyMeasurable -- Rewrite Y by the observed-data form, then split the conditional expectation. have hY : M.lReg =ᵐ[P.μ] P.μ[fun ω => (M.b (M.factualX ω) + M.θ * M.factualD ω) + M.U ω | M.sigmaX] := by unfold lReg refine MeasureTheory.condExp_congr_ae ?_ filter_upwards [M.factualY_eq] with ω hω simpa using hω have hsplit1 : P.μ[fun ω => (M.b (M.factualX ω) + M.θ * M.factualD ω) + M.U ω | M.sigmaX] =ᵐ[P.μ] P.μ[fun ω => M.b (M.factualX ω) + M.θ * M.factualD ω | M.sigmaX] + P.μ[M.U | M.sigmaX] := by condexp_linearity have hsplit2 : P.μ[fun ω => M.b (M.factualX ω) + M.θ * M.factualD ω | M.sigmaX] =ᵐ[P.μ] P.μ[fun ω => M.b (M.factualX ω) | M.sigmaX] + P.μ[fun ω => M.θ * M.factualD ω | M.sigmaX] := by condexp_linearity have hbXce : P.μ[fun ω => M.b (M.factualX ω) | M.sigmaX] = fun ω => M.b (M.factualX ω) := MeasureTheory.condExp_of_stronglyMeasurable M.sigmaX_le hbX_sm hbX_int have hθDce : P.μ[fun ω => M.θ * M.factualD ω | M.sigmaX] =ᵐ[P.μ] fun ω => M.θ * M.mReg ω := by have hsmul : P.μ[fun ω => M.θ • M.factualD ω | M.sigmaX] =ᵐ[P.μ] M.θ • P.μ[M.factualD | M.sigmaX] := by condexp_linearity refine hsmul.trans ?_ filter_upwards with ω simp [Pi.smul_apply, mReg, smul_eq_mul] rw [hbXce] at hsplit2 refine hY.trans (hsplit1.trans ?_) filter_upwards [hsplit2, hθDce, M.condExp_U_sigmaX] with ω h2 hθd hu rw [Pi.add_apply, h2, Pi.add_apply, hθd, hu] simp -
factualY_sub_lReglemma — Partialling-out identity (observed data): Y − ℓ₀(X) = θ·(D − m₀(X)) + U. Algebraic consequence of factualY_eq and lReg_eq.hypothesesγ :sharedType u_1hD :Integrable M.factualD P.μhbX :Integrable (fun ω => M.b (M.factualX ω)) P.μhU :Integrable M.U P.μconclusion(fun ω => M.factualY ω - M.lReg ω) =ᵐ[P.μ] fun ω => M.θ * M.resid ω + M.U ωProof (Lean source)
lemma factualY_sub_lReg (hD : Integrable M.factualD P.μ) (hbX : Integrable (fun ω => M.b (M.factualX ω)) P.μ) (hU : Integrable M.U P.μ) : (fun ω => M.factualY ω - M.lReg ω) =ᵐ[P.μ] fun ω => M.θ * M.resid ω + M.U ω := by filter_upwards [M.factualY_eq, M.lReg_eq hD hbX hU] with ω hY hl rw [hY, hl] simp only [resid] ring -
integral_partialledlemma — The Robinson numerator equals θ times the residual second moment: E[(Y − ℓ₀(X))·(D − m₀(X))] = θ·E[(D − m₀(X))²]. Expand Y − ℓ₀ = θ·V + U and use E[U·V] = 0.hypothesesγ :sharedType u_1hD :Integrable M.factualD P.μhbX :Integrable (fun ω => M.b (M.factualX ω)) P.μhU :Integrable M.U P.μhVsq :Integrable (fun ω => M.resid ω ^ 2) P.μhUV :Integrable (fun ω => M.U ω * M.resid ω) P.μconclusion∫ ω, (M.factualY ω - M.lReg ω) * M.resid ω ∂P.μ = M.θ * ∫ ω, M.resid ω ^ 2 ∂P.μProof (Lean source)
lemma integral_partialled (hD : Integrable M.factualD P.μ) (hbX : Integrable (fun ω => M.b (M.factualX ω)) P.μ) (hU : Integrable M.U P.μ) (hVsq : Integrable (fun ω => M.resid ω ^ 2) P.μ) (hUV : Integrable (fun ω => M.U ω * M.resid ω) P.μ) : ∫ ω, (M.factualY ω - M.lReg ω) * M.resid ω ∂P.μ = M.θ * ∫ ω, M.resid ω ^ 2 ∂P.μ := by rw [integral_congr_ae (g := fun ω => M.θ * M.resid ω ^ 2 + M.U ω * M.resid ω) ?_] · integral_linearity rw [M.integral_U_resid hU hUV, add_zero] · filter_upwards [M.factualY_sub_lReg hD hbX hU] with ω h rw [h]; ring