PO.Bridge
Bridges into the potential-outcome framework: the PO system induced by a structural causal model and by finite-coordinate restriction.
FromSCM 8 core · 16 supporting This file constructs the potential-outcome system induced by a generalized structural causal model and a background assignment of fixed variables. ★ ofSCM_consistency
Potential Outcome Systems from Structural Models
This file constructs the potential-outcome system induced by a generalized structural causal model and a background assignment of fixed variables. The construction keeps one potential-outcome variable for every observed random node, translates structurally eligible regime targets into interventions, evaluates the intervened model at latent draws, and projects back to the observed variables.
The construction is organized around ObsIdx, regimeTargetN,
combinedFixed, inducedEval, and POSystem.ofSCM. The theorem
POSystem.ofSCM_consistency proves that the induced potential-outcome system
satisfies factual and composition consistency by reducing those clauses to the
SCM counterfactual consistency lemmas.
abbrev ObsIdx reviewed
⚑ flagged
Causalean.PO
The observed-node index set of the induced potential-outcome system consists of all random observed nodes of the structural model.
def obsIdx_mk_random reviewed
⚑ flagged
Causalean.PO
Every observed random node is an index of the potential-outcome system induced by an SCM.
Definition (Lean source)
def obsIdx_mk_random (M : SCM N Ω) (n : N)
(h : SWIGNode.random n ∈ M.observed) : ObsIdx M :=
⟨SWIGNode.random n, h⟩
abbrev obsValue reviewed
⚑ flagged
Causalean.PO
The value space of an observed-node index in the induced potential-outcome system is the structural-model value space attached to that observed node.
def regimeTargetN reviewed
⚑ flagged
Causalean.PO
The structural variable names targeted by a potential-outcome regime are the underlying names of the regime targets whose fixed counterparts are not already fixed in the structural model.
Definition (Lean source)
noncomputable def regimeTargetN
(M : SCM N Ω) (r : Regime (ObsIdx M) (obsValue M)) : Finset N :=
(r.target.filter (fun v => SWIGNode.fixed
(choose (M.observed_is_random v.val v.property)) ∉ M.fixed)).image (fun v =>
-- v : ObsIdx M, i.e. v.val : SWIGNode N with v.property : v.val ∈ M.observed.
-- Extract the `N`-name via classical choice on `observed_is_random`.
choose (M.observed_is_random v.val v.property))
def combinedFixed reviewed
⚑ flagged
Causalean.PO
The combined fixed-variable assignment feeds the original background values and the regime's intervention values into the intervened structural model.
Definition (Lean source)
noncomputable def combinedFixed
(M : SCM N Ω) (s : SCM.FixedValues M)
(r : Regime (ObsIdx M) (obsValue M)) :
SCM.FixedValues
(M.fixSet (regimeTargetN M r) (regimeTargetN_obs M r) (regimeTargetN_notFixed M r)) :=
fun v =>
if hMfix : v.val ∈ M.fixed then
s ⟨v.val, hMfix⟩
else
let v' := choose (combinedFixed_exists M r v hMfix)
let hv'spec := Classical.choose_spec (combinedFixed_exists M r v hMfix)
-- Cast `r.assign v' hv'spec.1 : obsValue M v' = swigΩ Ω v'.val` into `swigΩ Ω v.val`.
-- Both reduce to `Ω (obsName' M v')` via `obsName'_spec` and `hv'spec.2`.
cast (show obsValue M v' = swigΩ Ω v.val by
change swigΩ Ω v'.val = swigΩ Ω v.val
rw [obsName_spec M v', ← hv'spec.2])
(r.assign v' hv'spec.1)
def inducedEval reviewed
⚑ flagged
Causalean.PO
The induced joint evaluation map assigns values to all observed-node indices by evaluating the intervened structural model at a background assignment, a potential-outcome regime, and a latent draw.
Definition (Lean source)
noncomputable def inducedEval
(M : SCM N Ω) (s : SCM.FixedValues M)
(r : Regime (ObsIdx M) (obsValue M))
(ℓ : SCM.LatentValues M) : ∀ v : ObsIdx M, obsValue M v :=
let M' := M.fixSet (regimeTargetN M r) (regimeTargetN_obs M r) (regimeTargetN_notFixed M r)
fun v =>
-- v.val ∈ M.observed = M'.observed, so v.val ∈ M'.randomVars
let hmem : v.val ∈ M'.randomVars := by
change v.val ∈ M.observed ∪ M.unobserved
exact mem_union_left _ v.property
M'.evalMap (combinedFixed M s r) ℓ ⟨v.val, hmem⟩
def ofSCM reviewed
⚑ flagged
Causalean.PO.POSystem
A structural model and a background assignment induce a potential-outcome system whose variables are all observed random nodes of the model.
Definition (Lean source)
noncomputable def POSystem.ofSCM
(M : SCM N Ω) (s : SCM.FixedValues M) :
POSystem where
V := ObsIdx M
X := obsValue M
Ω := SCM.LatentValues M
μ := M.latentProduct
eval := fun r ℓ => inducedEval M s r ℓ
measurable_eval := fun r => inducedEval_measurable M s r
theorem ofSCM_consistency reviewed
⚑ flagged
Causalean.PO.POSystem
For a structural causal model M and an assignment of values to its fixed background variables s, the potential-outcome system induced by M and s satisfies the consistency assumption.
Formal statement
Proof (Lean source)
theorem POSystem.ofSCM_consistency
(M : SCM N Ω) (s : SCM.FixedValues M) :
(POSystem.ofSCM M s).Consistency where
-- ---------------------------------------------------------------
-- Factual consistency
-- ---------------------------------------------------------------
factual := by
intro r Y hY_disj ℓ hFactual
funext v
simp only [POSystem.poVariable, POSystem.ofSCM]
change inducedEval M s r ℓ v.val = inducedEval M s Regime.empty ℓ v.val
rw [inducedEval_empty_eq_evalMap M s ℓ v.val]
-- Clear the let-binding from inducedEval's `hmem`
simp only [inducedEval]
-- Goal: (M.fixSet (regimeTargetN M r) ...).evalMap (combinedFixed M s r) ℓ ⟨v.val.val, _⟩
-- = M.evalMap s ℓ ⟨v.val.val, _⟩
exact SCM.evalMap_fixSet_factual_eq M (regimeTargetN M r)
(regimeTargetN_obs M r) (regimeTargetN_notFixed M r)
s ℓ (combinedFixed M s r)
-- hOld: combinedFixed agrees with s on M.fixed
(fun w hw => combinedFixed_old M s r w hw)
-- hNew: for D ∈ regimeTargetN M r,
-- M.evalMap s ℓ ⟨.random D, _⟩ = combinedFixed M s r ⟨.fixed D, _⟩
(fun D hD => by
obtain ⟨v', hv'tgt, hDval⟩ := regimeTargetN_mem_val M r D hD
have hfa := hFactual v' hv'tgt
simp only [POSystem.ofSCM] at hfa
change inducedEval M s Regime.empty ℓ v' = r.assign v' hv'tgt at hfa
rw [inducedEval_empty_eq_evalMap M s ℓ v'] at hfa
-- hfa : M.evalMap s ℓ ⟨v'.val, _⟩ = r.assign v' hv'tgt : swigΩ Ω v'.val
rw [combinedFixed_new M s r v' hv'tgt D hD hDval]
obtain ⟨v'val, v'prop⟩ := v'
cases hDval
exact hfa)
⟨v.val.val, v.val.property⟩
-- ---------------------------------------------------------------
-- Composition consistency
-- ---------------------------------------------------------------
composition := by
intro r₁ r₂ h Y hY_disj ℓ hIntermediate
funext v
simp only [POSystem.poVariable, POSystem.ofSCM]
unfold inducedEval
-- Sets and proof obligations for the union fixSet
set X₁ := regimeTargetN M r₁ with hX₁_def
set X₂ := regimeTargetN M r₂ with hX₂_def
have hUnion : regimeTargetN M (r₁.sqcup r₂ h) = X₁ ∪ X₂ := by
simp only [hX₁_def, hX₂_def]
exact regimeTargetN_sqcup M r₁ r₂ h
have hObsU : ∀ D ∈ X₁ ∪ X₂, SWIGNode.random D ∈ M.observed :=
fun D hD => regimeTargetN_obs M (r₁.sqcup r₂ h) D (hUnion ▸ hD)
have hFixU : ∀ D ∈ X₁ ∪ X₂, SWIGNode.fixed D ∉ M.fixed :=
fun D hD => regimeTargetN_notFixed M (r₁.sqcup r₂ h) D (hUnion ▸ hD)
-- sxU: combinedFixed M s (r₁.sqcup r₂ h) re-typed to live on M.fixSet (X₁ ∪ X₂)
set sxU : SCM.FixedValues (M.fixSet (X₁ ∪ X₂) hObsU hFixU) :=
fun w => combinedFixed M s (r₁.sqcup r₂ h) ⟨w.val, by
have := w.property
simp only [SCM.fixSet_fixed] at this ⊢
rw [hUnion]; exact this⟩
-- Transport LHS to use M.fixSet (X₁ ∪ X₂)
change (M.fixSet (regimeTargetN M (r₁.sqcup r₂ h)) _ _).evalMap
(combinedFixed M s (r₁.sqcup r₂ h)) ℓ ⟨v.val.val, _⟩ =
(M.fixSet X₁ _ _).evalMap (combinedFixed M s r₁) ℓ ⟨v.val.val, _⟩
refine trans (evalMap_fixSet_transport M hUnion _ _ hObsU hFixU
(combinedFixed M s (r₁.sqcup r₂ h)) sxU
(fun _ _ _ => rfl) ℓ v.val.val ?_ ?_) ?_
· change v.val.val ∈ M.observed ∪ M.unobserved
exact Finset.mem_union_left _ v.val.property
· change v.val.val ∈ M.observed ∪ M.unobserved
exact Finset.mem_union_left _ v.val.property
-- Disjointness of X₁ and X₂ in N
have hDisjN : Disjoint X₁ X₂ := by
simp only [hX₁_def, hX₂_def, regimeTargetN]
exact Finset.disjoint_image (obsName_injective M) |>.mpr (by
rw [Finset.disjoint_left]
intro v hv₁ hv₂
exact Finset.disjoint_left.mp h (Finset.mem_filter.mp hv₁).1 (Finset.mem_filter.mp hv₂).1)
-- Apply evalMap_fixSet_union_eq
refine SCM.evalMap_fixSet_union_eq M X₁ X₂
(regimeTargetN_obs M r₁) (regimeTargetN_notFixed M r₁)
hObsU hFixU ℓ (combinedFixed M s r₁) sxU
?_ ?_ ?_ ⟨v.val.val, v.val.property⟩
· -- hCompat_old: sxU and combinedFixed M s r₁ both equal s on M.fixed
intro w hw
change combinedFixed M s (r₁.sqcup r₂ h) ⟨w, Finset.mem_union_left _ hw⟩ =
combinedFixed M s r₁ ⟨w, Finset.mem_union_left _ hw⟩
rw [combinedFixed_old M s (r₁.sqcup r₂ h) w hw, combinedFixed_old M s r₁ w hw]
· -- hCompat_x₁: sxU ⟨.fixed D, _⟩ = (combinedFixed M s r₁) ⟨.fixed D, _⟩ for D ∈ X₁
intro D hD
-- Pick v' ∈ r₁.target with v'.val = .random D
obtain ⟨v', hv'tgt₁, hDval⟩ := regimeTargetN_mem_val M r₁ D hD
have hv'tgtU : v' ∈ (r₁.sqcup r₂ h).target := Finset.mem_union_left _ hv'tgt₁
have hD_U : D ∈ regimeTargetN M (r₁.sqcup r₂ h) := hUnion ▸ Finset.mem_union_left _ hD
change combinedFixed M s (r₁.sqcup r₂ h) ⟨SWIGNode.fixed D, _⟩ =
combinedFixed M s r₁ ⟨SWIGNode.fixed D, _⟩
rw [combinedFixed_new M s (r₁.sqcup r₂ h) v' hv'tgtU D hD_U hDval,
combinedFixed_new M s r₁ v' hv'tgt₁ D hD hDval,
sqcup_assign_left r₁ r₂ h v' hv'tgt₁]
· -- hIntermediate: (M.fixSet X₁).evalMap (combinedFixed M s r₁) ℓ ⟨.random D, _⟩
-- = sxU ⟨.fixed D, _⟩ for D ∈ X₂
intro D hD
obtain ⟨v', hv'tgt₂, hDval⟩ := regimeTargetN_mem_val M r₂ D hD
-- v' ∉ r₁.target by disjointness
have hv'_not₁ : v' ∉ r₁.target := fun hv₁ => Finset.disjoint_left.mp h hv₁ hv'tgt₂
have hv'tgtU : v' ∈ (r₁.sqcup r₂ h).target := Finset.mem_union_right _ hv'tgt₂
have hD_U : D ∈ regimeTargetN M (r₁.sqcup r₂ h) := hUnion ▸ Finset.mem_union_right _ hD
-- Use hIntermediate from PO consistency: inducedEval M s r₁ ℓ v' = r₂.assign v' hv'tgt₂
have hIA := hIntermediate v' hv'tgt₂
simp only [POSystem.ofSCM] at hIA
unfold inducedEval at hIA
-- hIA : (M.fixSet (regimeTargetN M r₁)).evalMap (combinedFixed M s r₁) ℓ ⟨v'.val, _⟩
-- = r₂.assign v' hv'tgt₂ (at type swigΩ Ω v'.val = Ω D)
change (M.fixSet X₁ _ _).evalMap (combinedFixed M s r₁) ℓ ⟨SWIGNode.random D, _⟩ =
combinedFixed M s (r₁.sqcup r₂ h) ⟨SWIGNode.fixed D, _⟩
rw [combinedFixed_new M s (r₁.sqcup r₂ h) v' hv'tgtU D hD_U hDval]
-- (r₁.sqcup r₂).assign v' hv'tgtU = r₂.assign v' hv'tgt₂
rw [show (r₁.sqcup r₂ h).assign v' hv'tgtU = r₂.assign v' hv'tgt₂ from
sqcup_assign_right r₁ r₂ h v' hv'tgt₂]
-- Now LHS at type Ω D, RHS = cast (...) (r₂.assign v' hv'tgt₂)
-- Use hIA and adjust via cast
have hThis : (M.fixSet X₁ _ _).evalMap (combinedFixed M s r₁) ℓ
⟨v'.val, Finset.mem_union_left _ v'.property⟩ = r₂.assign v' hv'tgt₂ := hIA
-- transport via hDval : v'.val = .random D
obtain ⟨v'val, v'prop⟩ := v'
cases hDval
exact hThis
16 supporting declarations (lemmas, instances)
-
instFintypeObsIdxinstance — The observed-node indices of an induced potential-outcome system form a finite type. -
instDecidableEqObsIdxinstance — Observed-node indices of an induced potential-outcome system have decidable equality. -
instMeasurableObsValueinstance — The value space attached to each observed-node index has the measurable structure inherited from the structural model.instance instMeasurableObsValue (M : SCM N Ω) (v : ObsIdx M) : MeasurableSpace (obsValue M v) := inferInstanceAs (MeasurableSpace (swigΩ Ω v.val)) -
regimeTargetN_obslemma — fixSet-obligation for regimeTargetN: every target D has .random D ∈ M.observed.hypothesesconclusion∀ D ∈ regimeTargetN M r, SWIGNode.random D ∈ M.observedProof (Lean source)
lemma regimeTargetN_obs (M : SCM N Ω) (r : Regime (ObsIdx M) (obsValue M)) : ∀ D ∈ regimeTargetN M r, SWIGNode.random D ∈ M.observed := by intro D hD simp only [regimeTargetN, mem_image] at hD rcases hD with ⟨v, _, rfl⟩ have hspec := Classical.choose_spec (M.observed_is_random v.val v.property) rw [← hspec] exact v.property -
regimeTargetN_notFixedlemma — fixSet-obligation: .fixed D ∉ M.fixed for every structurally eligible regime target D. The target-name translation filters out observed variables whose fixed counterpart is already in M.fixed.hypothesesconclusion∀ D ∈ regimeTargetN M r, SWIGNode.fixed D ∉ M.fixedProof (Lean source)
lemma regimeTargetN_notFixed (M : SCM N Ω) (r : Regime (ObsIdx M) (obsValue M)) : ∀ D ∈ regimeTargetN M r, SWIGNode.fixed D ∉ M.fixed := by intro D hD simp only [regimeTargetN, mem_image] at hD rcases hD with ⟨v, hv, rfl⟩ exact (Finset.mem_filter.mp hv).2 -
inducedEval_measurablelemma — The induced joint evaluation map of a structural model is measurable in the latent draw.hypothesesconclusionMeasurable (inducedEval M s r)Proof (Lean source)
lemma inducedEval_measurable (M : SCM N Ω) (s : SCM.FixedValues M) (r : Regime (ObsIdx M) (obsValue M)) : Measurable (inducedEval M s r) := by let M' := M.fixSet (regimeTargetN M r) (regimeTargetN_obs M r) (regimeTargetN_notFixed M r) refine measurable_pi_lambda _ (fun v => ?_) have h : Measurable (fun ℓ : SCM.LatentValues M => M'.evalMap (combinedFixed M s r) ℓ) := by have hmeas := M'.evalMap_measurable have : Measurable (fun ℓ : SCM.LatentValues M => uncurry M'.evalMap (combinedFixed M s r, ℓ)) := hmeas.comp (Measurable.prod measurable_const measurable_id') simpa [uncurry] using this exact (measurable_pi_apply ⟨v.val, by change v.val ∈ M.observed ∪ M.unobserved exact mem_union_left _ v.property⟩).comp h -
combinedFixed_oldlemma — On original fixed coordinates, combinedFixed agrees with s.hypothesesconclusioncombinedFixed M s r ⟨v, mem_union_left _ hv⟩ = s ⟨v, hv⟩Proof (Lean source)
lemma combinedFixed_old (M : SCM N Ω) (s : SCM.FixedValues M) (r : Regime (ObsIdx M) (obsValue M)) (v : SWIGNode N) (hv : v ∈ M.fixed) : combinedFixed M s r ⟨v, mem_union_left _ hv⟩ = s ⟨v, hv⟩ := by simp only [combinedFixed, dif_pos hv] -
regimeTargetN_eq_image_obsNamelemma — regimeTargetN M r is the image of the structurally eligible regime targets under obsName M.hypothesesconclusionregimeTargetN M r= (r.target.filter (fun v => SWIGNode.fixed (obsName M v) ∉ M.fixed)).image (obsName M)Proof (Lean source)
lemma regimeTargetN_eq_image_obsName (M : SCM N Ω) (r : Regime (ObsIdx M) (obsValue M)) : regimeTargetN M r = (r.target.filter (fun v => SWIGNode.fixed (obsName M v) ∉ M.fixed)).image (obsName M) := rfl -
regimeTargetN_mem_vallemma — Every structural variable name targeted by a translated regime comes from an observed-node index whose observed node is the corresponding random node.hypothesesconclusion∃ v' : ObsIdx M, v' ∈ r.target ∧ v'.val = SWIGNode.random DProof (Lean source)
lemma regimeTargetN_mem_val (M : SCM N Ω) (r : Regime (ObsIdx M) (obsValue M)) (D : N) (hD : D ∈ regimeTargetN M r) : ∃ v' : ObsIdx M, v' ∈ r.target ∧ v'.val = SWIGNode.random D := by simp only [regimeTargetN, mem_image] at hD rcases hD with ⟨v', hv'tgt, hDeq⟩ exact ⟨v', (Finset.mem_filter.mp hv'tgt).1, hDeq ▸ obsName_spec M v'⟩ -
obsIdx_val_injectivelemma — Two elements of ObsIdx M with the same .val are equal (injectivity of the coercion).Proof (Lean source)
lemma obsIdx_val_injective {M : SCM N Ω} {v w : ObsIdx M} (h : v.val = w.val) : v = w := Subtype.ext h -
obsName_injectivelemma — obsName M is injective: obsName v = obsName w → v = w.Proof (Lean source)
lemma obsName_injective (M : SCM N Ω) : Injective (obsName M) := fun v w hvw => obsIdx_val_injective (by rw [obsName_spec M v, obsName_spec M w, hvw]) -
sqcup_assign_leftlemma — Regime.sqcup agrees with r₁ on r₁.target.hypothesesconclusion(r₁.sqcup r₂ h).assign v (mem_union_left _ hv) = r₁.assign v hvProof (Lean source)
lemma sqcup_assign_left {V : Type*} [DecidableEq V] {X : V → Type*} [∀ v, MeasurableSpace (X v)] (r₁ r₂ : Regime V X) (h : r₁.Disjoint r₂) (v : V) (hv : v ∈ r₁.target) : (r₁.sqcup r₂ h).assign v (mem_union_left _ hv) = r₁.assign v hv := by simp [Regime.sqcup, Regime.leftBiasedUnion, hv] -
sqcup_assign_rightlemma — Regime.sqcup agrees with r₂ on r₂.target.hypothesesconclusion(r₁.sqcup r₂ h).assign v (mem_union_right _ hv) = r₂.assign v hvProof (Lean source)
lemma sqcup_assign_right {V : Type*} [DecidableEq V] {X : V → Type*} [∀ v, MeasurableSpace (X v)] (r₁ r₂ : Regime V X) (h : r₁.Disjoint r₂) (v : V) (hv : v ∈ r₂.target) : (r₁.sqcup r₂ h).assign v (mem_union_right _ hv) = r₂.assign v hv := by have h1 : v ∉ r₁.target := fun hv₁ => Finset.disjoint_left.mp h hv₁ hv simp [Regime.sqcup, Regime.leftBiasedUnion, h1] -
combinedFixed_newlemma — On new intervention coordinates, combinedFixed at ⟨.fixed D, _⟩ equals r.assign v' hv'tgt, both at type Ω D. The internal Classical.choose witness is identified with v' by uniqueness (both have .val = .random D); the cast chain collapses via cast_heq + proof_irrel_heq.hypothesesM :SCM N Ωs :SCM.FixedValues Mv' :ObsIdx Mhv'tgt :v' ∈ r.targetD :NhD :D ∈ regimeTargetN M rhDval :v'.val = SWIGNode.random Dconclusion(combinedFixed M s r ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩ : Ω D)Proof (Lean source)
lemma combinedFixed_new (M : SCM N Ω) (s : SCM.FixedValues M) (r : Regime (ObsIdx M) (obsValue M)) (v' : ObsIdx M) (hv'tgt : v' ∈ r.target) (D : N) (hD : D ∈ regimeTargetN M r) (hDval : v'.val = SWIGNode.random D) : (combinedFixed M s r ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩ : Ω D) = cast (congrArg (swigΩ Ω) hDval) (r.assign v' hv'tgt) := by have hFD_notFix : SWIGNode.fixed D ∉ M.fixed := regimeTargetN_notFixed M r D hD unfold combinedFixed rw [dif_neg hFD_notFix] set hExist := combinedFixed_exists M r ⟨SWIGNode.fixed D, _⟩ hFD_notFix with hE_def have hChosen : choose hExist = v' := by have hspec := Classical.choose_spec hExist apply obsIdx_val_injective have h_obsname : obsName M (choose hExist) = D := by have := hspec.2; injection this rw [obsName_spec M (choose hExist), h_obsname, hDval] apply eq_of_heq refine HEq.trans (cast_heq _ _) ?_ refine HEq.trans ?_ (cast_heq _ _).symm congr 1 exact proof_irrel_heq _ _ -
regimeTargetN_emptylemma — regimeTargetN M Regime.empty = ∅.Proof (Lean source)
@[simp] lemma regimeTargetN_empty (M : SCM N Ω) : regimeTargetN M (Regime.empty (V := ObsIdx M) (X := obsValue M)) = ∅ := by simp [regimeTargetN, Regime.empty] -
inducedEval_empty_eq_evalMaplemma — inducedEval at Regime.empty equals M.evalMap s at the same latent.hypothesesconclusioninducedEval M s Regime.empty ℓ v= M.evalMap s ℓ ⟨v.val, mem_union_left _ v.property⟩Proof (Lean source)
lemma inducedEval_empty_eq_evalMap (M : SCM N Ω) (s : SCM.FixedValues M) (ℓ : SCM.LatentValues M) (v : ObsIdx M) : inducedEval M s Regime.empty ℓ v = M.evalMap s ℓ ⟨v.val, mem_union_left _ v.property⟩ := by -- `inducedEval M s Regime.empty ℓ v = (M.fixSet ∅ ...).evalMap -- (combinedFixed M s Regime.empty) ℓ ⟨v.val, _⟩` -- Use `evalMap_eq_of_equiv (fixSet_empty_equiv M ...)`. unfold inducedEval -- RHS of inducedEval: `(M.fixSet ∅ ...).evalMap (combinedFixed M s Regime.empty) ℓ ⟨v.val, _⟩` let hObs : ∀ D ∈ (∅ : Finset N), SWIGNode.random D ∈ M.observed := by simp let hFix : ∀ D ∈ (∅ : Finset N), SWIGNode.fixed D ∉ M.fixed := by simp let hEq := SCM.fixSet_empty_equiv M apply SCM.evalMap_eq_of_equiv hEq.1 hEq.2.2.1 · -- Fixed coords agree: combinedFixed at M.fixed = s intro d hd₁ hd₂ -- `(M.fixSet ∅).fixed = M.fixed ∪ ∅ = M.fixed` (by rfl since ∅.image = ∅) simp only [SCM.fixSet_fixed, Finset.image_empty, union_empty] at hd₁ exact combinedFixed_old M s Regime.empty d hd₁ · -- Latent coords: `(M.fixSet ∅).unobserved = M.unobserved` (by rfl) intro u hu₁ hu₂ rfl
FromSCMCondIndep 1 core · 0 supporting This file connects graphical conditional independence in an SCM to counterfactual conditional independence in the potential-outcome system induced by that SCM. ★ ofSCM_condIndepCF_of_dSep
Conditional-Independence Bridge from SCMs to Induced PO Systems
This file connects graphical conditional independence in an SCM to
counterfactual conditional independence in the potential-outcome system induced
by that SCM. The bridge is stated with explicit value-correspondence
hypotheses: consumers identify the PO regimed values with measurable functions
of the SWIG coordinate projections whose d-separation they can prove. The main
theorem, POSystem.ofSCM_condIndepCF_of_dSep, pulls a global-Markov
CondIndepFun statement through the induced-system evaluation map and optional
measurable post-processing of the X- and Y-side values.
theorem ofSCM_condIndepCF_of_dSep reviewed
⚑ flagged
Causalean.PO.POSystem
SCM-to-PO conditional-independence bridge under d-separation. Fix a structural causal model M with a fixed-value assignment s, and SWIG node sets that are each contained in the model's random variables and pairwise disjoint from one another. Suppose the first node set is d-separated from the second by the third in the model's DAG. Suppose further that there is a measurable value-space map aMap for the first node set and a measurable value-space map BMap for the second node set such that, under the latent draw, the potential-outcome value of a regimed variable a equals aMap applied to the projection of the evaluated model state onto the first node set, the joint value of a counterfactual bundle B equals BMap applied to the projection onto the second node set, and the conditioning value of a regimed variable c equals the projection onto the third node set. Then, in the potential-outcome system induced by M at s, a and B are conditionally independent given c.
Formal statement
hypotheses
M :
SCM N Ω
s :
SCM.FixedValues M
StandardBorelSpace M.RandomValues
StandardBorelSpace M.LatentValues
StandardBorelSpace (POSystem.ofSCM M s).Ω
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
∀ s' :
M.FixedValues, IsFiniteMeasure (M.jointKernel s')
hX :
X ⊆ M.randomVars
hY :
Y ⊆ M.randomVars
hZ :
Z ⊆ M.randomVars
hDisj_XY :
Disjoint X Y
hDisj_XZ :
Disjoint X Z
hDisj_YZ :
Disjoint Y Z
hdSep :
M.dag.dSep X Y Z
α :
a :
RegimedVar (POSystem.ofSCM M s) α
B :
POCFBundle (POSystem.ofSCM M s)
StandardBorelSpace (∀ i : Fin B.n, B.type i)
Nonempty (∀ i : Fin B.n, B.type i)
c :
haMap :
Measurable aMap
hBMap :
Measurable BMap
ha_value :
a.value
= aMap ∘ valuesProjection (Ω := swigΩ Ω) hX ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ)
hB_value :
B.jointValue
= BMap ∘ valuesProjection (Ω := swigΩ Ω) hY ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ)
hc_value :
c.value = valuesProjection (Ω := swigΩ Ω) hZ ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ)
conclusion
(POSystem.ofSCM M s).CondIndepCF a B c (POSystem.ofSCM M s).μ
Proof (Lean source)
theorem ofSCM_condIndepCF_of_dSep
(M : SCM N Ω) (s : SCM.FixedValues M)
[StandardBorelSpace M.RandomValues] [StandardBorelSpace M.LatentValues]
[StandardBorelSpace (POSystem.ofSCM M s).Ω]
[∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)]
[∀ s' : M.FixedValues, IsFiniteMeasure (M.jointKernel s')]
{X Y Z : Finset (SWIGNode N)}
(hX : X ⊆ M.randomVars) (hY : Y ⊆ M.randomVars) (hZ : Z ⊆ M.randomVars)
(hDisj_XY : Disjoint X Y) (hDisj_XZ : Disjoint X Z) (hDisj_YZ : Disjoint Y Z)
(hdSep : M.dag.dSep X Y Z)
{α : Type*} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
(a : RegimedVar (POSystem.ofSCM M s) α)
(B : POCFBundle (POSystem.ofSCM M s))
[StandardBorelSpace (∀ i : Fin B.n, B.type i)] [Nonempty (∀ i : Fin B.n, B.type i)]
(c : RegimedVar (POSystem.ofSCM M s) (ValuesOn Z (swigΩ Ω)))
(aMap : ValuesOn X (swigΩ Ω) → α)
(BMap : ValuesOn Y (swigΩ Ω) → (∀ i : Fin B.n, B.type i))
(haMap : Measurable aMap) (hBMap : Measurable BMap)
(ha_value : a.value =
aMap ∘ valuesProjection (Ω := swigΩ Ω) hX ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ))
(hB_value : B.jointValue =
BMap ∘ valuesProjection (Ω := swigΩ Ω) hY ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ))
(hc_value : c.value =
valuesProjection (Ω := swigΩ Ω) hZ ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ)) :
(POSystem.ofSCM M s).CondIndepCF a B c (POSystem.ofSCM M s).μ := by
let E : M.LatentValues → M.RandomValues := fun ℓ => M.evalMap s ℓ
have hE : Measurable E := by
have hmeas := M.evalMap_measurable
simpa [E, uncurry, Function.comp_def] using
hmeas.comp (prodMk measurable_const measurable_id)
have hFull : SCM.FullCondIndep M X Y Z hX hY hZ (M.jointKernel s) :=
SCM.full_globalMarkov M X Y Z hX hY hZ hdSep s
have hJointEq : M.jointKernel s = M.latentProduct.map E := by
simpa [E] using SCM.jointKernel_apply_eq M s
haveI : IsFiniteMeasure (M.latentProduct.map E) := hJointEq ▸
(inferInstance : IsFiniteMeasure (M.jointKernel s))
have hFullMap : CondIndepFun
(comap (valuesProjection (Ω := swigΩ Ω) hZ) inferInstance)
(comap_valuesProjection_le (Ω' := swigΩ Ω) hZ)
(valuesProjection (Ω := swigΩ Ω) hX)
(valuesProjection (Ω := swigΩ Ω) hY)
(M.latentProduct.map E) := by
simpa [SCM.FullCondIndep, hJointEq] using hFull
have hPull : CondIndepFun
(comap
(valuesProjection (Ω := swigΩ Ω) hZ ∘ E) inferInstance)
(comap_le ((measurable_valuesProjection (Ω' := swigΩ Ω) hZ).comp hE))
(valuesProjection (Ω := swigΩ Ω) hX ∘ E)
(valuesProjection (Ω := swigΩ Ω) hY ∘ E)
M.latentProduct :=
condIndepFun_comp_of_map hE
(measurable_valuesProjection (Ω' := swigΩ Ω) hX)
(measurable_valuesProjection (Ω' := swigΩ Ω) hY)
(measurable_valuesProjection (Ω' := swigΩ Ω) hZ)
hFullMap
have hComp : CondIndepFun
(comap
(valuesProjection (Ω := swigΩ Ω) hZ ∘ E) inferInstance)
(comap_le ((measurable_valuesProjection (Ω' := swigΩ Ω) hZ).comp hE))
(aMap ∘ valuesProjection (Ω := swigΩ Ω) hX ∘ E)
(BMap ∘ valuesProjection (Ω := swigΩ Ω) hY ∘ E)
M.latentProduct := by
simpa [Function.comp_assoc] using hPull.comp haMap hBMap
unfold CondIndepCF
convert hComp using 3
· rfl
· exact heq_of_eq hc_value
· exact HEq.rfl
· exact heq_of_eq ha_value
· exact heq_of_eq hB_value
· exact HEq.rfl
Induce 3 core · 12 supporting This file builds the potential-outcome system induced by restricting attention to a finite set of variables. ★ restrict_consistency
Restricted Potential-Outcome Systems
This file builds the potential-outcome system induced by restricting attention
to a finite set of variables. POSystem.liftRegime embeds regimes on the
restricted variable set back into the ambient system, POSystem.restrict builds
the sub-system itself, and the lift lemmas show that targets, assignments,
empty regimes, disjointness, and Regime.sqcup are preserved. The theorem
POSystem.restrict_consistency proves that consistency of the original system
transfers to the restricted system.
def liftRegime reviewed
⚑ flagged
Causalean.PO.POSystem
For a potential-outcome system, a finite set of variables, and an intervention regime whose variables all lie in that finite set, this construction returns the corresponding intervention regime on the original system by viewing each restricted variable as a variable of the original system.
Definition (Lean source)
def liftRegime
(r' : Regime (↥R) (fun v : ↥R => P.X v.val)) : Regime P.V P.X where
target := r'.target.map ⟨Subtype.val, Subtype.val_injective⟩
assign v hv :=
have hvR : v ∈ R := by
rcases Finset.mem_map.mp hv with ⟨w, _, rfl⟩
exact w.property
have hwT : (⟨v, hvR⟩ : ↥R) ∈ r'.target := by
rcases Finset.mem_map.mp hv with ⟨w, hw, hwv⟩
have hwwR : (⟨v, hvR⟩ : ↥R) = w := Subtype.ext hwv.symm
exact hwwR ▸ hw
r'.assign ⟨v, hvR⟩ hwT
def restrict reviewed
⚑ flagged
Causalean.PO.POSystem
For a potential-outcome system and a finite set of variables, the restricted potential-outcome system has that finite set as its variable collection, keeps the same sample space and probability measure, and evaluates restricted intervention regimes by first lifting them back to intervention regimes of the original system.
Definition (Lean source)
theorem restrict_consistency reviewed
⚑ flagged
Causalean.PO.POSystem
Restriction preserves consistency. If the ambient potential-outcome system P is consistent (SUTVA holds), then the system P restricted to R is consistent as well.
Formal statement
Proof (Lean source)
theorem restrict_consistency (hP : P.Consistency) :
(P.restrict R).Consistency where
factual := by
intro r' Y hYr ω hag
-- Build the ambient FactualAgrees witness.
have hagP : P.FactualAgrees (P.liftRegime R r') ω := by
intro v hv
rcases Finset.mem_map.mp hv with ⟨w, hw, rfl⟩
have hv' : (w.val : P.V) ∈ (P.liftRegime R r').target := hv
change P.eval Regime.empty ω w.val =
(P.liftRegime R r').assign w.val hv'
rw [P.liftRegime_assign R r' w hw]
exact hag w hw
-- Lift Y.
set Yamb : Finset P.V :=
Y.map ⟨Subtype.val, Subtype.val_injective⟩ with hYamb_def
have hYr_amb : _root_.Disjoint Yamb (P.liftRegime R r').target := by
rw [hYamb_def, Finset.disjoint_left]
intro v hvY hvr
rcases Finset.mem_map.mp hvY with ⟨y, hy, rfl⟩
rcases Finset.mem_map.mp hvr with ⟨w, hw, hwy⟩
have : y = w := val_injective hwy.symm
subst this
exact (Finset.disjoint_left.mp hYr hy) hw
have hpv := hP.factual (P.liftRegime R r') Yamb hYr_amb ω hagP
-- Pointwise equality on Y.
funext y
have hyamb : (y.val.val : P.V) ∈ Yamb := by
rw [hYamb_def]; exact Finset.mem_map.mpr ⟨y.val, y.property, rfl⟩
have heq := congrArg (fun f => f ⟨y.val.val, hyamb⟩) hpv
-- Goal: (P.restrict R).poVariable r' Y ω y = (P.restrict R).poVariable Regime.empty Y ω y
change P.eval (P.liftRegime R r') ω y.val.val =
P.eval (P.liftRegime R Regime.empty) ω y.val.val
rw [liftRegime_empty]
exact heq
composition := by
intro r₁' r₂' hd Y hYr ω hag
-- Build ambient IntermediateAgrees.
have hagP : P.IntermediateAgrees (P.liftRegime R r₁') (P.liftRegime R r₂') ω := by
intro v hv
rcases Finset.mem_map.mp hv with ⟨w, hw, rfl⟩
have hv' : (w.val : P.V) ∈ (P.liftRegime R r₂').target := hv
change P.eval (P.liftRegime R r₁') ω w.val =
(P.liftRegime R r₂').assign w.val hv'
rw [P.liftRegime_assign R r₂' w hw]
exact hag w hw
-- Lift Y.
set Yamb : Finset P.V :=
Y.map ⟨Subtype.val, Subtype.val_injective⟩ with hYamb_def
have hd_amb : (P.liftRegime R r₁').Disjoint (P.liftRegime R r₂') :=
P.liftRegime_disjoint R hd
have hYr_amb : _root_.Disjoint Yamb
((P.liftRegime R r₁').target ∪ (P.liftRegime R r₂').target) := by
rw [hYamb_def, Finset.disjoint_left]
intro v hvY hvU
rcases Finset.mem_map.mp hvY with ⟨y, hy, rfl⟩
rcases Finset.mem_union.mp hvU with hv | hv
· rcases Finset.mem_map.mp hv with ⟨w, hw, hwy⟩
have : y = w := val_injective hwy.symm
subst this
exact (Finset.disjoint_left.mp hYr hy) (mem_union_left _ hw)
· rcases Finset.mem_map.mp hv with ⟨w, hw, hwy⟩
have : y = w := val_injective hwy.symm
subst this
exact (Finset.disjoint_left.mp hYr hy) (mem_union_right _ hw)
have hpv := hP.composition (P.liftRegime R r₁') (P.liftRegime R r₂')
hd_amb Yamb hYr_amb ω hagP
funext y
have hyamb : (y.val.val : P.V) ∈ Yamb := by
rw [hYamb_def]; exact Finset.mem_map.mpr ⟨y.val, y.property, rfl⟩
have heq := congrArg (fun f => f ⟨y.val.val, hyamb⟩) hpv
change P.eval (P.liftRegime R (r₁'.sqcup r₂' hd)) ω y.val.val =
P.eval (P.liftRegime R r₁') ω y.val.val
have hsq :
P.liftRegime R (r₁'.sqcup r₂' hd) =
(P.liftRegime R r₁').sqcup (P.liftRegime R r₂')
(P.liftRegime_disjoint R hd) := by
exact P.liftRegime_sqcup R hd
rw [hsq]
exact heq
12 supporting declarations (lemmas, instances)
-
liftRegime_targetlemma — The target of a lifted restricted regime is the image of the restricted target in the original variable set.hypothesesr' :Regime (↥R) (fun v : ↥R => P.X v.val)conclusion(P.liftRegime R r').target = r'.target.map ⟨Subtype.val, Subtype.val_injective⟩Proof (Lean source)
@[simp] lemma liftRegime_target (r' : Regime (↥R) (fun v : ↥R => P.X v.val)) : (P.liftRegime R r').target = r'.target.map ⟨Subtype.val, Subtype.val_injective⟩ := rfl -
liftRegime_assignlemma — Reading the lifted assignment at a known sub-regime member returns the original sub-assignment. Membership proofs are propositional, so the ambient hv is irrelevant.hypothesesr' :Regime (↥R) (fun v : ↥R => P.X v.val)w :↥Rhw :w ∈ r'.targethv :(w.val : P.V) ∈ (P.liftRegime R r').targetconclusion(P.liftRegime R r').assign w.val hv = r'.assign w hwProof (Lean source)
lemma liftRegime_assign (r' : Regime (↥R) (fun v : ↥R => P.X v.val)) (w : ↥R) (hw : w ∈ r'.target) (hv : (w.val : P.V) ∈ (P.liftRegime R r').target) : (P.liftRegime R r').assign w.val hv = r'.assign w hw := by change r'.assign ⟨w.val, w.property⟩ _ = r'.assign w hw congr 1 -
liftRegime_emptylemma — Lifting the empty restricted regime gives the empty regime on the original system.Proof (Lean source)
@[simp] lemma liftRegime_empty : P.liftRegime R (Regime.empty : Regime (↥R) (fun v : ↥R => P.X v.val)) = (Regime.empty : Regime P.V P.X) := by apply Regime.ext · simp [liftRegime_target, Regime.empty] · intro v hv _ simp [liftRegime_target, Regime.empty] at hv -
restrict_Vlemma — The variable type of the restricted potential-outcome system is the chosen finite set of variables.conclusion(P.restrict R).V = ↥RProof (Lean source)
@[simp] lemma restrict_V : (P.restrict R).V = ↥R := rfl -
restrict_Xlemma — The value space in the restricted system is the original value space at the underlying variable.hypothesesv :↥Rconclusion(P.restrict R).X v = P.X v.valProof (Lean source)
@[simp] lemma restrict_X (v : ↥R) : (P.restrict R).X v = P.X v.val := rfl -
restrict_Ωlemma — The restricted potential-outcome system uses the same sample space as the original system.conclusion(P.restrict R).Ω = P.ΩProof (Lean source)
@[simp] lemma restrict_Ω : (P.restrict R).Ω = P.Ω := rfl -
restrict_μlemma — The restricted potential-outcome system uses the same probability measure as the original system.conclusion(P.restrict R).μ = P.μProof (Lean source)
@[simp] lemma restrict_μ : (P.restrict R).μ = P.μ := rfl -
restrict_evallemma — Evaluation in the restricted system is evaluation in the original system after lifting the restricted regime.hypothesesconclusion(P.restrict R).eval r' ω v = P.eval (P.liftRegime R r') ω v.valProof (Lean source)
@[simp] lemma restrict_eval (r' : Regime (↥R) (fun v : ↥R => P.X v.val)) (ω : P.Ω) (v : ↥R) : (P.restrict R).eval r' ω v = P.eval (P.liftRegime R r') ω v.val := rfl -
restrict_componentlemma — A coordinate potential outcome in the restricted system agrees with the original coordinate after lifting the regime.hypothesesr' :Regime (↥R) (fun v : ↥R => P.X v.val)v :↥Rconclusion(P.restrict R).component r' v = P.component (P.liftRegime R r') v.valProof (Lean source)
@[simp] lemma restrict_component (r' : Regime (↥R) (fun v : ↥R => P.X v.val)) (v : ↥R) : (P.restrict R).component r' v = P.component (P.liftRegime R r') v.val := rfl -
liftRegime_disjointlemma — Disjoint restricted regimes remain disjoint after lifting them to the original system.hypothesesr₁' r₂' :Regime (↥R) (fun v : ↥R => P.X v.val)h :r₁'.Disjoint r₂'conclusion(P.liftRegime R r₁').Disjoint (P.liftRegime R r₂')Proof (Lean source)
lemma liftRegime_disjoint {r₁' r₂' : Regime (↥R) (fun v : ↥R => P.X v.val)} (h : r₁'.Disjoint r₂') : (P.liftRegime R r₁').Disjoint (P.liftRegime R r₂') := by rw [Regime.Disjoint, liftRegime_target, liftRegime_target, Finset.disjoint_left] intro v hv₁ hv₂ rcases Finset.mem_map.mp hv₁ with ⟨w₁, hw₁, rfl⟩ rcases Finset.mem_map.mp hv₂ with ⟨w₂, hw₂, hw₂eq⟩ have : w₁ = w₂ := val_injective hw₂eq.symm subst this exact (Finset.disjoint_left.mp h hw₁) hw₂ -
liftRegime_sqcup_targetlemma — The lift commutes with Regime.sqcup (target equality).hypothesesr₁' r₂' :Regime (↥R) (fun v : ↥R => P.X v.val)h :r₁'.Disjoint r₂'Proof (Lean source)
lemma liftRegime_sqcup_target {r₁' r₂' : Regime (↥R) (fun v : ↥R => P.X v.val)} (h : r₁'.Disjoint r₂') : (P.liftRegime R (r₁'.sqcup r₂' h)).target = (P.liftRegime R r₁').target ∪ (P.liftRegime R r₂').target := by simp [liftRegime_target, Finset.map_union] -
liftRegime_sqcuplemma — The lift commutes with Regime.sqcup (full equality).hypothesesr₁' r₂' :Regime (↥R) (fun v : ↥R => P.X v.val)h :r₁'.Disjoint r₂'conclusionP.liftRegime R (r₁'.sqcup r₂' h)= (P.liftRegime R r₁').sqcup (P.liftRegime R r₂') (P.liftRegime_disjoint R h)Proof (Lean source)
lemma liftRegime_sqcup {r₁' r₂' : Regime (↥R) (fun v : ↥R => P.X v.val)} (h : r₁'.Disjoint r₂') : P.liftRegime R (r₁'.sqcup r₂' h) = (P.liftRegime R r₁').sqcup (P.liftRegime R r₂') (P.liftRegime_disjoint R h) := by apply Regime.ext (P.liftRegime_sqcup_target R h) intro v hv hv2 -- v lies in the lifted union, so v = w.val for some w in r₁' ∪ r₂'. rw [liftRegime_target] at hv rcases Finset.mem_map.mp hv with ⟨w, hwU, rfl⟩ -- Normalize both membership proofs to talk about w.val instead of the -- raw embedding application. have hv1' : (w.val : P.V) ∈ (P.liftRegime R (r₁'.sqcup r₂' h)).target := by rw [liftRegime_target]; exact Finset.mem_map.mpr ⟨w, hwU, rfl⟩ have hv2' : (w.val : P.V) ∈ ((P.liftRegime R r₁').sqcup (P.liftRegime R r₂') (P.liftRegime_disjoint R h)).target := by rw [Regime.sqcup_target] rcases Finset.mem_union.mp hwU with hw | hw · exact mem_union_left _ (Finset.mem_map.mpr ⟨w, hw, rfl⟩) · exact mem_union_right _ (Finset.mem_map.mpr ⟨w, hw, rfl⟩) change (P.liftRegime R (r₁'.sqcup r₂' h)).assign w.val hv1' = ((P.liftRegime R r₁').sqcup (P.liftRegime R r₂') (P.liftRegime_disjoint R h)).assign w.val hv2' rw [P.liftRegime_assign R (r₁'.sqcup r₂' h) w hwU] -- Now goal: (r₁'.sqcup r₂' h).assign w hwU = (sqcup of lifts).assign w.val hv2' by_cases hw1 : w ∈ r₁'.target · have hv_in_lift1 : (w.val : P.V) ∈ (P.liftRegime R r₁').target := Finset.mem_map.mpr ⟨w, hw1, rfl⟩ rw [Regime.sqcup_assign_pos _ _ _ _ hw1, Regime.sqcup_assign_pos _ _ _ _ hv_in_lift1, P.liftRegime_assign R r₁' w hw1] · have hw2 : w ∈ r₂'.target := by rcases Finset.mem_union.mp hwU with hw | hw · exact (hw1 hw).elim · exact hw have hv_not_in_lift1 : (w.val : P.V) ∉ (P.liftRegime R r₁').target := by rw [liftRegime_target] intro hv1 rcases Finset.mem_map.mp hv1 with ⟨w', hw', heq⟩ have : w = w' := Subtype.val_injective heq.symm subst this exact hw1 hw' have hv_in_lift2 : (w.val : P.V) ∈ (P.liftRegime R r₂').target := Finset.mem_map.mpr ⟨w, hw2, rfl⟩ rw [Regime.sqcup_assign_neg _ _ _ _ hw1 hw2, Regime.sqcup_assign_neg _ _ _ _ hv_not_in_lift1 hv_in_lift2, P.liftRegime_assign R r₂' w hw2]