PO.ID.Exact.Proximal
Proximal causal inference: identification through outcome- and treatment-confounding proxies via bridge functions.
Setup 17 core · 14 supporting This file defines the data layer for proximal average treatment effect identification. ★ POProximalSystem★ σ_UX_le
Proximal Setup
This file defines the data layer for proximal average treatment effect
identification. POProximalSystem records a covariate, binary treatment,
treatment-side proxy, outcome-side proxy, real-valued outcome, and latent
confounder. The namespace then supplies the factual maps X, A, Z, W,
Y, and U; the treatment-specific potential outcome YofA; tuple-valued
conditioning targets AZX, AUX, UX, and AZUX; and the generated
sigma-algebras σ_AZX, σ_AUX, σ_UX, and σ_AZUX with their ambient
sub-sigma-algebra lemmas.
Assumption bundles and the identification theorem are kept in the companion
Proximal.Assumptions and Proximal.Main files.
structure POProximalSystem reviewed
⚑ flagged
Causalean.PO
Proximal ATE system. Bundles six distinguished potential-outcome variables inside a potential-outcome system: an observed covariate, a binary treatment, a treatment-side proxy, an outcome-side proxy, a real-valued outcome, and a latent confounder (def:po-proximal-system).
Definition (Lean source)
parameters
P :
γ_X γ_Z γ_W γ_U :
def X reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Factual covariate X = Xvar(r∅).
Definition (Lean source)
noncomputable def X : P.Ω → γ_X := S.Xvar.factual
def A reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Factual treatment A = Avar(r∅).
Definition (Lean source)
noncomputable def A : P.Ω → Bool := S.Avar.factual
def Z reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Factual treatment-side proxy Z = Zvar(r∅).
Definition (Lean source)
noncomputable def Z : P.Ω → γ_Z := S.Zvar.factual
def W reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Factual outcome-side proxy W = Wvar(r∅).
Definition (Lean source)
noncomputable def W : P.Ω → γ_W := S.Wvar.factual
def Y reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Factual outcome Y = Yvar(r∅).
Definition (Lean source)
noncomputable def Y : P.Ω → ℝ := S.Yvar.factual
def U reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Latent confounder U = Uvar(r∅).
Definition (Lean source)
noncomputable def U : P.Ω → γ_U := S.Uvar.factual
def YofA reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Treatment-specific potential outcome Y(a) := Yvar.cfUnder Avar a.
Definition (Lean source)
noncomputable def YofA (a : Bool) : P.Ω → ℝ := S.Yvar.cfUnder S.Avar a
def AZX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
(A, Z, X) : P.Ω → Bool × γ_Z × γ_X.
Definition (Lean source)
noncomputable def AZX : P.Ω → Bool × γ_Z × γ_X :=
fun ω => (S.A ω, S.Z ω, S.X ω)
def AUX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
(A, U, X) : P.Ω → Bool × γ_U × γ_X.
Definition (Lean source)
noncomputable def AUX : P.Ω → Bool × γ_U × γ_X :=
fun ω => (S.A ω, S.U ω, S.X ω)
def UX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
(U, X) : P.Ω → γ_U × γ_X.
Definition (Lean source)
noncomputable def UX : P.Ω → γ_U × γ_X :=
fun ω => (S.U ω, S.X ω)
def AZUX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
(A, Z, U, X) : P.Ω → Bool × γ_Z × γ_U × γ_X.
Definition (Lean source)
noncomputable def AZUX : P.Ω → Bool × γ_Z × γ_U × γ_X :=
fun ω => (S.A ω, S.Z ω, S.U ω, S.X ω)
def σ_AZX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
σ-algebra generated by (A, Z, X).
Definition (Lean source)
def σ_AUX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
σ-algebra generated by (A, U, X).
Definition (Lean source)
def σ_UX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
σ-algebra generated by (U, X).
Definition (Lean source)
def σ_AZUX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
σ-algebra generated by (A, Z, U, X).
Definition (Lean source)
lemma σ_UX_le reviewed
⚑ flagged
Causalean.PO.POProximalSystem
The σ-algebra generated by the latent confounder and covariate is a sub-σ-algebra of the ambient measurable space.
Formal statement
conclusion
S.σ_UX ≤ (inferInstance : MeasurableSpace P.Ω)
Proof (Lean source)
lemma σ_UX_le : S.σ_UX ≤ (inferInstance : MeasurableSpace P.Ω) :=
S.measurable_UX.comap_le
14 supporting declarations (lemmas, instances)
-
measurable_Xlemma — The factual covariate is measurable.conclusionMeasurable S.XProof (Lean source)
lemma measurable_X : Measurable S.X := S.Xvar.measurable_factual -
measurable_Alemma — The factual treatment is measurable.conclusionMeasurable S.AProof (Lean source)
lemma measurable_A : Measurable S.A := S.Avar.measurable_factual -
measurable_Zlemma — The factual treatment-side proxy is measurable.conclusionMeasurable S.ZProof (Lean source)
lemma measurable_Z : Measurable S.Z := S.Zvar.measurable_factual -
measurable_Wlemma — The factual outcome-side proxy is measurable.conclusionMeasurable S.WProof (Lean source)
lemma measurable_W : Measurable S.W := S.Wvar.measurable_factual -
measurable_Ylemma — The factual outcome is measurable.conclusionMeasurable S.YProof (Lean source)
lemma measurable_Y : Measurable S.Y := S.Yvar.measurable_factual -
measurable_Ulemma — The factual latent confounder is measurable.conclusionMeasurable S.UProof (Lean source)
lemma measurable_U : Measurable S.U := S.Uvar.measurable_factual -
measurable_YofAlemma — The treatment-specific potential outcome is measurable.Proof (Lean source)
lemma measurable_YofA (a : Bool) : Measurable (S.YofA a) := S.Yvar.measurable_cfUnder S.Avar a -
measurable_AZXlemma — The treatment, treatment-side proxy, and covariate tuple is measurable.conclusionMeasurable S.AZXProof (Lean source)
lemma measurable_AZX : Measurable S.AZX := prodMk S.measurable_A (prodMk S.measurable_Z S.measurable_X) -
measurable_AUXlemma — The treatment, latent confounder, and covariate tuple is measurable.conclusionMeasurable S.AUXProof (Lean source)
lemma measurable_AUX : Measurable S.AUX := prodMk S.measurable_A (prodMk S.measurable_U S.measurable_X) -
measurable_UXlemma — The latent confounder and covariate tuple is measurable.conclusionMeasurable S.UXProof (Lean source)
lemma measurable_UX : Measurable S.UX := prodMk S.measurable_U S.measurable_X -
measurable_AZUXlemma — The treatment, treatment-side proxy, latent confounder, and covariate tuple is measurable.conclusionMeasurable S.AZUXProof (Lean source)
lemma measurable_AZUX : Measurable S.AZUX := prodMk S.measurable_A (prodMk S.measurable_Z (prodMk S.measurable_U S.measurable_X)) -
σ_AZX_lelemma — The sigma-algebra generated by treatment, treatment-side proxy, and covariate is a sub-sigma-algebra of the ambient space.conclusionS.σ_AZX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma σ_AZX_le : S.σ_AZX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_AZX.comap_le -
σ_AUX_lelemma — The sigma-algebra generated by treatment, latent confounder, and covariate is a sub-sigma-algebra of the ambient space.conclusionS.σ_AUX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma σ_AUX_le : S.σ_AUX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_AUX.comap_le -
σ_AZUX_lelemma — The sigma-algebra generated by treatment, treatment-side proxy, latent confounder, and covariate is a sub-sigma-algebra of the ambient space.conclusionS.σ_AZUX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma σ_AZUX_le : S.σ_AZUX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_AZUX.comap_le
Assumptions 2 core · 0 supporting This file states the proximal proxy assumptions for average treatment effect identification. ★ integrable_Y
Proximal Assumptions
This file states the proximal proxy assumptions for average treatment effect
identification. POProximalSystem.Assumptions bundles consistency, latent
exchangeability, outcome-side and treatment-side proxy restrictions, an outcome
bridge equation, arm positivity, treatment-arm completeness, and the
integrability conditions needed for the bridge representation.
The assumptions follow the Miao, Geng, and Tchetgen Tchetgen proximal
identification setup. The only exported lemma, Assumptions.integrable_Y, is a
compatibility projection showing that factual outcome integrability follows
from consistency and integrability of the two potential-outcome cells.
structure Assumptions reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Proximal ATE assumption bundle (Miao–Geng–Tchetgen Tchetgen proximal identification, def:po-proximal-assumptions). For a proximal system with covariate, binary treatment, treatment-side and outcome-side proxies, outcome, and latent confounder, this packages consistency (SUTVA), latent exchangeability: each potential outcome is independent of treatment given the latent confounder and covariate, the two proxy restrictions that the outcome-side proxy carries no information about the outcome beyond treatment, latent confounder, and covariate and the treatment-side proxy is independent of treatment and the outcome-side proxy given the latent confounder and covariate, a measurable outcome bridge function h satisfying the bridge equation that the outcome minus h evaluated at treatment, outcome-side proxy, and covariate has zero mean conditional on treatment, treatment-side proxy, and covariate, a positivity condition that every latent-confounder-and-covariate- measurable event of positive probability meets each treatment arm with positive probability, a completeness condition that within each treatment arm, functions of the latent confounder and covariate with zero bridge-conditional mean vanish almost surely, and integrability of the two potential outcomes, the composite h(A,W,X), and the bridge function evaluated at each fixed treatment arm.
Definition (Lean source)
parameters
S :
POProximalSystem P γ_X γ_Z γ_W γ_U
μ :
Measure P.Ω := P.μ
fields
Consistency axiom for the ambient PO system.
consistency :
POSystem.Consistency P
Latent exchangeability: Y(a) ⟂ A | (U,X) for each treatment level.
latent_exch :
∀ a : Bool, CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μ
Proxy restriction (outcome side): Y ⟂ Z | (A,U,X).
proxy_YZ :
CondIndepFun S.σ_AUX S.σ_AUX_le S.Y S.Z μ
Proxy restriction (treatment side): W ⟂ (A,Z) | (U,X).
proxy_WAZ :
CondIndepFun S.σ_UX S.σ_UX_le S.W (fun ω => (S.A ω, S.Z ω)) μ
Bridge function h : Bool × γ_W × γ_X → ℝ.
h :
Bool × γ_W × γ_X → ℝ
h is measurable.
measurable_h :
h(A,W,X) is integrable under μ.
integrable_hAWX :
Integrable (fun ω => h (S.A ω, S.W ω, S.X ω)) μ
Outcome bridge: E[Y - h(A,W,X) | σ(A,Z,X)] = 0 a.s.
bridge :
(μ[fun ω => S.Y ω - h (S.A ω, S.W ω, S.X ω) | S.σ_AZX]) =ᵐ[μ] 0
Positivity (Miao-Geng-Tchetgen Tchetgen 2018, Assumption 7).
Every σ_UX-measurable set of positive μ-measure intersects each arm
`{A=a}` in a positive-measure subset. Equivalently (contrapositive):
if a σ_UX-measurable set `B` has μ-null intersection with the arm, then
`B` itself is μ-null.
This is the measure-zero form of `0 < P(A=a | U, X)` a.s., chosen because
it is consumed directly by the stratum-to-global lift in `Helpers.lean`
(see `eq_zero_globally_of_eq_zero_on_arm`).
positivity_arm :
Completeness within treatment level
(Miao-Geng-Tchetgen Tchetgen 2018, Assumption 8).
For each `a ∈ {0,1}` and every measurable `g : γ_U × γ_X → ℝ` integrable
on `μ.restrict {A=a}`,
if μ[g(U,X) | σ(A,Z,X)] = 0 a.s. on {A=a},
then g(U,X) = 0 a.s. on {A=a}.
Conclusion is **stratum-wise** (`=ᵐ[μ.restrict {A=a}]`), not global,
matching the classical pointwise-in-(a,x) statement under disintegration.
The global conclusion is recovered downstream (step 7 of `Main.lean`)
by combining this with `positivity_arm`.
completeness :
∀ (a : Bool) (g : γ_U × γ_X → ℝ)
if
and
Integrable (fun ω => g (S.UX ω)) (μ.restrict {ω | S.A ω = a})
and
(μ[fun ω => g (S.UX ω) | S.σ_AZX]) =ᵐ[μ.restrict {ω | S.A ω = a}] 0
then
(fun ω => g (S.UX ω)) =ᵐ[μ.restrict {ω | S.A ω = a}] 0
Integrability of Y(0).
integrable_YofA0 :
Integrable (S.YofA false) μ
Integrability of Y(1).
integrable_YofA1 :
Integrable (S.YofA true) μ
Integrability of h(0,W,X).
integrable_h0WX :
Integrable (fun ω => h (false, S.W ω, S.X ω)) μ
Integrability of h(1,W,X).
integrable_h1WX :
Integrable (fun ω => h (true, S.W ω, S.X ω)) μ
lemma integrable_Y reviewed
⚑ flagged
Causalean.PO.POProximalSystem.Assumptions
Compatibility projection. Under the proximal identifying assumption bundle, and given the treatment and outcome are distinct nodes, the factual outcome Y is integrable, as a consequence of the consistency assumption together with the integrability of the two potential-outcome cells Y(0) and Y(1).
Formal statement
Proof (Lean source)
lemma integrable_Y (HA : Assumptions S μ) (hAY : S.Avar.v ≠ S.Yvar.v) :
Integrable S.Y μ := by
have htrue_int : Integrable (fun ω => S.YofA true ω * S.Avar.indicator true ω) μ :=
integrable_mul_indicator S.Avar true HA.integrable_YofA1 (S.measurable_YofA true)
have hfalse_int : Integrable (fun ω => S.YofA false ω * S.Avar.indicator false ω) μ :=
integrable_mul_indicator S.Avar false HA.integrable_YofA0 (S.measurable_YofA false)
have hsum_int : Integrable
((fun ω => S.YofA true ω * S.Avar.indicator true ω) +
fun ω => S.YofA false ω * S.Avar.indicator false ω) μ :=
htrue_int.add hfalse_int
refine hsum_int.congr (Filter.Eventually.of_forall ?_)
intro ω
by_cases hω : S.A ω = true
· have hcf : S.YofA true ω = S.Y ω := by
simpa [YofA, Y, A] using
POVar.cf_eq_factual_on_event HA.consistency S.Yvar S.Avar true hAY.symm hω
have hind_true : S.Avar.indicator true ω = 1 :=
S.Avar.indicator_apply_eq_one hω
have hfalse : S.A ω ≠ false := by
rw [hω]
decide
have hind_false : S.Avar.indicator false ω = 0 :=
S.Avar.indicator_apply_eq_zero hfalse
simp [Pi.add_apply, hcf, hind_true, hind_false]
· have hω_false : S.A ω = false := by
cases hA : S.A ω <;> simp_all
have hcf : S.YofA false ω = S.Y ω := by
simpa [YofA, Y, A] using
POVar.cf_eq_factual_on_event HA.consistency S.Yvar S.Avar false hAY.symm hω_false
have hind_true : S.Avar.indicator true ω = 0 :=
S.Avar.indicator_apply_eq_zero hω
have hind_false : S.Avar.indicator false ω = 1 :=
S.Avar.indicator_apply_eq_one hω_false
simp [Pi.add_apply, hcf, hind_true, hind_false]
Helpers 1 core · 10 supporting This file supplies the conditional-expectation reductions used by the proximal ATE theorem: dropping proxy or treatment coordinates under conditional independence, transporting consistency through event restrictions, and ★ consistency_event
Conditional-expectation helpers for proximal ATE
This file supplies the conditional-expectation reductions used by the proximal ATE theorem: dropping proxy or treatment coordinates under conditional independence, transporting consistency through event restrictions, and exposing both field-level and bundled forms for reuse by exact and partial proximal identification modules.
lemma consistency_event reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Factual-outcome bridge on the treatment-arm event. From the consistency assumption in the proximal identifying assumption bundle, and given the treatment and outcome are distinct nodes, on the event where the treatment equals arm a, the conditional expectation of the factual outcome given σ(A,U,X) agrees almost surely with the conditional expectation of the potential outcome Y(a) given the same σ-algebra, since Y = Y(a) pointwise there.
Formal statement
hypotheses
conclusion
μ[S.Y | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[S.YofA a | S.σ_AUX]
Proof (Lean source)
lemma consistency_event (HA : Assumptions S μ) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) :
μ[S.Y | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[S.YofA a | S.σ_AUX] := by
have hYaInt : Integrable (S.YofA a) μ := by
cases a
· exact HA.integrable_YofA0
· exact HA.integrable_YofA1
exact consistency_event' HA.consistency a hAY (HA.integrable_Y hAY) hYaInt
10 supporting declarations (lemmas, instances)
-
condExp_drop_Z'lemma — Field-level form: from proxy_YZ : Y ⟂ Z | (A,U,X) and integrability of Y, E[Y | σ(A,Z,U,X)] =ᵐ[μ] E[Y | σ(A,U,X)].hypothesesproxy_YZ :CondIndepFun S.σ_AUX S.σ_AUX_le S.Y S.Z μhYInt :Integrable S.Y μconclusionμ[S.Y | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AUX]Proof (Lean source)
lemma condExp_drop_Z' (proxy_YZ : CondIndepFun S.σ_AUX S.σ_AUX_le S.Y S.Z μ) (hYInt : Integrable S.Y μ) : μ[S.Y | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AUX] := by -- Show σ_AZUX = σ_AUX ⊔ comap S.Z. have hσ_eq : S.σ_AZUX = S.σ_AUX ⊔ comap S.Z inferInstance := by change comap (fun ω => (S.A ω, S.Z ω, S.U ω, S.X ω)) _ = _ rw [show (inferInstance : MeasurableSpace (Bool × γ_Z × γ_U × γ_X)) = (inferInstance : MeasurableSpace Bool).prod inferInstance from rfl, MeasurableSpace.comap_prodMk, show (inferInstance : MeasurableSpace (γ_Z × γ_U × γ_X)) = (inferInstance : MeasurableSpace γ_Z).prod inferInstance from rfl, MeasurableSpace.comap_prodMk] have hAUX : S.σ_AUX = comap S.A inferInstance ⊔ comap (fun ω => (S.U ω, S.X ω)) inferInstance := by change comap (fun ω => (S.A ω, S.U ω, S.X ω)) _ = _ rw [show (inferInstance : MeasurableSpace (Bool × γ_U × γ_X)) = (inferInstance : MeasurableSpace Bool).prod inferInstance from rfl, MeasurableSpace.comap_prodMk] rw [hAUX] ac_rfl rw [hσ_eq] exact condExp_sup_comap_eq_of_condIndep (m := S.σ_AUX) S.σ_AUX_le S.measurable_Z S.measurable_Y proxy_YZ (h := id) measurable_id (by simpa using hYInt) -
condExp_drop_Zlemma — From proxy_YZ : Y ⟂ Z | (A,U,X), conclude E[Y | σ(A,Z,U,X)] =ᵐ[μ] E[Y | σ(A,U,X)].hypothesesHA :Assumptions S μhAY :S.Avar.v ≠ S.Yvar.vconclusionμ[S.Y | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AUX]Proof (Lean source)
lemma condExp_drop_Z (HA : Assumptions S μ) (hAY : S.Avar.v ≠ S.Yvar.v) : μ[S.Y | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AUX] := condExp_drop_Z' HA.proxy_YZ (HA.integrable_Y hAY) -
condExp_h_drop_Z'lemma — Field-level form: from proxy_WAZ : W ⟂ (A,Z) | (U,X), measurability and arm-integrability of the bridge h, conclude E[h(a,W,X) | σ(A,Z,U,X)] =ᵐ[μ] E[h(a,W,X) | σ(A,U,X)].hypothesesh_fun :Bool × γ_W × γ_X → ℝproxy_WAZ :CondIndepFun S.σ_UX S.σ_UX_le S.W (fun ω => (S.A ω, S.Z ω)) μmeasurable_h :Measurable h_funa :h_int :Integrable (fun ω => h_fun (a, S.W ω, S.X ω)) μconclusionμ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_AZUX]=ᵐ[μ] μ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_AUX]Proof (Lean source)
lemma condExp_h_drop_Z' {h_fun : Bool × γ_W × γ_X → ℝ} (proxy_WAZ : CondIndepFun S.σ_UX S.σ_UX_le S.W (fun ω => (S.A ω, S.Z ω)) μ) (measurable_h : Measurable h_fun) (a : Bool) (h_int : Integrable (fun ω => h_fun (a, S.W ω, S.X ω)) μ) : μ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_AZUX] =ᵐ[μ] μ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_AUX] := by -- σ-algebra: σ_AZUX = σ_AUX ⊔ comap Z. have hσ_eq : S.σ_AZUX = S.σ_AUX ⊔ comap S.Z inferInstance := by change comap (fun ω => (S.A ω, S.Z ω, S.U ω, S.X ω)) _ = _ rw [show (inferInstance : MeasurableSpace (Bool × γ_Z × γ_U × γ_X)) = (inferInstance : MeasurableSpace Bool).prod inferInstance from rfl, MeasurableSpace.comap_prodMk, show (inferInstance : MeasurableSpace (γ_Z × γ_U × γ_X)) = (inferInstance : MeasurableSpace γ_Z).prod inferInstance from rfl, MeasurableSpace.comap_prodMk] have hAUX : S.σ_AUX = comap S.A inferInstance ⊔ comap (fun ω => (S.U ω, S.X ω)) inferInstance := by change comap (fun ω => (S.A ω, S.U ω, S.X ω)) _ = _ rw [show (inferInstance : MeasurableSpace (Bool × γ_U × γ_X)) = (inferInstance : MeasurableSpace Bool).prod inferInstance from rfl, MeasurableSpace.comap_prodMk] rw [hAUX] ac_rfl -- Weak union: W ⟂ (A,Z) | σ_UX ⇒ W ⟂ Z | σ_UX ⊔ comap A = σ_AUX. have hWZA : CondIndepFun S.σ_UX S.σ_UX_le S.W (fun ω => (S.Z ω, S.A ω)) μ := by have h := proxy_WAZ.comp (φ := id) (ψ := fun (p : Bool × γ_Z) => (p.2, p.1)) measurable_id (by fun_prop) simpa [Function.comp_def] using h have hWZ_AUX : CondIndepFun (S.σ_UX ⊔ comap S.A inferInstance) (sup_le S.σ_UX_le S.measurable_A.comap_le) S.W S.Z μ := condIndepFun_weak_union_of_prodMk S.σ_UX_le S.measurable_W S.measurable_Z S.measurable_A hWZA -- σ_AUX = σ_UX ⊔ comap A. have hσ_AUX : S.σ_AUX = S.σ_UX ⊔ comap S.A inferInstance := by change comap (fun ω => (S.A ω, S.U ω, S.X ω)) _ = _ rw [show (inferInstance : MeasurableSpace (Bool × γ_U × γ_X)) = (inferInstance : MeasurableSpace Bool).prod inferInstance from rfl, MeasurableSpace.comap_prodMk] exact sup_comm _ _ -- Cast hWZ_AUX to use σ_AUX. have hWZ_AUX' : CondIndepFun S.σ_AUX S.σ_AUX_le S.W S.Z μ := by convert hWZ_AUX -- X is σ_AUX-measurable. have hX_m : Measurable[S.σ_AUX] S.X := by change Measurable[comap S.AUX inferInstance] S.X intro s hs refine ⟨(fun p : Bool × γ_U × γ_X => p.2.2) ⁻¹' s, ?_, rfl⟩ exact (measurable_snd.comp measurable_snd) hs -- Lift to (W, X) ⟂ Z | σ_AUX. have hWX_Z : CondIndepFun S.σ_AUX S.σ_AUX_le (fun ω => (S.W ω, S.X ω)) S.Z μ := Causalean.condIndepFun_prodMk_of_measurable_left S.σ_AUX_le S.measurable_W S.measurable_Z hX_m hWZ_AUX' let h_comb : γ_W × γ_X → ℝ := fun p => h_fun (a, p.1, p.2) have h_comb_meas : Measurable h_comb := by have : Measurable (fun p : γ_W × γ_X => (a, p.1, p.2)) := by fun_prop exact measurable_h.comp this rw [hσ_eq] exact condExp_sup_comap_eq_of_condIndep (m := S.σ_AUX) S.σ_AUX_le S.measurable_Z (prodMk S.measurable_W S.measurable_X) hWX_Z h_comb_meas h_int -
condExp_h_drop_Zlemma — From proxy_WAZ : W ⟂ (A,Z) | (U,X), for any a : Bool, E[h(a,W,X) | σ(A,Z,U,X)] =ᵐ[μ] E[h(a,W,X) | σ(A,U,X)].hypothesesHA :Assumptions S μa :conclusionμ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AZUX]=ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]Proof (Lean source)
lemma condExp_h_drop_Z (HA : Assumptions S μ) (a : Bool) : μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AZUX] =ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := by have h_int : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ := by cases a · exact HA.integrable_h0WX · exact HA.integrable_h1WX exact condExp_h_drop_Z' HA.proxy_WAZ HA.measurable_h a h_int -
condExp_h_drop_A'lemma — Field-level form: from proxy_WA : W ⟂ A | (U,X), measurability and arm-integrability of the bridge h, conclude E[h(a,W,X) | σ(A,U,X)] =ᵐ[μ] E[h(a,W,X) | σ(U,X)].hypothesesh_fun :Bool × γ_W × γ_X → ℝproxy_WA :CondIndepFun S.σ_UX S.σ_UX_le S.W S.A μmeasurable_h :Measurable h_funa :h_int :Integrable (fun ω => h_fun (a, S.W ω, S.X ω)) μconclusionμ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_AUX]=ᵐ[μ] μ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_UX]Proof (Lean source)
lemma condExp_h_drop_A' {h_fun : Bool × γ_W × γ_X → ℝ} (proxy_WA : CondIndepFun S.σ_UX S.σ_UX_le S.W S.A μ) (measurable_h : Measurable h_fun) (a : Bool) (h_int : Integrable (fun ω => h_fun (a, S.W ω, S.X ω)) μ) : μ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_AUX] =ᵐ[μ] μ[fun ω => h_fun (a, S.W ω, S.X ω) | S.σ_UX] := by -- σ-algebra: σ_AUX = σ_UX ⊔ comap A. have hσ_eq : S.σ_AUX = S.σ_UX ⊔ comap S.A inferInstance := by change comap (fun ω => (S.A ω, S.U ω, S.X ω)) _ = _ rw [show (inferInstance : MeasurableSpace (Bool × γ_U × γ_X)) = (inferInstance : MeasurableSpace Bool).prod inferInstance from rfl, MeasurableSpace.comap_prodMk] exact sup_comm _ _ -- X is σ_UX-measurable. have hX_m : Measurable[S.σ_UX] S.X := by change Measurable[comap S.UX inferInstance] S.X intro s hs exact ⟨Prod.snd ⁻¹' s, measurable_snd hs, rfl⟩ -- Lift to (W, X) ⟂ A | σ_UX. have hWX_A : CondIndepFun S.σ_UX S.σ_UX_le (fun ω => (S.W ω, S.X ω)) S.A μ := Causalean.condIndepFun_prodMk_of_measurable_left S.σ_UX_le S.measurable_W S.measurable_A hX_m proxy_WA let h_comb : γ_W × γ_X → ℝ := fun p => h_fun (a, p.1, p.2) have h_comb_meas : Measurable h_comb := by have : Measurable (fun p : γ_W × γ_X => (a, p.1, p.2)) := by fun_prop exact measurable_h.comp this rw [hσ_eq] exact condExp_sup_comap_eq_of_condIndep (m := S.σ_UX) S.σ_UX_le S.measurable_A (prodMk S.measurable_W S.measurable_X) hWX_A h_comb_meas h_int -
condExp_h_drop_Alemma — From proxy_WAZ : W ⟂ (A,Z) | (U,X), projecting to W ⟂ A | (U,X), E[h(a,W,X) | σ(A,U,X)] =ᵐ[μ] E[h(a,W,X) | σ(U,X)].hypothesesHA :Assumptions S μa :conclusionμ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]=ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX]Proof (Lean source)
lemma condExp_h_drop_A (HA : Assumptions S μ) (a : Bool) : μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] =ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX] := by -- Project proxy_WAZ to W ⟂ A | σ_UX via .comp with Prod.fst. have hWA : CondIndepFun S.σ_UX S.σ_UX_le S.W S.A μ := by have h := HA.proxy_WAZ.comp (φ := id) (ψ := fst) measurable_id measurable_fst simpa [Function.comp_def] using h have h_int : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ := by cases a · exact HA.integrable_h0WX · exact HA.integrable_h1WX exact condExp_h_drop_A' hWA HA.measurable_h a h_int -
latent_exch_to_condExp'lemma — Field-level form: from latent_exch a : Y(a) ⟂ A | (U,X) and integrability of Y(a), conclude E[Y(a) | σ(A,U,X)] =ᵐ[μ] E[Y(a) | σ(U,X)].hypothesesconclusionμ[S.YofA a | S.σ_AUX] =ᵐ[μ] μ[S.YofA a | S.σ_UX]Proof (Lean source)
lemma latent_exch_to_condExp' (a : Bool) (latent_exch : CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μ) (hYaInt : Integrable (S.YofA a) μ) : μ[S.YofA a | S.σ_AUX] =ᵐ[μ] μ[S.YofA a | S.σ_UX] := by -- Show σ_AUX = σ_UX ⊔ comap S.A. have hσ_eq : S.σ_AUX = S.σ_UX ⊔ comap S.A inferInstance := by change comap (fun ω => (S.A ω, S.U ω, S.X ω)) _ = _ rw [show (inferInstance : MeasurableSpace (Bool × γ_U × γ_X)) = (inferInstance : MeasurableSpace Bool).prod inferInstance from rfl, MeasurableSpace.comap_prodMk] exact sup_comm _ _ rw [hσ_eq] exact condExp_sup_comap_eq_of_condIndep (m := S.σ_UX) S.σ_UX_le S.measurable_A (S.measurable_YofA a) latent_exch (h := id) measurable_id (by simpa using hYaInt) -
latent_exch_to_condExplemma — From latent_exch a : Y(a) ⟂ A | (U,X): E[Y(a) | σ(A,U,X)] =ᵐ[μ] E[Y(a) | σ(U,X)].hypothesesHA :Assumptions S μa :conclusionμ[S.YofA a | S.σ_AUX] =ᵐ[μ] μ[S.YofA a | S.σ_UX]Proof (Lean source)
lemma latent_exch_to_condExp (HA : Assumptions S μ) (a : Bool) : μ[S.YofA a | S.σ_AUX] =ᵐ[μ] μ[S.YofA a | S.σ_UX] := by have hYaInt : Integrable (S.YofA a) μ := by cases a · exact HA.integrable_YofA0 · exact HA.integrable_YofA1 exact latent_exch_to_condExp' a (HA.latent_exch a) hYaInt -
consistency_event'lemma — Field-level form: from consistency, integrability of Y and Y(a), on {A=a} we have E[Y | σ(A,U,X)] =ᵐ[μ.restrict {A=a}] E[Y(a) | σ(A,U,X)].hypothesesHC :POSystem.Consistency Pa :hAY :S.Avar.v ≠ S.Yvar.vhYInt :Integrable S.Y μhYaInt :Integrable (S.YofA a) μconclusionμ[S.Y | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[S.YofA a | S.σ_AUX]Proof (Lean source)
lemma consistency_event' (HC : POSystem.Consistency P) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) (hYInt : Integrable S.Y μ) (hYaInt : Integrable (S.YofA a) μ) : μ[S.Y | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[S.YofA a | S.σ_AUX] := by -- Step 1: Y =ᵐ[μ.restrict {A=a}] Y(a) pointwise from consistency. have hYeq : S.Y =ᵐ[μ.restrict {ω | S.A ω = a}] S.YofA a := by have hs : MeasurableSet {ω : P.Ω | S.A ω = a} := S.measurable_A (measurableSet_singleton a) apply ae_restrict_of_forall_mem hs intro ω hω exact (POVar.cf_eq_factual_on_event HC S.Yvar S.Avar a hAY.symm hω).symm set s : Set P.Ω := {ω | S.A ω = a} have hs_in_m : MeasurableSet[S.σ_AUX] s := by refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩ · exact measurable_fst (measurableSet_singleton a) · ext ω; rfl have hs : MeasurableSet s := S.measurable_A (measurableSet_singleton a) let h : P.Ω → ℝ := fun ω => S.Y ω - S.YofA a ω have hint : Integrable h μ := hYInt.sub hYaInt -- s.indicator h = 0 μ-a.e. have hind_zero : s.indicator h =ᵐ[μ] 0 := by have h_zero_on_s : h =ᵐ[μ.restrict s] 0 := by filter_upwards [hYeq] with ω hω simp [h, hω] simpa using Causalean.indicator_aeEq_of_aeEq_restrict hs h_zero_on_s have hh_zero_on_s : μ[h | S.σ_AUX] =ᵐ[μ.restrict s] 0 := by have hindCE_zero : s.indicator (μ[h | S.σ_AUX]) =ᵐ[μ] 0 := Causalean.condExp_indicator_aeEq_zero hs_in_m hint hind_zero have hindCE_zero' : s.indicator (μ[h | S.σ_AUX]) =ᵐ[μ] s.indicator (0 : P.Ω → ℝ) := by simpa using hindCE_zero simpa using Causalean.aeEq_restrict_of_indicator_aeEq hs hindCE_zero' have hCE_sub : μ[h | S.σ_AUX] =ᵐ[μ] μ[S.Y | S.σ_AUX] - μ[S.YofA a | S.σ_AUX] := MeasureTheory.condExp_sub (m := S.σ_AUX) hYInt hYaInt have hCE_sub_restrict : μ[h | S.σ_AUX] =ᵐ[μ.restrict s] μ[S.Y | S.σ_AUX] - μ[S.YofA a | S.σ_AUX] := ae_restrict_of_ae hCE_sub have hdiff_zero : (μ[S.Y | S.σ_AUX] - μ[S.YofA a | S.σ_AUX]) =ᵐ[μ.restrict s] 0 := hCE_sub_restrict.symm.trans hh_zero_on_s filter_upwards [hdiff_zero] with ω hω have : (μ[S.Y | S.σ_AUX]) ω - (μ[S.YofA a | S.σ_AUX]) ω = 0 := by simpa [Pi.sub_apply, Pi.zero_apply] using hω linarith -
eq_zero_globally_of_eq_zero_on_armlemma — From positivity_arm a and a σ_UX-measurable function that is μ-a.e. zero on the arm {A=a}, conclude it is μ-a.e. zero globally.hypothesesHA :Assumptions S μa :f :P.Ω → ℝhf_meas :Measurable[S.σ_UX] fhf_zero_on_arm :f =ᵐ[μ.restrict {ω | S.A ω = a}] 0conclusionf =ᵐ[μ] 0Proof (Lean source)
lemma eq_zero_globally_of_eq_zero_on_arm (HA : Assumptions S μ) (a : Bool) {f : P.Ω → ℝ} (hf_meas : Measurable[S.σ_UX] f) (hf_zero_on_arm : f =ᵐ[μ.restrict {ω | S.A ω = a}] 0) : f =ᵐ[μ] 0 := by set s : Set P.Ω := {ω | S.A ω = a} with hs_def have hs : MeasurableSet s := S.measurable_A (measurableSet_singleton a) -- Carrier B := {ω | f ω ≠ 0}, σ_UX-measurable. set B : Set P.Ω := {ω | f ω ≠ 0} with hB_def have hB_eq : B = f ⁻¹' {0}ᶜ := by ext ω; simp [B, hB_def] have hB_meas : MeasurableSet[S.σ_UX] B := by rw [hB_eq] exact hf_meas (MeasurableSet.compl (measurableSet_singleton (0 : ℝ))) -- arm hypothesis: μ(B ∩ s) = 0. have hB_meas' : MeasurableSet B := S.σ_UX_le _ hB_meas have hBs_zero : μ (B ∩ s) = 0 := by have h1 : (μ.restrict s) B = 0 := by have h := hf_zero_on_arm rw [EventuallyEq, MeasureTheory.ae_iff] at h rw [hB_def] simpa using h rwa [MeasureTheory.Measure.restrict_apply hB_meas'] at h1 -- positivity_arm gives μ B = 0, i.e. f =ᵐ[μ] 0. have hB_zero : μ B = 0 := HA.positivity_arm a B hB_meas hBs_zero rw [EventuallyEq, MeasureTheory.ae_iff] simpa [hB_def] using hB_zero
Main 2 core · 0 supporting This file proves the proximal causal identification equalities from the POProximalSystem.Assumptions bundle. ★ Eofyofa_eq_Eh★ ate_proximal
Proximal ATE Identification
This file proves the proximal causal identification equalities from the
POProximalSystem.Assumptions bundle. The theorem
Assumptions.Eofyofa_eq_Eh shows that each treatment-specific counterfactual
mean equals the corresponding bridge-function mean,
integral Y(a) = integral h(a,W,X). The theorem Assumptions.ate_proximal
then identifies the average treatment effect as
integral h(true,W,X) - integral h(false,W,X).
The proof uses the helper reductions from Proximal.Helpers, a Doob-Dynkin
factorization through (U,X), treatment-arm completeness, and arm positivity
to globalize the arm-wise bridge equality.
theorem Eofyofa_eq_Eh reviewed
⚑ flagged
Causalean.PO.POProximalSystem.Assumptions
Proximal ATE identification (prop:po-proximal-ate step 1). Under the proximal identifying assumption bundle, including completeness within treatment level and integrability of the potential outcomes and bridge-function values, provided the treatment and outcome are distinct nodes, for each treatment level a the counterfactual mean outcome equals the mean of the proximal bridge function evaluated at that level: E[Y(a)] = E[h(a,W,X)].
Formal statement
hypotheses
conclusion
∫ ω, S.YofA a ω ∂μ = ∫ ω, HA.h (a, S.W ω, S.X ω) ∂μ
Proof (Lean source)
theorem Eofyofa_eq_Eh (HA : Assumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v) :
∫ ω, S.YofA a ω ∂μ = ∫ ω, HA.h (a, S.W ω, S.X ω) ∂μ := by
-- Set s = {A = a}; needed throughout.
set s : Set P.Ω := {ω | S.A ω = a} with hs_def
have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a)
-- Integrability shortcuts.
have hYInt : Integrable S.Y μ := HA.integrable_Y hAY
have hYaInt : Integrable (S.YofA a) μ := by
cases a
· exact HA.integrable_YofA0
· exact HA.integrable_YofA1
have hhInt : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ := by
cases a
· exact HA.integrable_h0WX
· exact HA.integrable_h1WX
have hhAInt : Integrable (fun ω => HA.h (S.A ω, S.W ω, S.X ω)) μ := HA.integrable_hAWX
have h_meas_haWX : Measurable (fun ω => HA.h (a, S.W ω, S.X ω)) := by
have hp : Measurable (fun ω : P.Ω => (a, S.W ω, S.X ω)) := by
exact prodMk measurable_const
(prodMk S.measurable_W S.measurable_X)
exact HA.measurable_h.comp hp
-- ============================================================
-- Step 1: Construct g_a : γ_U × γ_X → ℝ via Doob–Dynkin.
-- ============================================================
-- μ[Y | σ_AUX] is σ_AUX = comap S.AUX-measurable, so factors through S.AUX.
have hCEY_meas : Measurable[S.σ_AUX] (μ[S.Y | S.σ_AUX]) :=
MeasureTheory.stronglyMeasurable_condExp.measurable
have hCEY_meas' : Measurable[comap S.AUX inferInstance]
(μ[S.Y | S.σ_AUX]) := hCEY_meas
obtain ⟨f_Y, hf_Y_meas, hf_Y_eq⟩ :=
Measurable.exists_eq_measurable_comp (f := S.AUX) (Z := ℝ) hCEY_meas'
-- μ[h(a,W,X) | σ_AUX] is also σ_AUX-measurable.
have hCEh_meas : Measurable[S.σ_AUX]
(μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) :=
MeasureTheory.stronglyMeasurable_condExp.measurable
have hCEh_meas' : Measurable[comap S.AUX inferInstance]
(μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) := hCEh_meas
obtain ⟨f_h, hf_h_meas, hf_h_eq⟩ :=
Measurable.exists_eq_measurable_comp (f := S.AUX) (Z := ℝ) hCEh_meas'
-- Define g_a (u, x) := f_Y (a, u, x) - f_h (a, u, x).
let g_a : γ_U × γ_X → ℝ := fun p => f_Y (a, p.1, p.2) - f_h (a, p.1, p.2)
have g_a_meas : Measurable g_a := by
have h1 : Measurable (fun p : γ_U × γ_X => f_Y (a, p.1, p.2)) := by
have : Measurable (fun p : γ_U × γ_X => (a, p.1, p.2)) := by fun_prop
exact hf_Y_meas.comp this
have h2 : Measurable (fun p : γ_U × γ_X => f_h (a, p.1, p.2)) := by
have : Measurable (fun p : γ_U × γ_X => (a, p.1, p.2)) := by fun_prop
exact hf_h_meas.comp this
exact h1.sub h2
-- g_a ∘ S.UX is integrable on the restriction to s = {A = a}.
-- On s, S.AUX ω = (a, S.U ω, S.X ω), so g_a ∘ UX = (μ[Y|σ_AUX]) - (μ[h|σ_AUX])
-- pointwise. Both condExps are integrable globally, hence on restrict, and
-- their difference is integrable; congr lifts to g_a ∘ UX.
have g_a_UX_int : Integrable (fun ω => g_a (S.UX ω)) (μ.restrict s) := by
have hCEY_int : Integrable (μ[S.Y | S.σ_AUX]) μ := MeasureTheory.integrable_condExp
have hCEh_int : Integrable (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) μ :=
MeasureTheory.integrable_condExp
have hCEY_int_r : Integrable (μ[S.Y | S.σ_AUX]) (μ.restrict s) := hCEY_int.restrict
have hCEh_int_r : Integrable (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX])
(μ.restrict s) := hCEh_int.restrict
have hdiff_int : Integrable
(fun ω => (μ[S.Y | S.σ_AUX]) ω -
(μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω) (μ.restrict s) :=
hCEY_int_r.sub hCEh_int_r
-- Show on s: g_a (S.UX ω) = (μ[Y|σ_AUX]) ω - (μ[h|σ_AUX]) ω.
have hae : (fun ω => (μ[S.Y | S.σ_AUX]) ω -
(μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω)
=ᵐ[μ.restrict s] (fun ω => g_a (S.UX ω)) := by
filter_upwards [ae_restrict_mem hs_meas] with ω hω_s
have hAa : S.A ω = a := hω_s
have hAUX_eq : S.AUX ω = (a, S.U ω, S.X ω) := by
change (S.A ω, S.U ω, S.X ω) = (a, S.U ω, S.X ω); rw [hAa]
have hY : (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω) := by
have h1 := congrFun hf_Y_eq ω
change (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω)
rw [h1]; change f_Y (S.AUX ω) = f_Y (a, S.U ω, S.X ω); rw [hAUX_eq]
have hh : (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω
= f_h (a, S.U ω, S.X ω) := by
have h1 := congrFun hf_h_eq ω
change (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = f_h (a, S.U ω, S.X ω)
rw [h1]; change f_h (S.AUX ω) = f_h (a, S.U ω, S.X ω); rw [hAUX_eq]
have hUX : S.UX ω = (S.U ω, S.X ω) := rfl
simp [hY, hh, g_a, hUX]
exact hdiff_int.congr hae
-- ============================================================
-- Step 2: μ[Y - h(a,W,X) | σ_AZUX] =ᵐ[μ.restrict s] g_a ∘ S.UX.
-- ============================================================
-- By linearity + helpers 1, 2:
-- μ[Y - h(a,W,X) | σ_AZUX]
-- =ᵐ μ[Y | σ_AZUX] - μ[h(a,W,X) | σ_AZUX] (linearity)
-- =ᵐ μ[Y | σ_AUX] - μ[h(a,W,X) | σ_AUX] (helpers 1, 2)
-- = (f_Y ∘ S.AUX) - (f_h ∘ S.AUX) (Doob–Dynkin)
-- On s = {A=a}, S.AUX ω = (a, S.U ω, S.X ω), so this evaluates to
-- f_Y(a, S.U ω, S.X ω) - f_h(a, S.U ω, S.X ω) = g_a (S.UX ω).
have step2 : (μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX])
=ᵐ[μ.restrict s] (fun ω => g_a (S.UX ω)) := by
-- Linearity: μ[Y - h(a,W,X)|σ_AZUX] =ᵐ μ[Y|σ_AZUX] - μ[h(a,W,X)|σ_AZUX].
have hlin : μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX]
=ᵐ[μ] μ[S.Y | S.σ_AZUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AZUX] :=
MeasureTheory.condExp_sub (m := S.σ_AZUX) hYInt hhInt
-- Helpers 1, 2: drop Z.
have h1 : μ[S.Y | S.σ_AZUX] =ᵐ[μ] μ[S.Y | S.σ_AUX] := condExp_drop_Z HA hAY
have h2 : μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AZUX]
=ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := condExp_h_drop_Z HA a
-- Combine globally:
-- μ[Y-h|σ_AZUX] =ᵐ μ[Y|σ_AUX] - μ[h|σ_AUX].
have hglobal : μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX]
=ᵐ[μ] μ[S.Y | S.σ_AUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := by
refine hlin.trans ?_
filter_upwards [h1, h2] with ω hω1 hω2
simp [Pi.sub_apply, hω1, hω2]
-- Now restrict to s.
have hrestrict : μ[fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω) | S.σ_AZUX]
=ᵐ[μ.restrict s]
μ[S.Y | S.σ_AUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
ae_restrict_of_ae hglobal
-- On s, the RHS = g_a ∘ S.UX (Doob–Dynkin substitution, same as step 5).
refine hrestrict.trans ?_
filter_upwards [ae_restrict_mem hs_meas] with ω hω_s
have hAa : S.A ω = a := hω_s
have hAUX_eq : S.AUX ω = (a, S.U ω, S.X ω) := by
change (S.A ω, S.U ω, S.X ω) = (a, S.U ω, S.X ω); rw [hAa]
have hY : (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω) := by
have h1 := congrFun hf_Y_eq ω
change (μ[S.Y | S.σ_AUX]) ω = f_Y (a, S.U ω, S.X ω)
rw [h1]; change f_Y (S.AUX ω) = f_Y (a, S.U ω, S.X ω); rw [hAUX_eq]
have hh : (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω
= f_h (a, S.U ω, S.X ω) := by
have h1 := congrFun hf_h_eq ω
change (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = f_h (a, S.U ω, S.X ω)
rw [h1]; change f_h (S.AUX ω) = f_h (a, S.U ω, S.X ω); rw [hAUX_eq]
show (μ[S.Y | S.σ_AUX] - μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω
= g_a (S.UX ω)
have hUX : S.UX ω = (S.U ω, S.X ω) := rfl
simp [Pi.sub_apply, hY, hh, g_a, hUX]
-- ============================================================
-- Step 3: μ[g_a ∘ S.UX | σ_AZX] =ᵐ[μ.restrict s] 0.
-- ============================================================
-- σ_AZX ≤ σ_AZUX (σ_AZUX includes U), so by tower:
-- μ[Y - h(A,W,X) | σ_AZX] =ᵐ μ[μ[Y - h(A,W,X) | σ_AZUX] | σ_AZX].
-- Bridge gives LHS =ᵐ 0; on s, h(A,W,X) =ᵐ h(a,W,X) (since A=a on s), and
-- s ∈ σ_AZX, so we can swap to get
-- μ[μ[Y - h(a,W,X) | σ_AZUX] | σ_AZX] =ᵐ[restrict s] 0.
-- Combining with step2: μ[g_a ∘ S.UX | σ_AZX] =ᵐ[restrict s] 0.
have step3 : (μ[fun ω => g_a (S.UX ω) | S.σ_AZX]) =ᵐ[μ.restrict s] 0 := by
-- Strategy:
-- 1. Tower: σ_AZX ≤ σ_AZUX. Get
-- μ[g_a∘UX | σ_AZX] =ᵐ μ[μ[g_a∘UX | σ_AZUX] | σ_AZX].
-- 2. Step 2 says μ[Y - h(a,W,X) | σ_AZUX] =ᵐ[restrict s] g_a∘UX.
-- Lift LHS to global: bridge gives μ[Y - h(A,W,X) | σ_AZX] =ᵐ 0,
-- so condExp through indicator on {A=a} (where h(A,W,X)=h(a,W,X))
-- gives the goal.
-- σ_AZX ≤ σ_AZUX (since AZUX projects onto AZX measurably).
have hAZX_le_AZUX : S.σ_AZX ≤ S.σ_AZUX := by
-- Show S.AZX is σ_AZUX-measurable.
have hAZX_meas : Measurable[S.σ_AZUX] S.AZX := by
show Measurable[comap S.AZUX inferInstance] S.AZX
intro u hu
refine ⟨(fun p : Bool × γ_Z × γ_U × γ_X => (p.1, p.2.1, p.2.2.2)) ⁻¹' u, ?_, ?_⟩
· exact (measurable_fst.prodMk
(measurable_fst.comp measurable_snd |>.prodMk
(measurable_snd.comp (measurable_snd.comp measurable_snd)))) hu
· ext ω; rfl
exact hAZX_meas.comap_le
-- s = {A=a} ∈ σ_AZX (use comap of (A,Z,X) on the first coordinate).
have hs_in_AZX : MeasurableSet[S.σ_AZX] s := by
refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩
· exact measurable_fst (measurableSet_singleton a)
· ext ω; rfl
-- Difference function and integrability.
let h : P.Ω → ℝ := fun ω => S.Y ω - HA.h (S.A ω, S.W ω, S.X ω)
let h' : P.Ω → ℝ := fun ω => S.Y ω - HA.h (a, S.W ω, S.X ω)
have hint : Integrable h μ := hYInt.sub hhAInt
have hint' : Integrable h' μ := hYInt.sub hhInt
-- On s, h = h' pointwise.
have hh_eq_on_s : ∀ᵐ ω ∂(μ.restrict s), h ω = h' ω := by
filter_upwards [ae_restrict_mem hs_meas] with ω hω_s
have hAa : S.A ω = a := hω_s
show S.Y ω - HA.h (S.A ω, S.W ω, S.X ω) = S.Y ω - HA.h (a, S.W ω, S.X ω)
rw [hAa]
-- Tower step 2 to σ_AZX:
-- μ[h' | σ_AZX] =ᵐ μ[μ[h' | σ_AZUX] | σ_AZX].
have h_tower : μ[h' | S.σ_AZX] =ᵐ[μ] μ[μ[h' | S.σ_AZUX] | S.σ_AZX] :=
(MeasureTheory.condExp_condExp_of_le hAZX_le_AZUX S.σ_AZUX_le).symm
-- step2 (restricted) lifts: μ[μ[h' | σ_AZUX] | σ_AZX] =ᵐ[restrict s] μ[g_a∘UX | σ_AZX].
-- Use indicator technique: 1_s · μ[h' | σ_AZUX] =ᵐ 1_s · g_a∘UX (both globally).
-- Then condExp_indicator with s ∈ σ_AZX.
-- Actually simpler: condExp_congr on restrict requires inner =ᵐ on restrict,
-- which doesn't directly give condExp =ᵐ on restrict.
-- We use: indicator s · μ[h'|σ_AZUX] =ᵐ[μ] indicator s · g_a∘UX.
have hCEh'_AZUX_int : Integrable (μ[h' | S.σ_AZUX]) μ := MeasureTheory.integrable_condExp
-- Case split: if g_a ∘ UX is not globally integrable, μ[g_a∘UX|σ_AZX] = 0
-- everywhere, so the goal is trivial. Otherwise, use original argument.
by_cases hg_a_int : Integrable (fun ω => g_a (S.UX ω)) μ
case neg =>
-- μ[g_a∘UX|σ_AZX] = 0 globally, so a.e. zero on restrict s.
have h0 : (μ[fun ω => g_a (S.UX ω) | S.σ_AZX]) = 0 :=
MeasureTheory.condExp_of_not_integrable hg_a_int
rw [h0]
-- pos branch: hg_a_int : Integrable (fun ω => g_a (S.UX ω)) μ holds.
-- 1_s · μ[h'|σ_AZUX] =ᵐ[μ] 1_s · g_a∘UX (from step2 restricted to s).
have hind_eq : s.indicator (μ[h' | S.σ_AZUX]) =ᵐ[μ] s.indicator (fun ω => g_a (S.UX ω)) := by
exact indicator_aeEq_of_aeEq_restrict hs_meas step2
-- Apply condExp to both sides and use condExp_indicator.
have hCE_ind_h' := MeasureTheory.condExp_indicator (m := S.σ_AZX) hCEh'_AZUX_int hs_in_AZX
have hCE_ind_g := MeasureTheory.condExp_indicator (m := S.σ_AZX) hg_a_int hs_in_AZX
-- μ[1_s · μ[h'|σ_AZUX] | σ_AZX] =ᵐ μ[1_s · g_a∘UX | σ_AZX] (by hind_eq + condExp_congr).
have hCE_eq : μ[s.indicator (μ[h' | S.σ_AZUX]) | S.σ_AZX]
=ᵐ[μ] μ[s.indicator (fun ω => g_a (S.UX ω)) | S.σ_AZX] :=
MeasureTheory.condExp_congr_ae hind_eq
-- Combine: 1_s · μ[μ[h'|σ_AZUX] | σ_AZX] =ᵐ 1_s · μ[g_a∘UX | σ_AZX].
have hind_CE : s.indicator (μ[μ[h' | S.σ_AZUX] | S.σ_AZX])
=ᵐ[μ] s.indicator (μ[fun ω => g_a (S.UX ω) | S.σ_AZX]) :=
hCE_ind_h'.symm.trans (hCE_eq.trans hCE_ind_g)
-- Now we need: 1_s · μ[μ[h'|σ_AZUX] | σ_AZX] =ᵐ 0, since by tower
-- μ[μ[h'|σ_AZUX] | σ_AZX] =ᵐ μ[h' | σ_AZX]
-- and on s (since {A=a} ∈ σ_AZX), μ[h'|σ_AZX] =ᵐ μ[h|σ_AZX] =ᵐ 0 (bridge).
-- We prove 1_s · μ[h'|σ_AZX] =ᵐ 0 using bridge.
-- Step (a): μ[h'|σ_AZX] =ᵐ[restrict s] 0.
-- Use indicator technique: 1_s · h =ᵐ 1_s · h' globally (both pointwise on s).
have hind_h_h' : s.indicator h =ᵐ[μ] s.indicator h' := by
exact indicator_aeEq_of_aeEq_restrict hs_meas hh_eq_on_s
-- Apply condExp_indicator to both:
have hCE_ind_h := MeasureTheory.condExp_indicator (m := S.σ_AZX) hint hs_in_AZX
have hCE_ind_h'_AZX := MeasureTheory.condExp_indicator (m := S.σ_AZX) hint' hs_in_AZX
-- μ[1_s · h | σ_AZX] =ᵐ μ[1_s · h' | σ_AZX] (by hind_h_h').
have hCE_eq2 : μ[s.indicator h | S.σ_AZX] =ᵐ[μ] μ[s.indicator h' | S.σ_AZX] :=
MeasureTheory.condExp_congr_ae hind_h_h'
have hind_CE_h : s.indicator (μ[h | S.σ_AZX]) =ᵐ[μ] s.indicator (μ[h' | S.σ_AZX]) :=
hCE_ind_h.symm.trans (hCE_eq2.trans hCE_ind_h'_AZX)
-- Bridge: μ[h | σ_AZX] =ᵐ 0, so 1_s · μ[h|σ_AZX] =ᵐ 0.
have hbridge : (μ[h | S.σ_AZX]) =ᵐ[μ] 0 := HA.bridge
have hind_h_zero : s.indicator (μ[h | S.σ_AZX]) =ᵐ[μ] 0 := by
-- … truncated; follow the source link for the rest …
theorem ate_proximal reviewed
⚑ flagged
Causalean.PO.POProximalSystem.Assumptions
Proximal ATE identification. Under the proximal identifying assumption bundle and given the treatment and outcome are distinct nodes, the average treatment effect E[Y(1)] − E[Y(0)] equals the bridge-function contrast E[h(1,W,X)] − E[h(0,W,X)].
Formal statement
Proof (Lean source)
theorem ate_proximal (HA : Assumptions S μ) (hAY : S.Avar.v ≠ S.Yvar.v) :
∫ ω, S.YofA true ω ∂μ - ∫ ω, S.YofA false ω ∂μ
= ∫ ω, HA.h (true, S.W ω, S.X ω) ∂μ
- ∫ ω, HA.h (false, S.W ω, S.X ω) ∂μ := by
rw [Eofyofa_eq_Eh HA true hAY, Eofyofa_eq_Eh HA false hAY]