SCM.ID

Φ :

CausalQuery N Ω α

M₁ M₂ :

SCM N Ω

M₁.toSWIGGraph = G

M₂.toSWIGGraph = G

obsEquiv M₁ M₂

def

Identifiable G Φ :

Prop

given by

Φ M₁ = Φ M₂

Causalean.SCM.ID.Identifiable · Causalean/SCM/ID/Identifiable.lean:105 · uses SWIGGraph , CausalQuery

def NonIdentifiable reviewed

Causalean.SCM.ID

For a finite node-label set, measurable node-value spaces, a SWIG graph, and a causal query, non-identifiability means that the query is not identifiable from the observational distribution: it is not the case that every two models with that graph and equal observational probability kernels have equal query values.

Definition (Lean source)

parameters

N :

Type u_1

N → Type*

shared

∀ n, MeasurableSpace (Ω n)

α :

Type*

G :

Φ :

CausalQuery N Ω α

def

NonIdentifiable G Φ :

Prop

given by

¬Identifiable G Φ

Causalean.SCM.ID.NonIdentifiable · Causalean/SCM/ID/Identifiable.lean:127 · uses SWIGGraph , CausalQuery

theorem nonIdentifiable_iff reviewed

Causalean.SCM.ID

For a SWIG graph G and a causal query Φ, the causal query is non-identifiable from the observational distribution if and only if there exist two causal models with SWIG graph G and the same observational law that disagree on the value of Φ.

Formal statement

hypotheses

N :

Type u_1

N → Type*

shared

∀ n, MeasurableSpace (Ω n)

α :

Type*

G :

Φ :

CausalQuery N Ω α

conclusion

NonIdentifiable G Φ

↔ ∃ M₁ M₂ : SCM N Ω, M₁.toSWIGGraph = G ∧ M₂.toSWIGGraph = G ∧ obsEquiv M₁ M₂ ∧ Φ M₁ ≠ Φ M₂

Proof (Lean source)

theorem nonIdentifiable_iff {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)] {α : Type*} (G : SWIGGraph N) (Φ : CausalQuery N Ω α) : NonIdentifiable G Φ ↔ ∃ M₁ M₂ : SCM N Ω, M₁.toSWIGGraph = G ∧ M₂.toSWIGGraph = G ∧ obsEquiv M₁ M₂ ∧ Φ M₁ ≠ Φ M₂ := by simp only [NonIdentifiable, Identifiable, not_forall] constructor · intro ⟨M₁, M₂, h1, h2, h3, h4⟩ exact ⟨M₁, M₂, h1, h2, h3, h4⟩ · intro ⟨M₁, M₂, h1, h2, h3, h4⟩ exact ⟨M₁, M₂, h1, h2, h3, h4⟩

Causalean.SCM.ID.nonIdentifiable_iff · Causalean/SCM/ID/Identifiable.lean:139 · uses SWIGGraph , SCM , CausalQuery , NonIdentifiable , obsEquiv

def IdentifiableUnder reviewed

Causalean.SCM.ID

For a finite node-label set, measurable node-value spaces, a SWIG graph, a functional-assumption predicate, a structural-assumption predicate, and a causal query, identifiability under the two assumptions means that every pair of models whose SWIG graphs equal the given graph, which both satisfy each predicate, and which have equal observational probability kernels, has the same query value.

Definition (Lean source)

parameters

N :

Type u_1

N → Type*

shared

∀ n, MeasurableSpace (Ω n)

α :

Type*

G :

Af :

SCM N Ω → Prop

functional assumptions

As :

SCM N Ω → Prop

structural assumptions

Φ :

CausalQuery N Ω α

M₁ M₂ :

SCM N Ω

M₁.toSWIGGraph = G

M₂.toSWIGGraph = G

Af M₁

Af M₂

As M₁

As M₂

obsEquiv M₁ M₂

def

IdentifiableUnder G Af As Φ :

Prop

given by

Φ M₁ = Φ M₂

Causalean.SCM.ID.IdentifiableUnder · Causalean/SCM/ID/Identifiable.lean:161 · uses SWIGGraph , SCM , CausalQuery

theorem identifiableUnder_mono reviewed

Causalean.SCM.ID

Monotonicity of identifiability under assumptions. Fix functional-assumption predicates Af₁, Af₂ and structural-assumption predicates As₁, As₂ on causal models sharing a graph G, together with a causal query Φ. If every model satisfying Af₂ also satisfies Af₁, every model satisfying As₂ also satisfies As₁, and Φ is identifiable under the assumption pair (Af₁, As₁), then Φ is identifiable under (Af₂, As₂): passing to the more restrictive assumption predicates Af₂, As₂ cannot destroy identifiability.

Formal statement

hypotheses

N :

Type u_1

N → Type*

shared

∀ n, MeasurableSpace (Ω n)

α :

Type*

G :

Af₁ Af₂ :

SCM N Ω → Prop

As₁ As₂ :

SCM N Ω → Prop

Φ :

CausalQuery N Ω α

hf :

∀ M

Af₂ M

then

Af₁ M

hs :

∀ M

As₂ M

then

As₁ M

h_id :

IdentifiableUnder G Af₁ As₁ Φ

conclusion

IdentifiableUnder G Af₂ As₂ Φ

Proof (Lean source)

theorem identifiableUnder_mono {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)] {α : Type*} (G : SWIGGraph N) (Af₁ Af₂ : SCM N Ω → Prop) (As₁ As₂ : SCM N Ω → Prop) (Φ : CausalQuery N Ω α) (hf : ∀ M, Af₂ M → Af₁ M) (hs : ∀ M, As₂ M → As₁ M) (h_id : IdentifiableUnder G Af₁ As₁ Φ) : IdentifiableUnder G Af₂ As₂ Φ := fun M₁ M₂ hG₁ hG₂ hAf₁ hAf₂ hAs₁ hAs₂ hObs => h_id M₁ M₂ hG₁ hG₂ (hf M₁ hAf₁) (hf M₂ hAf₂) (hs M₁ hAs₁) (hs M₂ hAs₂) hObs

Causalean.SCM.ID.identifiableUnder_mono · Causalean/SCM/ID/Identifiable.lean:195 · uses SWIGGraph , SCM , CausalQuery , IdentifiableUnder

1 supporting declaration (lemmas, instances)

identifiable_eq_identifiableUnder_true theorem — Identifiability without additional assumptions is the special case where both Af and As are trivially satisfied.

hypotheses

N :

Type u_1
N → Type*
shared

∀ n, MeasurableSpace (Ω n)

α :

Type*

G :

SWIGGraph N

Φ :

CausalQuery N Ω α

conclusion

Identifiable G Φ ↔ IdentifiableUnder G (fun _ => True) (fun _ => True) Φ

Proof (Lean source)

theorem identifiable_eq_identifiableUnder_true {Ω : N → Type*} [∀ n, MeasurableSpace (Ω n)] {α : Type*} (G : SWIGGraph N) (Φ : CausalQuery N Ω α) : Identifiable G Φ ↔ IdentifiableUnder G (fun _ => True) (fun _ => True) Φ := by simp [Identifiable, IdentifiableUnder]

Causalean.SCM.ID.identifiable_eq_identifiableUnder_true · Causalean/SCM/ID/Identifiable.lean:187

BackdoorCriterion 2 core · 0 supporting This file defines the SWIG backdoor criterion used by SCM backdoor identification and proves the Rule 3 marginal-invariance step for the adjustment set. ★ backdoor_rule3_Z_marginal

Backdoor criterion and Rule 3 marginal leg

This file defines the SWIG backdoor criterion used by SCM backdoor identification and proves the Rule 3 marginal-invariance step for the adjustment set. The full backdoor completeness and identifiability theorems live in Causalean/SCM/ID/Backdoor.lean; this module supplies their reusable graphical criterion and the Z-marginal equality needed in the do-calculus assembly.

def backdoorCriterion reviewed

Causalean.SWIGGraph

Given a SWIG graph, a finite treatment-variable set $X$ , the condition that the random copy of every treatment variable is observed, the condition that the fixed copy of no treatment variable is already fixed, a finite outcome-vertex set $Y$ , and a finite candidate adjustment-vertex set $Z$ , the backdoor criterion holds precisely when every vertex in $Z$ is observed, $Z$ is disjoint from $Y$ , $Z$ is disjoint from the random copies of the treatment variables, no vertex in $Z$ is a descendant of a random treatment copy, and in the graph obtained by splitting the treatment variables, $Y$ is d-separated from their random copies after conditioning on $Z$ and their fixed copies.

Definition (Lean source)

parameters

N :

Type u_1

shared

G :

shared

X :

hX_obs :

∀ D ∈ X, SWIGNode.random D ∈ G.observed

hX_fix :

∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed

Y Z :

def

backdoorCriterion G X hX_obs hX_fix Y Z :

Prop

given by

clause 1

Z ⊆ G.observed

clause 2

Disjoint Z Y

clause 3

Disjoint Z (X.image SWIGNode.random)

clause 4

z ∈ Z :

D ∈ X :

¬ G.dag.isAncestor (SWIGNode.random D) z

clause 5

(G.splitMono X hX_obs hX_fix).dag.dSep Y (X.image SWIGNode.random) (Z ∪ X.image SWIGNode.fixed)

Causalean.SWIGGraph.backdoorCriterion · Causalean/SCM/ID/BackdoorCriterion.lean:77 · uses SWIGGraph , SWIGNode

theorem backdoor_rule3_Z_marginal reviewed

Causalean.SCM

Backdoor Rule-3 leg. Fix a causal model M and a treatment set X whose random copy is observed and whose fixed copy is not already held fixed in M, and a set Z that is observed in M such that no node of Z is a descendant of any treatment random node — the non-descendant clause of the backdoor criterion. Then, at any post-intervention configuration s_post, the Z-marginal of the post-intervention observational law at s_post equals the Z-marginal of the original observational law at the pre-intervention configuration underlying s_post.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hX_obs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hX_fixed :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Z :

hZ :

Z ⊆ M.observed

h_crit_i :

∀ z ∈ Z, ∀ D ∈ X, ¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) z

s_post :

(M.fixSet X hX_obs hX_fixed).FixedValues

conclusion

((M.fixSet X hX_obs hX_fixed).obsKernel s_post).map (valuesProjection ((SCM.fixSet_observed M X hX_obs hX_fixed).symm ▸ hZ))

= (M.obsKernel (M.fixSetProj X hX_obs hX_fixed s_post)).map (valuesProjection hZ)

Proof (Lean source)

theorem backdoor_rule3_Z_marginal (M : SCM N Ω) (X : Finset N) (hX_obs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hX_fixed : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Z : Finset (SWIGNode N)) (hZ : Z ⊆ M.observed) (h_crit_i : ∀ z ∈ Z, ∀ D ∈ X, ¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) z) (s_post : (M.fixSet X hX_obs hX_fixed).FixedValues) : ((M.fixSet X hX_obs hX_fixed).obsKernel s_post).map (valuesProjection ((SCM.fixSet_observed M X hX_obs hX_fixed).symm ▸ hZ)) = (M.obsKernel (M.fixSetProj X hX_obs hX_fixed s_post)).map (valuesProjection hZ) := by -- Compose criterion (i) with A2-forward to get Rule 3's `hNoDesc`. have hNoDesc : ∀ v ∈ (∅ : Finset (SWIGNode N)) ∪ Z, ∀ d ∈ X, ¬ (M.fixSet X hX_obs hX_fixed).dag.isAncestor (SWIGNode.fixed d) v := by intro v hv d hd hanc -- A2-forward lifts `.fixed d`-ancestry in `fixSet X` to `.random d`-ancestry in `M`. have hanc_base : M.toSWIGGraph.dag.isAncestor (SWIGNode.random d) v := SCM.fixSet_isAncestor_fixed_forward M X hX_obs hX_fixed hd hanc -- Unpack `v ∈ ∅ ∪ Z = Z` and contradict criterion (i). rw [Finset.empty_union] at hv exact h_crit_i v hv d hd hanc_base -- Apply `do_rule3_star` with `Y_param := ∅`, `W_param := Z`. Rule 3*'s -- conclusion projects along `union_subset (∅.empty_subset _) hZ` -- (indexed by `∅ ∪ Z`); the goal projects along `hZ` (indexed by `Z`). have _h := SCM.do_rule3_star M X hX_obs hX_fixed (∅ : Finset (SWIGNode N)) Z (empty_subset _) hZ hNoDesc s_post -- Bridge `ValuesOn (∅ ∪ Z) ↦ ValuesOn Z` via `valuesEquivOfEq`. -- Post-composing both sides of `_h` with `valuesEquivOfEq hU` and applying -- `Measure.map_map` produces `valuesProjection` into `Z` on both sides -- (the composition reduces definitionally). have hU : (∅ : Finset (SWIGNode N)) ∪ Z = Z := Finset.empty_union _ have hmap := congrArg (fun μ : Measure (ValuesOn (∅ ∪ Z) (swigΩ Ω)) => μ.map (valuesEquivOfEq (Ω := swigΩ Ω) hU)) _h rw [MeasureTheory.Measure.map_map (valuesEquivOfEq (Ω := swigΩ Ω) hU).measurable (measurable_valuesProjection _), MeasureTheory.Measure.map_map (valuesEquivOfEq (Ω := swigΩ Ω) hU).measurable (measurable_valuesProjection _)] at hmap exact hmap

Causalean.SCM.backdoor_rule3_Z_marginal · Causalean/SCM/ID/BackdoorCriterion.lean:117 · uses isAncestor , SWIGNode , instFintype , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , valuesProjection , SCM , FixedValues , ObservedValues , fixSet , fixSetProj , fixSet_observed , obsKernel

Backdoor 6 core · 5 supporting The kernel equality proved by backdoor_completeness_ae is almost everywhere in the treatment value. ★ backdoor_completeness_ae★ backdoor_identifiable_ae

Backdoor identification, a.e. in the treatment value

The kernel equality proved by backdoor_completeness_ae is almost everywhere in the treatment value. For non-atomic (continuous) treatment, a pointwise version would read the conditional obsCondKernel on the measure-zero {X = t} slice, where Mathlib's disintegration representative is not pinned by the observational law, so such a pointwise form would be too strong.

This file states the honest, regime-uniform version: the identity holds for νX-almost-every treatment value t, where νX is the observational treatment marginal, under a standard positivity / overlap assumption P_X × P_Z ≪ P_{X,Z}. Discrete/atomic treatment is the special case where νX is atomic, so "a.e. t" is "every positive-mass treatment value".

The proof vehicle is the joint identity νX ⊗ₘ Kdo = νX ⊗ₘ Kbd, from which the a.e. statement follows by ProbabilityTheory.Kernel.ae_eq_of_compProd_eq.

Main declarations

* SCM.treatmentMarginal — observational treatment marginal νX. * SCM.BackdoorPositivityAE — product-overlap condition P_X × P_Z ≪ P_{X,Z}. * SCM.doKernelY and SCM.adjustmentKernelY — treatment-indexed do and backdoor-adjustment kernels for the outcome block. * SCM.doKernelY_disintegrate and SCM.doKernelY_marginal_const — chain-rule and Rule-3 reductions used in the proof. * SCM.backdoor_completeness_ae_compProd — primary joint-kernel completeness. * SCM.backdoor_completeness_ae — almost-every treatment-value completeness. * SCM.backdoor_identifiable_ae — cross-SCM almost-every identifiability.

def treatmentMarginal reviewed

Causalean.SCM

For a finite node population with measurable value spaces, a structural causal model, a finite treatment set, the condition that its random treatment copies are observed, and fixed-node values, the observational treatment marginal is the observational law of the random treatment coordinates at those fixed-node values.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hXr :

X.image SWIGNode.random ⊆ M.observed

s0 :

M.FixedValues

def

treatmentMarginal M X hXr s0 :

Measure (ValuesOn (X.image SWIGNode.random) (swigΩ Ω))

given by

(M.obsKernel s0).map (valuesProjection hXr)

Causalean.SCM.treatmentMarginal · Causalean/SCM/ID/Backdoor.lean:69 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues

def BackdoorPositivityAE reviewed

Causalean.SCM

For a finite node population with measurable value spaces, a structural causal model, a finite treatment set, a finite adjustment-node set, the condition that every adjustment node is observed, the condition that every random treatment copy and adjustment node is observed, and fixed-node values, the backdoor product-positivity condition states that the product of the observational treatment marginal and observational adjustment marginal is absolutely continuous with respect to the observational joint law of treatment and adjustment coordinates.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

Z :

hZ :

Z ⊆ M.observed

hXrZ :

X.image SWIGNode.random ∪ Z ⊆ M.observed

s0 :

M.FixedValues

def

BackdoorPositivityAE M X Z hZ hXrZ s0 :

Prop

given by

(((M.treatmentMarginal X (Finset.subset_union_left.trans hXrZ) s0) ⊗ₘ (const _ ((M.obsKernel s0).map (valuesProjection hZ)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M.obsKernel s0).map (valuesProjection hXrZ))

Causalean.SCM.BackdoorPositivityAE · Causalean/SCM/ID/Backdoor.lean:79 · uses SWIGNode , instDecidableEqSWIGNode , SCM , FixedValues

def doKernelY reviewed

Causalean.SCM

For a finite node population with measurable value spaces, a structural causal model, a finite treatment set, the condition that every random treatment copy is observed, the condition that no fixed treatment copy is already fixed, a finite observed outcome-node set, and fixed-node values, the treatment-indexed post-intervention outcome kernel maps each treatment value to the post-intervention observational law of the outcome coordinates.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :

hY :

Y ⊆ M.observed

s0 :

M.FixedValues

def

doKernelY M X hObs hFix Y hY s0 :

Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) (ValuesOn Y (swigΩ Ω))

given by

(((M.fixSet X hObs hFix).obsKernel.comap (M.fixSetExtend X hObs hFix s0) (M.measurable_fixSetExtend X hObs hFix s0)).map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY)))

Causalean.SCM.doKernelY · Causalean/SCM/ID/Backdoor.lean:106 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues

def adjustmentKernelY reviewed

Causalean.SCM

For a finite node population with measurable value spaces, a structural causal model, a finite treatment set, the condition that every random treatment copy is observed, the condition that no fixed treatment copy is already fixed, a finite observed outcome-node set, a finite observed adjustment-node set, and fixed-node values, the treatment-indexed backdoor-adjustment outcome kernel maps each treatment value to the backdoor-adjustment law of the outcome coordinates.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y Z :

hY :

Y ⊆ M.observed

hZ :

Z ⊆ M.observed

s0 :

M.FixedValues

def

adjustmentKernelY M X hObs hFix Y Z hY hZ s0 :

Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) (ValuesOn Y (swigΩ Ω))

given by

(M.backdoorAdjustment X hObs hFix Y Z hY hZ).comap (M.fixSetExtend X hObs hFix s0) (M.measurable_fixSetExtend X hObs hFix s0)

Causalean.SCM.adjustmentKernelY · Causalean/SCM/ID/Backdoor.lean:125 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues

theorem backdoor_completeness_ae reviewed

Causalean.SCM

Backdoor completeness, a.e. in the treatment value. For a finite node population with measurable, standard-Borel, nonempty value spaces, fix a causal model and a treatment set whose random copy is observed and whose fixed copy is not already held fixed in M, and let outcome and adjustment sets be observed, satisfying the backdoor criterion relative to (X,Y). Given a base configuration, and the product of the observational treatment and adjustment-set marginals is absolutely continuous with respect to their joint observational law, then for almost every treatment value t under the observational treatment marginal, the post-intervention outcome distribution at t equals the backdoor-adjustment functional evaluated at t.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y Z :

hY :

Y ⊆ M.observed

hZ :

Z ⊆ M.observed

h_bd :

backdoorCriterion M.toSWIGGraph X hObs hFix Y Z

s0 :

M.FixedValues

hPositivity :

M.BackdoorPositivityAE X Z hZ (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0

conclusion

∀ᵐ t ∂(M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0), M.doKernelY X hObs hFix Y hY s0 t

= M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t

Proof (Lean source)

theorem backdoor_completeness_ae (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (h_bd : backdoorCriterion M.toSWIGGraph X hObs hFix Y Z) (s0 : M.FixedValues) (hPositivity : M.BackdoorPositivityAE X Z hZ (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0) : ∀ᵐ t ∂(M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0), M.doKernelY X hObs hFix Y hY s0 t = M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t := by have hXrZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := union_subset (Finset.image_subset_iff.mpr hObs) hZ have hXr : X.image SWIGNode.random ⊆ M.observed := Finset.subset_union_left.trans hXrZ haveI : IsFiniteMeasure (M.treatmentMarginal X hXr s0) := by unfold treatmentMarginal exact (M.obsKernel s0).isFiniteMeasure_map _ exact ProbabilityTheory.Kernel.ae_eq_of_compProd_eq (M.backdoor_completeness_ae_compProd X hObs hFix Y Z hY hZ h_bd s0 hPositivity)

Causalean.SCM.backdoor_completeness_ae · Causalean/SCM/ID/Backdoor.lean:392 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , BackdoorPositivityAE , FixedValues , adjustmentKernelY , doKernelY , treatmentMarginal , backdoorCriterion

theorem backdoor_identifiable_ae reviewed

Causalean.SCM

Backdoor identifiability, a.e. in the treatment value (cross-SCM corollary). For a finite node population with measurable, standard-Borel, nonempty value spaces, fix two causal models that share the same SWIG graph and the same observational kernel, with base configurations that agree under this shared identification. Fix a treatment set valid in both models and outcome/adjustment sets that are observed in both models, such that Z satisfies the backdoor criterion for (X,Y) in each model separately, at base configurations, with product positivity of the observational treatment and adjustment-set marginals holding in each model. Then for almost every treatment value t under the shared observational treatment marginal, the post-intervention outcome distribution computed in M₁ at t equals the one computed in M₂ at t, since each model individually satisfies backdoor completeness and the two share the same graph and observational kernel.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

M₁ M₂ :

SCM N Ω

h_swig :

M₁.toSWIGGraph = M₂.toSWIGGraph

X :

Y Z :

hObs₁ :

∀ D ∈ X, SWIGNode.random D ∈ M₁.observed

hFix₁ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed

hObs₂ :

∀ D ∈ X, SWIGNode.random D ∈ M₂.observed

hFix₂ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed

hY₁ :

Y ⊆ M₁.observed

hZ₁ :

Z ⊆ M₁.observed

hY₂ :

Y ⊆ M₂.observed

hZ₂ :

Z ⊆ M₂.observed

h_bd₁ :

backdoorCriterion M₁.toSWIGGraph X hObs₁ hFix₁ Y Z

h_bd₂ :

backdoorCriterion M₂.toSWIGGraph X hObs₂ hFix₂ Y Z

s0₁ :

M₁.FixedValues

s0₂ :

M₂.FixedValues

hPositivity₁ :

M₁.BackdoorPositivityAE X Z hZ₁ (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s0₁

hPositivity₂ :

M₂.BackdoorPositivityAE X Z hZ₂ (union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s0₂

h_obs :

HEq M₁.obsKernel M₂.obsKernel

h_s0 :

HEq s0₁ s0₂

conclusion

(M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁)

=ᵐ[M₁.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁)) s0₁] (M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂)

Proof (Lean source)

theorem backdoor_identifiable_ae (M₁ M₂ : SCM N Ω) (h_swig : M₁.toSWIGGraph = M₂.toSWIGGraph) (X : Finset N) (Y Z : Finset (SWIGNode N)) (hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed) (hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed) (hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed) (hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed) (hY₁ : Y ⊆ M₁.observed) (hZ₁ : Z ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (hZ₂ : Z ⊆ M₂.observed) (h_bd₁ : backdoorCriterion M₁.toSWIGGraph X hObs₁ hFix₁ Y Z) (h_bd₂ : backdoorCriterion M₂.toSWIGGraph X hObs₂ hFix₂ Y Z) (s0₁ : M₁.FixedValues) (s0₂ : M₂.FixedValues) (hPositivity₁ : M₁.BackdoorPositivityAE X Z hZ₁ (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s0₁) (hPositivity₂ : M₂.BackdoorPositivityAE X Z hZ₂ (union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s0₂) (h_obs : HEq M₁.obsKernel M₂.obsKernel) (h_s0 : HEq s0₁ s0₂) : (M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁) =ᵐ[M₁.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁)) s0₁] (M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂) := by -- Destructure both SCMs and `cases h_swig` to align the SWIGGraph-derived -- type indices (FixedValues, observed, fixSet, treatmentMarginal); then the -- base points `s0₁ s0₂` and obsKernels coincide. obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases h_swig -- After `cases h_swig` the SWIGGraph fields agree definitionally, so the two -- `FixedValues` types coincide and `h_s0` is an equality of base points. -- The two SCMs still differ in their non-SWIGGraph fields, so we keep them as -- distinct structure literals and use `h_obs` as a rewrite (obsKernel is a -- *derived* def, not a structure field, hence not `cases`-able). cases h_s0 have hXr₁ : X.image SWIGNode.random ⊆ observed₁ := Finset.image_subset_iff.mpr hObs₁ have hXr₂ : X.image SWIGNode.random ⊆ observed₁ := Finset.image_subset_iff.mpr hObs₂ -- Step 1: do-side ≡ adjustment-side on each SCM, a.e. have hc1 := backdoor_completeness_ae ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ X hObs₁ hFix₁ Y Z hY₁ hZ₁ h_bd₁ s0₁ hPositivity₁ have hc2 := backdoor_completeness_ae ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ X hObs₂ hFix₂ Y Z hY₂ hZ₂ h_bd₂ s0₁ hPositivity₂ -- Step 2: cross-SCM invariance of the adjustment kernel. have hinv : (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ : SCM N Ω).adjustmentKernelY X hObs₁ hFix₁ Y Z hY₁ hZ₁ s0₁ = (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ : SCM N Ω).adjustmentKernelY X hObs₂ hFix₂ Y Z hY₂ hZ₂ s0₁ := by rw [adjustmentKernelY, adjustmentKernelY] have hbd := backdoorAdjustment_invariant (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ : SCM N Ω) (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ : SCM N Ω) rfl h_obs X hObs₁ hFix₁ hObs₂ hFix₂ Y Z hY₁ hZ₁ hY₂ hZ₂ rw [eq_of_heq hbd] rfl -- Step 3: the treatment marginals coincide (same obsKernel, same base, same -- projection index). have hνX : (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ : SCM N Ω).treatmentMarginal X hXr₁ s0₁ = (⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ : SCM N Ω).treatmentMarginal X hXr₂ s0₁ := by rw [treatmentMarginal, treatmentMarginal, eq_of_heq h_obs] -- Assemble: doKernelY M₁ ≡ adjY M₁ = adjY M₂ ≡ doKernelY M₂. refine Filter.EventuallyEq.trans hc1 ?_ rw [hinv, hνX] exact Filter.EventuallyEq.symm hc2

Causalean.SCM.backdoor_identifiable_ae · Causalean/SCM/ID/Backdoor.lean:431 · uses SWIGGraph , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , BackdoorPositivityAE , FixedValues , ObservedValues , doKernelY , obsKernel , treatmentMarginal , backdoorCriterion

5 supporting declarations (lemmas, instances)

instIsFiniteKernelDoKernelY instance — For a finite, distinguishable node population with measurable node-value spaces and a structural causal model, a finite treatment set, the requirement that every corresponding random treatment node is observed, the requirement that no corresponding fixed treatment node is already fixed, a finite observed outcome-node set, and a fixed-node assignment, the treatment-indexed post-intervention outcome kernel is finite.

parameters

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

s0 :

M.FixedValues

instance

instIsFiniteKernelDoKernelY M X hObs hFix Y hY s0 :
IsFiniteKernel (M.doKernelY X hObs hFix Y hY s0)

given by

by rw [SCM.doKernelY]; infer_instance

Causalean.SCM.instIsFiniteKernelDoKernelY · Causalean/SCM/ID/Backdoor.lean:141
instIsFiniteKernelAdjustmentKernelY instance — For a finite, distinguishable node population with measurable, standard-Borel, nonempty node-value spaces and a structural causal model, a finite treatment set, the requirement that every corresponding random treatment node is observed, the requirement that no corresponding fixed treatment node is already fixed, finite observed outcome and adjustment-node sets, and a fixed-node assignment, the treatment-indexed backdoor-adjustment outcome kernel is finite.

parameters

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y Z :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

hZ :

Z ⊆ M.observed

s0 :

M.FixedValues

instance

instIsFiniteKernelAdjustmentKernelY M X hObs hFix Y Z hY hZ s0 :
IsFiniteKernel (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0)

given by

by rw [SCM.adjustmentKernelY]; infer_instance

Causalean.SCM.instIsFiniteKernelAdjustmentKernelY · Causalean/SCM/ID/Backdoor.lean:151
doKernelY_disintegrate theorem — Treatment-indexed chain rule. At treatment value t, the post-do(X) Y-marginal kernel disintegrates through Z: it is the conditional Y ∣ Z (under do(X)) composed with the post-do(X) Z-marginal kernel. The doKernelY-level form of obsKernel_map_eq_obsCondKernel_comp.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y Z :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

hZ :

Z ⊆ M.observed

s0 :

M.FixedValues

t :

ValuesOn (X.image SWIGNode.random) (swigΩ Ω)

conclusion

M.doKernelY X hObs hFix Y hY s0 t
= ((M.fixSet X hObs hFix).obsCondKernel Y Z ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY) ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)).sectR (M.fixSetExtend X hObs hFix s0 t) ∘ₘ M.doKernelY X hObs hFix Z hZ s0 t

Proof (Lean source)

theorem doKernelY_disintegrate (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) : M.doKernelY X hObs hFix Y hY s0 t = ((M.fixSet X hObs hFix).obsCondKernel Y Z ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY) ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)).sectR (M.fixSetExtend X hObs hFix s0 t) ∘ₘ M.doKernelY X hObs hFix Z hZ s0 t := by have hY' : M.doKernelY X hObs hFix Y hY s0 t = ((M.fixSet X hObs hFix).obsKernel (M.fixSetExtend X hObs hFix s0 t)).map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY)) := by rw [SCM.doKernelY, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply] have hZ' : M.doKernelY X hObs hFix Z hZ s0 t = ((M.fixSet X hObs hFix).obsKernel (M.fixSetExtend X hObs hFix s0 t)).map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)) := by rw [SCM.doKernelY, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply] rw [hY', hZ'] exact SCM.obsKernel_map_eq_obsCondKernel_comp (M.fixSet X hObs hFix) Y Z _ _ _

Causalean.SCM.doKernelY_disintegrate · Causalean/SCM/ID/Backdoor.lean:170
doKernelY_marginal_const theorem — Treatment-indexed Rule 3 (marginal invariance). If no X-copy is an ancestor of any Z-node, the post-do(X) Z-marginal kernel is constant in the treatment value and equals the observational Z-marginal at base s₀. The doKernelY-level form of backdoor_rule3_Z_marginal.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Z :

Finset (SWIGNode N)

hZ :

Z ⊆ M.observed

h_noanc :

∀ z ∈ Z, ∀ D ∈ X, ¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) z

s0 :

M.FixedValues

t :

ValuesOn (X.image SWIGNode.random) (swigΩ Ω)

conclusion

M.doKernelY X hObs hFix Z hZ s0 t = (M.obsKernel s0).map (valuesProjection hZ)

Proof (Lean source)

theorem doKernelY_marginal_const (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Z : Finset (SWIGNode N)) (hZ : Z ⊆ M.observed) (h_noanc : ∀ z ∈ Z, ∀ D ∈ X, ¬ M.toSWIGGraph.dag.isAncestor (SWIGNode.random D) z) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) : M.doKernelY X hObs hFix Z hZ s0 t = (M.obsKernel s0).map (valuesProjection hZ) := by have hZ' : M.doKernelY X hObs hFix Z hZ s0 t = ((M.fixSet X hObs hFix).obsKernel (M.fixSetExtend X hObs hFix s0 t)).map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hZ)) := by rw [SCM.doKernelY, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply] rw [hZ'] have hR3 := SCM.backdoor_rule3_Z_marginal M X hObs hFix Z hZ h_noanc (M.fixSetExtend X hObs hFix s0 t) rw [SCM.fixSetProj_fixSetExtend] at hR3 exact hR3

Causalean.SCM.doKernelY_marginal_const · Causalean/SCM/ID/Backdoor.lean:198
backdoor_completeness_ae_compProd theorem — For a finite node population with measurable, standard-Borel, nonempty value spaces, a structural causal model, a treatment set whose random copies are observed and whose fixed copies are not already fixed, observed outcome and adjustment sets, a backdoor criterion, including its disjointness conditions, a fixed-node assignment, and product positivity, the treatment-marginal joint laws of the interventional and adjustment kernels are equal. Joint (compProd) completeness — primary form. νX ⊗ₘ doKernelY = νX ⊗ₘ adjustmentKernelY at base s₀. This is the object that is well-posed for continuous treatment: it never reads obsCondKernel on a μXZ-null treatment slice.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y Z :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

hZ :

Z ⊆ M.observed

h_bd :

backdoorCriterion M.toSWIGGraph X hObs hFix Y Z

s0 :

M.FixedValues

_hPositivity :

M.BackdoorPositivityAE X Z hZ (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0

conclusion

(M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0)
= (M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0)

Proof (Lean source)

theorem backdoor_completeness_ae_compProd (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y Z : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (h_bd : backdoorCriterion M.toSWIGGraph X hObs hFix Y Z) (s0 : M.FixedValues) (_hPositivity : M.BackdoorPositivityAE X Z hZ (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s0) : (M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0) = (M.treatmentMarginal X (Finset.subset_union_left.trans (union_subset (Finset.image_subset_iff.mpr hObs) hZ)) s0) ⊗ₘ (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0) := by have hXrZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := union_subset (Finset.image_subset_iff.mpr hObs) hZ have hXr : X.image SWIGNode.random ⊆ M.observed := Finset.subset_union_left.trans hXrZ -- Abbreviations. set sT := fun t => M.fixSetExtend X hObs hFix s0 t with hsT set hZ_post : Z ⊆ (M.fixSet X hObs hFix).observed := (SCM.fixSet_observed M X hObs hFix).symm ▸ hZ with hZpost_def set hY_post : Y ⊆ (M.fixSet X hObs hFix).observed := (SCM.fixSet_observed M X hObs hFix).symm ▸ hY with hYpost_def -- μZ = (M.obsKernel s0).map projZ, the observational Z-marginal at base s0. set μZ := (M.obsKernel s0).map (valuesProjection hZ) with hμZ -- ============================================================ -- Reduction 1 (chain rule + Rule 3): the do-side Y-marginal kernel at t. -- doKernelY t = (sectR (fixSet X).obsCondKernel (sT t)) ∘ₘ μZ -- ============================================================ -- Reduction 1 (chain rule + Rule 3) is now packaged in the treatment-indexed -- do-calculus lemmas `doKernelY_disintegrate` and `doKernelY_marginal_const`. have hLHS : ∀ t, M.doKernelY X hObs hFix Y hY s0 t = ((M.fixSet X hObs hFix).obsCondKernel Y Z hY_post hZ_post).sectR (sT t) ∘ₘ μZ := by intro t rw [doKernelY_disintegrate M X hObs hFix Y Z hY hZ s0 t, doKernelY_marginal_const M X hObs hFix Z hZ h_bd.2.2.2.1 s0 t] -- ============================================================ -- Reduction 2 (unfold backdoorAdjustment): the adjustment-side kernel at t. -- adjustmentKernelY t = (sectR condPost (sT t)) ∘ₘ μZ -- where condPost z = M.obsCondKernel Y (Xr∪Z) (s0, fillZrW (sT t) z). -- ============================================================ -- The `condPost` kernel appearing in `backdoorAdjustment`. set hXZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := hXrZ with hXZ_def set condPost : Kernel ((M.fixSet X hObs hFix).FixedValues × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := (M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) hY hXZ).comap (fun p : (M.fixSet X hObs hFix).FixedValues × ValuesOn Z (swigΩ Ω) => (M.fixSetProj X hObs hFix p.1, M.fillZrW X hObs hFix Z p.1 p.2)) (prodMk ((M.measurable_fixSetProj X hObs hFix).comp measurable_fst) (M.measurable_fillZrW_prod X hObs hFix Z)) with hcondPost_def haveI : IsMarkovKernel (M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) hY hXZ) := by unfold SCM.obsCondKernel; infer_instance haveI : IsMarkovKernel condPost := by rw [hcondPost_def]; infer_instance have hRHS : ∀ t, M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t = condPost.sectR (sT t) ∘ₘ μZ := by intro t -- adjustmentKernelY t = backdoorAdjustment (sT t). have hadj : M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t = M.backdoorAdjustment X hObs hFix Y Z hY hZ (sT t) := by rw [SCM.adjustmentKernelY, ProbabilityTheory.Kernel.comap_apply] rw [hadj] -- Unfold backdoorAdjustment body to ((zMarginalPost ⊗ₖ condPost).map snd) (sT t). change ((((M.obsKernel.map (valuesProjection hZ)).comap (M.fixSetProj X hObs hFix) (M.measurable_fixSetProj X hObs hFix)) ⊗ₖ condPost).map snd) (sT t) = condPost.sectR (sT t) ∘ₘ μZ rw [compProd_map_snd_apply, ProbabilityTheory.Kernel.comap_apply, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), SCM.fixSetProj_fixSetExtend, ← hμZ] -- ============================================================ -- a.e. Rule 2 on the product νX ⊗ₘ const μZ. -- ============================================================ -- νX = treatmentMarginal = (M.obsKernel s0).map projXr. set νX := M.treatmentMarginal X hXr s0 with hνX have hνX_eq : νX = (M.obsKernel s0).map (valuesProjection hXr) := by rw [hνX, SCM.treatmentMarginal] -- The product measure λ = νX ⊗ₘ const μZ. set lam := νX ⊗ₘ const _ μZ with hlam -- Finiteness instances. haveI : IsFiniteMeasure νX := by rw [hνX_eq]; exact (M.obsKernel s0).isFiniteMeasure_map _ haveI : IsFiniteMeasure μZ := by rw [hμZ]; exact (M.obsKernel s0).isFiniteMeasure_map _ -- Apply the a.e. Rule 2 with Z := X, W := Z. have hPos_ae : (((M.obsKernel s0).map (valuesProjection hXr) ⊗ₘ const _ ((M.obsKernel s0).map (valuesProjection hZ))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M.obsKernel s0).map (valuesProjection hXrZ)) := _hPositivity -- Rule 2 straight from the backdoor criterion: the applicator derives the -- d-separation + non-descendance premises internally. have hR2 := SCM.do_rule2_kernel_of_nondescendant_product_ae M X hObs hFix Y Z hY hZ hXr hXrZ (backdoorCriterion_dSep_fixSet M X hObs hFix Y Z hY hXr h_bd) (backdoorCriterion_W_nonDesc M X hObs hFix Y Z h_bd) (backdoorCriterion_W_nonDescM1 M X hObs hFix Y Z h_bd) s0 hPos_ae haveI hdoKfin : IsFiniteKernel (M.doKernelY X hObs hFix Y hY s0) := by rw [SCM.doKernelY]; infer_instance haveI hadjSF : IsSFiniteKernel (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0) := by rw [SCM.adjustmentKernelY, SCM.backdoorAdjustment]; infer_instance set liftTZ : ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω) → (M.fixSet X hObs hFix).FixedValues × ValuesOn Z (swigΩ Ω) := fun p => (sT p.1, p.2) with hliftTZ_def have hliftTZ_meas : Measurable liftTZ := by rw [hliftTZ_def, hsT] exact prodMk ((M.measurable_fixSetExtend X hObs hFix s0).comp measurable_fst) measurable_snd set fL : Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := ((M.fixSet X hObs hFix).obsCondKernel Y Z hY_post hZ_post).comap liftTZ hliftTZ_meas with hfL_def set fR : Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := condPost.comap liftTZ hliftTZ_meas with hfR_def have hL : ∀ t, M.doKernelY X hObs hFix Y hY s0 t = (fL.sectR t) ∘ₘ μZ := by intro t exact hLHS t have hR : ∀ t, M.adjustmentKernelY X hObs hFix Y Z hY hZ s0 t = (fR.sectR t) ∘ₘ μZ := by intro t exact hRHS t have hae : ∀ᵐ p ∂(νX ⊗ₘ const (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) μZ), fL p = fR p := by rw [hνX_eq, hμZ] filter_upwards [hR2] with p hp simpa [hfL_def, hfR_def, hliftTZ_def, hcondPost_def, hsT, ProbabilityTheory.Kernel.comap_apply, SCM.fixSetProj_fixSetExtend, SCM.fillZrW_fixSetExtend] using hp exact compProd_eq_of_inner_ae νX μZ (M.doKernelY X hObs hFix Y hY s0) (M.adjustmentKernelY X hObs hFix Y Z hY hZ s0) fL fR hL hR hae

Causalean.SCM.backdoor_completeness_ae_compProd · Causalean/SCM/ID/Backdoor.lean:225

Query 8 core · 1 supporting This file contains the lightweight query-level API shared by ID soundness theorems. ★ interventionalQuery_eq_doKernelY_of_valid★ interventionalQueryValid_iff_of_toSWIGGraph_eq

Total interventional query API

This file contains the lightweight query-level API shared by ID soundness theorems. It deliberately avoids importing the Tian/c-factor ID skeleton, so modules can state and prove base cases for interventionalQuery without depending on the full density recovery stack.

def swigValueNonempty reviewed

Causalean.SCM.ID

For a population of variables with nonempty value spaces and a SWIG node, a witness that that node's value space is nonempty is provided.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

w :

SWIGNode N

def

swigValueNonempty w :

Nonempty (swigΩ Ω w)

given by

by cases w <;> infer_instance

Causalean.SCM.ID.swigValueNonempty · Causalean/SCM/ID/Query.lean:33 · uses SWIGNode , swigΩ

def valuesOnNonempty reviewed

Causalean.SCM.ID

For a population of variables with nonempty value spaces and a finite SWIG-node set, a witness that the corresponding joint value space is nonempty is provided.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

Y :

def

valuesOnNonempty Y :

Nonempty (ValuesOn Y (swigΩ Ω))

given by

⟨fun y => choice (swigValueNonempty (Ω := Ω) y.val)⟩

Causalean.SCM.ID.valuesOnNonempty · Causalean/SCM/ID/Query.lean:42 · uses SWIGNode , swigΩ , ValuesOn

def defaultInterventionalKernel reviewed

Causalean.SCM.ID

For a population of variables with nonempty measurable value spaces, an intervention set, and an outcome-node set, the default interventional kernel is the constant kernel concentrated at an arbitrary outcome assignment.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

X :

Y :

def

defaultInterventionalKernel X Y :

Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) (ValuesOn Y (swigΩ Ω))

given by

by classical letI : Nonempty (ValuesOn Y (swigΩ Ω)) := valuesOnNonempty (Ω := Ω) Y exact const _ (dirac (choice inferInstance))

Causalean.SCM.ID.defaultInterventionalKernel · Causalean/SCM/ID/Query.lean:53 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn

def standardFixedValues reviewed

Causalean.SCM.ID

For a finite population of variables with measurable value spaces, a structural causal model that is standard, the canonical fixed-value assignment is the unique assignment on its empty fixed-node set.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

hM :

M.isStandard

def

standardFixedValues M hM :

M.FixedValues

given by

fun d

=> False.elim (by have hempty : M.fixed = ∅ := hM have hd : d.val ∈ (∅ : Finset (SWIGNode N)) := by simpa [hempty] using d.property exact notMem_empty d.val hd)

Causalean.SCM.ID.standardFixedValues · Causalean/SCM/ID/Query.lean:71 · uses SCM , FixedValues , isStandard

def interventionalQueryValid reviewed

Causalean.SCM.ID

For a finite population of variables with measurable value spaces, an intervention set, an outcome-node set, and a structural causal model, interventional-query validity holds exactly when all intervention random nodes are observed, their fixed nodes are absent, all outcomes are observed, and the model is standard.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

X :

Y :

M :

SCM N Ω

def

interventionalQueryValid X Y M :

Prop

given by

clause 1

D ∈ X :

SWIGNode.random D ∈ M.observed

clause 2

D ∈ X :

SWIGNode.fixed D ∉ M.fixed

clause 3

Y ⊆ M.observed

clause 4

M.isStandard

Causalean.SCM.ID.interventionalQueryValid · Causalean/SCM/ID/Query.lean:87 · uses SWIGNode , SCM

def interventionalQuery reviewed

Causalean.SCM.ID

For a finite population of variables with nonempty measurable value spaces, an intervention set, and an outcome-node set, the interventional query maps each structural causal model to its post-intervention outcome kernel at a chosen default assignment of the model's fixed values when the query is valid, and otherwise to the default constant kernel.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

X :

Y :

def

interventionalQuery X Y :

CausalQuery N Ω (Kernel (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)))

given by

by classical exact fun M => if h : (∀ D ∈ X, SWIGNode.random D ∈ M.observed) ∧

(∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) ∧

(Y ⊆ M.observed) ∧

M.isStandard then M.doKernelY X h.1 h.2.1 Y h.2.2.1 (standardFixedValues M h.2.2.2) else defaultInterventionalKernel X Y

Causalean.SCM.ID.interventionalQuery · Causalean/SCM/ID/Query.lean:102 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , CausalQuery

lemma interventionalQuery_eq_doKernelY_of_valid reviewed

Causalean.SCM.ID

For treatment nodes X and outcome nodes Y satisfying the well-formedness conditions for a valid interventional query in a model M, the total interventional query evaluated at M equals the post-intervention outcome-marginal kernel doKernelY at the chosen default fixed-value assignment.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

X :

Y :

M :

SCM N Ω

h :

interventionalQueryValid X Y M

conclusion

interventionalQuery (Ω := Ω) X Y M

= M.doKernelY X h.1 h.2.1 Y h.2.2.1 (standardFixedValues M h.2.2.2)

Proof (Lean source)

lemma interventionalQuery_eq_doKernelY_of_valid [∀ n, Nonempty (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (M : SCM N Ω) (h : interventionalQueryValid X Y M) : interventionalQuery (Ω := Ω) X Y M = M.doKernelY X h.1 h.2.1 Y h.2.2.1 (standardFixedValues M h.2.2.2) := by classical rw [interventionalQuery] exact dif_pos (by simpa [interventionalQueryValid] using h)

Causalean.SCM.ID.interventionalQuery_eq_doKernelY_of_valid · Causalean/SCM/ID/Query.lean:129 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , interventionalQuery , interventionalQueryValid , standardFixedValues , doKernelY , isStandard

theorem interventionalQueryValid_iff_of_toSWIGGraph_eq reviewed

Causalean.SCM.ID

Well-formedness invariance under matching SWIG graphs. For an intervention target set X and outcome set Y, if two structural causal models M₁, M₂ have the same SWIG graph, then they agree on whether the total interventional query for X, Y is well formed.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

X :

Y :

M₁ M₂ :

SCM N Ω

hsg :

M₁.toSWIGGraph = M₂.toSWIGGraph

conclusion

interventionalQueryValid X Y M₁ ↔ interventionalQueryValid X Y M₂

Proof (Lean source)

theorem interventionalQueryValid_iff_of_toSWIGGraph_eq (X : Finset N) (Y : Finset (SWIGNode N)) (M₁ M₂ : SCM N Ω) (hsg : M₁.toSWIGGraph = M₂.toSWIGGraph) : interventionalQueryValid X Y M₁ ↔ interventionalQueryValid X Y M₂ := by have ho : M₁.observed = M₂.observed := congrArg SWIGGraph.observed hsg have hf : M₁.fixed = M₂.fixed := congrArg SWIGGraph.fixed hsg unfold interventionalQueryValid isStandard rw [ho, hf, hsg]

Causalean.SCM.ID.interventionalQueryValid_iff_of_toSWIGGraph_eq · Causalean/SCM/ID/Query.lean:154 · uses SWIGGraph , SWIGNode , SCM , interventionalQueryValid

1 supporting declaration (lemmas, instances)

interventionalQuery_eq_default_of_not_valid lemma — Outside the well-formed branch, the total interventional query is the fixed fallback kernel.

hypotheses

N :

Type u_1
N → Type u_2
shared

∀ n, Nonempty (Ω n)

X :

Finset N

Y :

Finset (SWIGNode N)

M :

SCM N Ω

h :

¬ interventionalQueryValid X Y M

conclusion

interventionalQuery (Ω := Ω) X Y M = defaultInterventionalKernel (Ω := Ω) X Y

Proof (Lean source)

lemma interventionalQuery_eq_default_of_not_valid [∀ n, Nonempty (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (M : SCM N Ω) (h : ¬ interventionalQueryValid X Y M) : interventionalQuery (Ω := Ω) X Y M = defaultInterventionalKernel (Ω := Ω) X Y := by classical rw [interventionalQuery] exact dif_neg (by simpa [interventionalQueryValid] using h)

Causalean.SCM.ID.interventionalQuery_eq_default_of_not_valid · Causalean/SCM/ID/Query.lean:143

DoLawTransport 2 core · 0 supporting The post-intervention Y-marginal kernel doKernelY is built from the do-observational law (M.fixSet X).obsKernel by a comap (extend the fixed slice by the treatment value) followed by a map (project to the outcomes Y): do ★ doKernelY_eq_of_doObsKernel_heq

Structural transport of the do-observational law to `doKernelY`

The post-intervention Y-marginal kernel doKernelY is built from the do-observational law (M.fixSet X).obsKernel by a comap (extend the fixed slice by the treatment value) followed by a map (project to the outcomes Y):

doKernelY M X … Y … s₀ = ((M.fixSet X).obsKernel.comap (fixSetExtend s₀)).map π_Y.

The comap/map data (fixSetExtend, the Y-projection) and the intermediate value-space types depend on M only through its SWIG graph (observed, fixed, which fixSet preserves/enlarges structurally) and the base slice s₀. Therefore two models sharing a SWIG graph whose do-observational laws agree produce the same doKernelY.

This isolates the genuine identification content — that the do-observational laws agree — from the purely structural transport performed here. The identification content is discharged elsewhere (the Tian g-formula in GraphicalThms/DoGFormula and its recursive/discrete soundness layers); this file is graph/measure bookkeeping only and makes no appeal to idSucceeds or any reference measure.

def doObsKernelYMarginal reviewed

Causalean.SCM.ID

For a finite population of variables with measurable value spaces, a structural causal model, an intervention set whose random nodes are observed and whose fixed nodes are not already fixed, an outcome-node set contained in the observed nodes, the do-observational outcome marginal kernel maps fixed intervention values to the induced distribution of those outcomes.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :

hY :

Y ⊆ M.observed

def

doObsKernelYMarginal M X hObs hFix Y hY :

Kernel (M.fixSet X hObs hFix).FixedValues (ValuesOn Y (swigΩ Ω))

given by

(M.fixSet X hObs hFix).obsKernel.map (valuesProjection ((SCM.fixSet_observed M X hObs hFix).symm ▸ hY))

Causalean.SCM.ID.doObsKernelYMarginal · Causalean/SCM/ID/DoLawTransport.lean:46 · uses SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , fixSet

theorem doKernelY_eq_of_doObsKernel_heq reviewed

Causalean.SCM.ID

Structural transport. Fix two causal models that share the same underlying SWIG graph, together with a treatment set X that is a valid intervention in the first model — every node of X is observed and not already fixed there and likewise valid in the second model, and an outcome set Y that is observed in the first model and observed in the second. If the two models' base fixed-value slices coincide and their Y-marginals of the do-observational law agree, up to the type-level identification the shared graph provides, then the resulting post-intervention Y-marginal kernels doKernelY agree at that shared base slice.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

X :

Y :

M₁ M₂ :

SCM N Ω

hsg :

M₁.toSWIGGraph = M₂.toSWIGGraph

hObs₁ :

∀ D ∈ X, SWIGNode.random D ∈ M₁.observed

hFix₁ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed

hObs₂ :

∀ D ∈ X, SWIGNode.random D ∈ M₂.observed

hFix₂ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed

hY₁ :

Y ⊆ M₁.observed

hY₂ :

Y ⊆ M₂.observed

s0₁ :

M₁.FixedValues

s0₂ :

M₂.FixedValues

hs0 :

HEq s0₁ s0₂

hdoobsY :

HEq (doObsKernelYMarginal M₁ X hObs₁ hFix₁ Y hY₁) (doObsKernelYMarginal M₂ X hObs₂ hFix₂ Y hY₂)

conclusion

M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁ = M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂

Proof (Lean source)

theorem doKernelY_eq_of_doObsKernel_heq (X : Finset N) (Y : Finset (SWIGNode N)) (M₁ M₂ : SCM N Ω) (hsg : M₁.toSWIGGraph = M₂.toSWIGGraph) (hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed) (hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed) (hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed) (hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed) (hY₁ : Y ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (s0₁ : M₁.FixedValues) (s0₂ : M₂.FixedValues) (hs0 : HEq s0₁ s0₂) (hdoobsY : HEq (doObsKernelYMarginal M₁ X hObs₁ hFix₁ Y hY₁) (doObsKernelYMarginal M₂ X hObs₂ hFix₂ Y hY₂)) : M₁.doKernelY X hObs₁ hFix₁ Y hY₁ s0₁ = M₂.doKernelY X hObs₂ hFix₂ Y hY₂ s0₂ := by obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases hsg have hs0_eq : s0₁ = s0₂ := eq_of_heq hs0 subst hs0_eq have hmapY_eq : _ = _ := eq_of_heq hdoobsY unfold SCM.doKernelY doObsKernelYMarginal at * ext t A hA -- Peel `map`/`comap` to the fibre, then fold the fibre back into `obsKernel.map π_Y` -- so the marginal hypothesis `hmapY_eq` rewrites both sides to the same kernel. rw [ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply, ← ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ← ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), hmapY_eq] -- Both sides are now the same `Y`-marginal kernel; the residual fibre arguments -- differ only in proof-irrelevant SWIG-graph proof fields. congr 1

Causalean.SCM.ID.doKernelY_eq_of_doObsKernel_heq · Causalean/SCM/ID/DoLawTransport.lean:70 · uses SWIGGraph , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , doObsKernelYMarginal , doKernelY , fixSet

Adjustment 4 core · 3 supporting This file defines graph-level adjustment functionals for backdoor and frontdoor identification. ★ backdoorAdjustment_invariant★ frontdoorAdjustment_invariant

Adjustment Functionals

This file defines graph-level adjustment functionals for backdoor and frontdoor identification. These functionals express post-intervention outcome distributions in terms of observational kernels, enabling single-model completeness arguments to be combined with cross-model invariance statements. It also proves finite-kernel instances and cross-SCM invariance for both adjustment functionals.

def backdoorAdjustment reviewed

Causalean.SCM

For a finite node set with measurable node-value spaces in which every random or fixed node value space is standard Borel and nonempty, a structural causal model, a treatment node set whose random copies are observed, whose fixed copies are not already fixed in the model, and outcome and adjustment SWIG-node sets, each contained in the observed-node set, the backdoor adjustment functional is the kernel from post-intervention fixed-node assignments to distributions of the outcome-node assignment. It first forms the observational marginal distribution of the adjustment nodes, then that marginal indexed by the post-intervention fixed-node assignment, and then the conditional outcome distribution given the treatment and adjustment-node assignments.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hX_obs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hX_fixed :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y Z :

_hY :

Y ⊆ M.observed

_hZ :

Z ⊆ M.observed

def

backdoorAdjustment M X hX_obs hX_fixed Y Z _hY _hZ :

Kernel (M.fixSet X hX_obs hX_fixed).FixedValues (ValuesOn Y (swigΩ Ω))

given by

by have hXZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := by refine union_subset ?_ _hZ intro v hv rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩ exact hX_obs D hD let zMarginal : Kernel M.FixedValues (ValuesOn Z (swigΩ Ω)) := (M.obsKernel).map (valuesProjection _hZ) let zMarginalPost : Kernel (M.fixSet X hX_obs hX_fixed).FixedValues (ValuesOn Z (swigΩ Ω)) := zMarginal.comap (M.fixSetProj X hX_obs hX_fixed) (M.measurable_fixSetProj X hX_obs hX_fixed) let condPost : Kernel ((M.fixSet X hX_obs hX_fixed).FixedValues × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := (M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) _hY hXZ).comap (fun p => (M.fixSetProj X hX_obs hX_fixed p.1, M.fillZrW X hX_obs hX_fixed Z p.1 p.2)) (prodMk ((M.measurable_fixSetProj X hX_obs hX_fixed).comp measurable_fst) (M.measurable_fillZrW_prod X hX_obs hX_fixed Z)) exact ((zMarginalPost ⊗ₖ condPost).map snd)

Causalean.SCM.backdoorAdjustment · Causalean/SCM/ID/Adjustment.lean:49 · uses SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , fixSet

def frontdoorAdjustment reviewed

Causalean.SCM

For a finite node set with measurable node-value spaces in which every random or fixed node value space is standard Borel and nonempty, a structural causal model, a treatment node set whose random copies are observed, whose fixed copies are not already fixed in the model, and outcome and mediator SWIG-node sets, each contained in the observed-node set, the frontdoor adjustment functional is the kernel from post-intervention fixed-node assignments to distributions of the outcome-node assignment. It first forms the intervention treatment assignment, the mediator law conditional on that assignment, the observational treatment marginal, the conditional outcome law given observational treatment and mediator assignments, and the outcome law obtained by averaging over observational treatment.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M :

SCM N Ω

X :

hX_obs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hX_fixed :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y Z :

_hY :

Y ⊆ M.observed

_hZ :

Z ⊆ M.observed

def

frontdoorAdjustment M X hX_obs hX_fixed Y Z _hY _hZ :

Kernel (M.fixSet X hX_obs hX_fixed).FixedValues (ValuesOn Y (swigΩ Ω))

given by

by have hXr : X.image SWIGNode.random ⊆ M.observed := by intro v hv rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩ exact hX_obs D hD have hXZ : X.image SWIGNode.random ∪ Z ⊆ M.observed := Finset.union_subset hXr _hZ let xDo : (M.fixSet X hX_obs hX_fixed).FixedValues → ValuesOn (X.image SWIGNode.random) (swigΩ Ω) := fun s

=> zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M X hX_obs hX_fixed) s) have hxDo : Measurable xDo := measurable_zFixedAsRandom.comp (measurable_valuesProjection (fixSet_image_fixed_subset M X hX_obs hX_fixed)) let zCondXdo : Kernel (M.fixSet X hX_obs hX_fixed).FixedValues (ValuesOn Z (swigΩ Ω)) := (M.obsCondKernel Z (X.image SWIGNode.random) _hZ hXr).comap (fun s => (M.fixSetProj X hX_obs hX_fixed s, xDo s)) (prodMk (M.measurable_fixSetProj X hX_obs hX_fixed) hxDo) let xMarginal : Kernel (M.fixSet X hX_obs hX_fixed).FixedValues (ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) := (M.obsKernel.map (valuesProjection hXr)).comap (M.fixSetProj X hX_obs hX_fixed) (M.measurable_fixSetProj X hX_obs hX_fixed) let yCondXZ : Kernel ((M.fixSet X hX_obs hX_fixed).FixedValues × ValuesOn (X.image SWIGNode.random) (swigΩ Ω) × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := (M.obsCondKernel Y (X.image SWIGNode.random ∪ Z) _hY hXZ).comap (fun p => (M.fixSetProj X hX_obs hX_fixed p.1, valuesUnionMk p.2.1 p.2.2)) (prodMk ((M.measurable_fixSetProj X hX_obs hX_fixed).comp measurable_fst) (measurable_valuesUnionMk.comp (prodMk (measurable_fst.comp measurable_snd) (measurable_snd.comp measurable_snd)))) let innerY : Kernel ((M.fixSet X hX_obs hX_fixed).FixedValues × ValuesOn Z (swigΩ Ω)) (ValuesOn Y (swigΩ Ω)) := ((xMarginal.comap fst measurable_fst) ⊗ₖ (yCondXZ.comap (fun q : ((M.fixSet X hX_obs hX_fixed).FixedValues × ValuesOn Z (swigΩ Ω)) × ValuesOn (X.image SWIGNode.random) (swigΩ Ω) => (q.1.1, q.2, q.1.2)) (prodMk (measurable_fst.comp measurable_fst) (prodMk measurable_snd (measurable_snd.comp measurable_fst))))).map snd exact (zCondXdo ⊗ₖ innerY).map snd

Causalean.SCM.frontdoorAdjustment · Causalean/SCM/ID/Adjustment.lean:132 · uses SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , fixSet

theorem backdoorAdjustment_invariant reviewed

Causalean.SCM

Cross-SCM invariance of backdoorAdjustment. Fix two causal models M₁ and M₂ that share the same SWIG graph and the same observational kernel, and a treatment set X, an outcome set Y, and an adjustment set Z that are valid intervention data and observed variables in both models. Then the backdoor-adjustment kernel for Y given Z after intervening on X, computed within M₁, is the same as the one computed within M₂.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

M₁ M₂ :

SCM N Ω

h_swig :

M₁.toSWIGGraph = M₂.toSWIGGraph

_h_obs :

HEq M₁.obsKernel M₂.obsKernel

X :

hX_obs₁ :

∀ D ∈ X, SWIGNode.random D ∈ M₁.observed

hX_fixed₁ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed

hX_obs₂ :

∀ D ∈ X, SWIGNode.random D ∈ M₂.observed

hX_fixed₂ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed

Y Z :

hY₁ :

Y ⊆ M₁.observed

hZ₁ :

Z ⊆ M₁.observed

hY₂ :

Y ⊆ M₂.observed

hZ₂ :

Z ⊆ M₂.observed

conclusion

HEq (M₁.backdoorAdjustment X hX_obs₁ hX_fixed₁ Y Z hY₁ hZ₁) (M₂.backdoorAdjustment X hX_obs₂ hX_fixed₂ Y Z hY₂ hZ₂)

Proof (Lean source)

theorem backdoorAdjustment_invariant (M₁ M₂ : SCM N Ω) (h_swig : M₁.toSWIGGraph = M₂.toSWIGGraph) (_h_obs : HEq M₁.obsKernel M₂.obsKernel) (X : Finset N) (hX_obs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed) (hX_fixed₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed) (hX_obs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed) (hX_fixed₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed) (Y Z : Finset (SWIGNode N)) (hY₁ : Y ⊆ M₁.observed) (hZ₁ : Z ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (hZ₂ : Z ⊆ M₂.observed) : HEq (M₁.backdoorAdjustment X hX_obs₁ hX_fixed₁ Y Z hY₁ hZ₁) (M₂.backdoorAdjustment X hX_obs₂ hX_fixed₂ Y Z hY₂ hZ₂) := by -- Kernel-native transport: the remaining work is the HEq compatibility -- of `obsCondKernel` (via `heq_obsKernel`/`heq_obsCondKernel` from -- `EquivKernel.lean`) plus the `Kernel.comap`/`bind` reindexing along -- `fixSetProj` and `fillZrW`. obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases h_swig apply heq_of_eq -- After `cases h_swig`, the SWIGGraph-level indices on both sides are unified -- (proofs `fio/oi/od/...` are Prop-valued, hence definitionally equal by -- proof irrelevance), while the non-SWIGGraph fields `eT/iota/sf/mf/lD/pL` -- still differ. The `backdoorAdjustment` body uses only -- `toSWIGGraph`-derived data (`fixSetProj`, `fillZrW`, `FixedValues`, -- `observed`) plus `obsKernel` and `obsCondKernel`; the latter two agree -- via `_h_obs` and its derived `obsCondKernel` consequence. have h_ok : _ = _ := eq_of_heq _h_obs unfold SCM.backdoorAdjustment simp only -- Peel off `.map snd`. congr 1 -- Peel off `⊗ₖ` into zMarginalPost and condPost equalities. congr 1 · -- zMarginalPost equality: `(obsKernel.map (valuesProjection hZ)).comap fixSetProj` -- Only uses `obsKernel` (pointed from `h_ok`) and SWIG-level projections. congr 1 · rw [h_ok] · -- condPost equality: `(obsCondKernel Y CC hY hXZ).comap (fixSetProj, fillZrW)` -- Uses `obsCondKernel` (unfolds to `(obsKernel.map _).condKernel`). congr 1 unfold SCM.obsCondKernel SCM.obsCondPairKernel congr 1 rw [h_ok]

Causalean.SCM.backdoorAdjustment_invariant · Causalean/SCM/ID/Adjustment.lean:263 · uses SWIGGraph , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , ObservedValues , backdoorAdjustment , fixSet , obsKernel

theorem frontdoorAdjustment_invariant reviewed

Causalean.SCM

Cross-SCM invariance of frontdoorAdjustment. Fix two causal models M₁ and M₂ that share the same SWIG graph and the same observational kernel, and a treatment set X, an outcome set Y, and a mediator set Z that are valid intervention data and observed variables in both models. Then the frontdoor-adjustment kernel for Y through mediator Z after intervening on X, computed within M₁, is the same as the one computed within M₂.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

M₁ M₂ :

SCM N Ω

h_swig :

M₁.toSWIGGraph = M₂.toSWIGGraph

_h_obs :

HEq M₁.obsKernel M₂.obsKernel

X :

hX_obs₁ :

∀ D ∈ X, SWIGNode.random D ∈ M₁.observed

hX_fixed₁ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed

hX_obs₂ :

∀ D ∈ X, SWIGNode.random D ∈ M₂.observed

hX_fixed₂ :

∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed

Y Z :