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 · 9 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)
The treatment regarded as a real-valued potential-outcome variable.
Definition (Lean source)
The outcome regarded as a real-valued potential-outcome variable.
Definition (Lean source)
The covariate regarded as a potential-outcome variable.
Definition (Lean source)
The potential outcome under dose d: the value the outcome would take were the treatment set to the real number d.
Definition (Lean source)
The factual (observed) treatment level of each unit.
Definition (Lean source)
The factual (observed) outcome of each unit.
Definition (Lean source)
The factual (observed) covariate of each unit.
Definition (Lean source)
The σ-algebra generated by the observed covariate.
Definition (Lean source)
The joint observed covariate-and-treatment map ω ↦ (X(ω), D(ω)).
Definition (Lean source)
The σ-algebra generated by the observed covariate and treatment jointly.
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)
9 supporting declarations (lemmas, instances)
-
measurable_YofDlemma — The potential outcome under a fixed dose is measurable.Proof (Lean source)
lemma measurable_YofD (d : ℝ) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_factualDlemma — The factual treatment level is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_factualXlemma — The factual covariate is measurable.conclusionMeasurable S.factualXProof (Lean source)
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.conclusionS.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaX_le : S.sigmaX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualX.comap_le -
measurable_factualXDlemma — The joint observed covariate-and-treatment map is measurable.conclusionMeasurable S.factualXDProof (Lean source)
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.conclusionS.sigmaXD ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigmaXD_le : S.sigmaXD ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_factualXD.comap_le -
sigmaX_le_sigmaXDlemma — The covariate σ-algebra is contained in the joint covariate-treatment σ-algebra.conclusionS.sigmaX ≤ S.sigmaXD -
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).conclusionM.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.
The treatment regression m₀(X) = E[D | σ(X)] (the conditional mean of the treatment given the covariate).
Definition (Lean source)
The outcome regression ℓ₀(X) = E[Y | σ(X)] (the conditional mean of the outcome given the covariate).
Definition (Lean source)
The treatment residual V = D − m₀(X) (treatment with its covariate prediction partialled out).
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).conclusionP.μ[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.Proof (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] := MeasureTheory.condExp_sub hD MeasureTheory.integrable_condExp M.sigmaX 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).hypotheseshU :Integrable M.U P.μhUV :Integrable (fun ω => M.U ω * M.resid ω) P.μconclusion∫ ω, 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 have heq : M.factualD = snd ∘ M.factualXD := rfl rw [heq] exact (measurable_snd.comp (comap_measurable M.factualXD)).stronglyMeasurable 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.hypotheseshD :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] := MeasureTheory.condExp_add (hbX_int.add hθD_int) hU M.sigmaX 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] := MeasureTheory.condExp_add hbX_int hθD_int M.sigmaX 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] := MeasureTheory.condExp_smul M.θ M.factualD M.sigmaX 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.hypotheseshD :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.hypotheseshD :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 ω) ?_] · rw [integral_add (hVsq.const_mul M.θ) hUV, integral_const_mul, M.integral_U_resid hU hUV, add_zero] · filter_upwards [M.factualY_sub_lReg hD hbX hU] with ω h rw [h]; ring