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)
The continuous treatment variable in a partially linear potential-outcome system represents dose on the real line, within the ambient potential-outcome population and covariate space.
Definition (Lean source)
The real-valued outcome variable in a partially linear potential-outcome system is the response modeled as baseline plus a linear dose effect and error, within the ambient population and covariate space.
Definition (Lean source)
The adjustment covariate variable in a partially linear potential-outcome system retains its original measurable value space inside the ambient population and covariate space.
Definition (Lean source)
The dose-response potential outcome in a partially linear system records each unit's response if treatment were set to the selected dose; the real-valued dose varies continuously in the ambient population with covariates.
Definition (Lean source)
The observed treatment dose in a partially linear system records each unit's realized continuous treatment in the ambient population with covariates.
Definition (Lean source)
The observed outcome in a partially linear system records each unit's realized response in the ambient population with covariates.
Definition (Lean source)
The observed covariate in a partially linear system records each unit's realized adjustment value in the ambient population and covariate space.
Definition (Lean source)
The covariate information set in a partially linear system is generated by the observed adjustment covariate in the ambient population with covariate space.
Definition (Lean source)
The observed covariate–dose state in a partially linear system pairs each unit's covariate with its realized treatment dose in the ambient population and covariate space.
Definition (Lean source)
The joint covariate–treatment information set in a partially linear system is generated by observed covariates and the realized dose, in the ambient population with covariate space; this is the information set on which the structural error must have mean zero.
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 — In a partially linear system, the potential outcome at a fixed dose is measurable, so dose-specific means and conditional means are well-defined.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 realized dose in a partially linear system is measurable, so it can enter the observed treatment–covariate information set.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The observed response in a partially linear system is measurable, so its conditional regression is well-defined.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_factualXlemma — The observed covariate in a partially linear system is measurable, so it can generate the adjustment information set.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 partially linear system is contained in the full observable σ-algebra, so covariate-measurable quantities are also valid random variables on the population.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 partially linear system is measurable using only the information it generates, which licenses conditioning on covariates.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 observed covariate–dose state in a partially linear system is measurable, so it can index the backdoor conditional mean.hypothesesconclusionMeasurable S.factualXDProof (Lean source)
@[fun_prop] lemma measurable_factualXD : Measurable S.factualXD := S.measurable_factualX.prodMk S.measurable_factualD -
sigmaXD_lelemma — The covariate–treatment information set in a partially linear system is contained in the full observable σ-algebra, so conditioning on both variables is well-defined.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–dose state in a partially linear system is measurable using only its jointly generated information.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 in a partially linear system is available in the joint covariate–treatment information set.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 realized dose in a partially linear system is available in the joint covariate–treatment information set.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 information set in a partially linear system is coarser than the joint covariate–treatment information set, enabling the conditional- expectation tower used for partialling out.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.
The treatment nuisance regression in a partially linear model predicts the realized dose from observed covariates in the ambient potential-outcome population with covariate space.
Definition (Lean source)
The outcome nuisance regression in a partially linear model predicts the observed response from covariates alone in the ambient potential-outcome population with covariate space.
Definition (Lean source)
The residualized treatment in a partially linear model removes the covariate-predicted component from the realized dose, isolating variation orthogonal to covariates in the ambient population with covariate space.
Definition (Lean source)
The causal bridge. In a partially linear causal model, the Robinson partialling-out estimand equals the structural treatment effect θ when the treatment has residual variation, i.e. E[(D − m₀(X))²] ≠ 0, the factual treatment is integrable, the structural covariate baseline b(X) 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. 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