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:99 · uses CausalQuery , SWIGGraph

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:121 · uses CausalQuery , SWIGGraph

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:133 · uses SCM , CausalQuery , NonIdentifiable , obsEquiv , SWIGGraph

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:155 · uses SCM , CausalQuery , SWIGGraph

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:189 · uses SCM , CausalQuery , IdentifiableUnder , SWIGGraph

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:181

Overlap 1 core · 0 supporting This file defines the kernel-level overlap condition used by do-calculus identification rules. ★ Rule2JointOverlap

Overlap

This file defines the kernel-level overlap condition used by do-calculus identification rules. The main predicate, Rule2JointOverlap, requires the post-intervention marginal on Z.random ∪ W to be absolutely continuous with respect to the corresponding observational marginal. This continuous-friendly support condition feeds the kernel-native Rule 2 and the backdoor/frontdoor identification theorems without imposing pointwise singleton positivity.

def Rule2JointOverlap reviewed

Causalean.SCM.ID

For a finite node-label set, measurable node-value spaces, a structural causal model, an intervention target set, proof that each target is an observed random node not already fixed, an additional observed-node set, proof that the random copies of the targets together with that set are observed, and a fixed-value assignment after intervention, Rule 2 joint overlap means that the post-intervention observational marginal on those nodes is absolutely continuous with respect to the corresponding pre-intervention observational marginal at the projected fixed-value assignment.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

M' :

SCM N Ω

Z :

hZ_obs :

∀ D ∈ Z, SWIGNode.random D ∈ M'.observed

hZ_fixed :

∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed

W :

hZrW :

Z.image SWIGNode.random ∪ W ⊆ M'.observed

s' :

(M'.fixSet Z hZ_obs hZ_fixed).FixedValues

def

Rule2JointOverlap M' Z hZ_obs hZ_fixed W hZrW s' :

Prop

given by

((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s' |>.map (valuesProjection ((SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))) ≪ (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s') |>.map (valuesProjection hZrW))

Causalean.SCM.ID.Rule2JointOverlap · Causalean/SCM/ID/Overlap.lean:48 · uses SCM , FixedValues , fixSet , SWIGNode , instDecidableEqSWIGNode

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:69 · 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` 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 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:109 · uses isAncestor , SCM , FixedValues , ObservedValues , fixSet , fixSetProj , fixSet_observed , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection

Backdoor 6 core · 5 supporting The kernel-equality backdoor_completeness is pointwise in the post-intervention slice, hence pointwise in the treatment value t. ★ backdoor_completeness_ae★ backdoor_identifiable_ae

Backdoor identification, a.e. in the treatment value

The kernel-equality backdoor_completeness is pointwise in the post-intervention slice, hence pointwise in the treatment value t. For non-atomic (continuous) treatment that statement reads the conditional obsCondKernel on the measure-zero {X = t} slice, where Mathlib's disintegration representative is not pinned by the observational law — so the pointwise form is 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:60 · uses SCM , FixedValues , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

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:70 · uses SCM , FixedValues , SWIGNode , instDecidableEqSWIGNode

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:97 · uses SCM , FixedValues , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

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:116 · uses SCM , FixedValues , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

theorem backdoor_completeness_ae reviewed

Causalean.SCM

Backdoor completeness, a.e. in the treatment value. 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 let Y, Z be observed outcome and adjustment sets, neither of which overlaps the treatment's random nodes, satisfying the backdoor criterion relative to (X,Y). Given a base configuration s0 at which overlap holds along every post-intervention slice 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 :

M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z

hDisj_YXr :

Disjoint Y (X.image SWIGNode.random)

hDisj_XrZ :

Disjoint (X.image SWIGNode.random) Z

s0 :

M.FixedValues

hOverlap :

∀ s : (M.fixSet X hObs hFix).FixedValues,

Rule2JointOverlap M X hObs hFix Z (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s

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 : M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z) (hDisj_YXr : Disjoint Y (X.image SWIGNode.random)) (hDisj_XrZ : Disjoint (X.image SWIGNode.random) Z) (s0 : M.FixedValues) (hOverlap : ∀ s : (M.fixSet X hObs hFix).FixedValues, Rule2JointOverlap M X hObs hFix Z (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s) (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 hDisj_YXr hDisj_XrZ s0 hOverlap hPositivity)

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

theorem backdoor_identifiable_ae reviewed

Causalean.SCM

Backdoor identifiability, a.e. in the treatment value (cross-SCM corollary). Fix two causal models M₁, M₂ that share the same SWIG graph and the same observational kernel, with base configurations that agree under this shared identification. Fix a treatment set X valid in both models and disjoint outcome/adjustment sets Y, Z that are observed in both models and disjoint from the treatment's random nodes, such that Z satisfies the backdoor criterion for (X,Y) in each model separately, with overlap holding along every post-intervention slice in each model and 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₁ :

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

h_bd₂ :

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

hDisj_YXr :

Disjoint Y (X.image SWIGNode.random)

hDisj_XrZ :

Disjoint (X.image SWIGNode.random) Z

s0₁ :

M₁.FixedValues

s0₂ :

M₂.FixedValues

hOverlap₁ :

∀ s : (M₁.fixSet X hObs₁ hFix₁).FixedValues,

Rule2JointOverlap M₁ X hObs₁ hFix₁ Z (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s

hOverlap₂ :

∀ s : (M₂.fixSet X hObs₂ hFix₂).FixedValues,

Rule2JointOverlap M₂ X hObs₂ hFix₂ Z (union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s

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₁ : M₁.toSWIGGraph.backdoorCriterion X hObs₁ hFix₁ Y Z) (h_bd₂ : M₂.toSWIGGraph.backdoorCriterion X hObs₂ hFix₂ Y Z) (hDisj_YXr : Disjoint Y (X.image SWIGNode.random)) (hDisj_XrZ : Disjoint (X.image SWIGNode.random) Z) (s0₁ : M₁.FixedValues) (s0₂ : M₂.FixedValues) (hOverlap₁ : ∀ s : (M₁.fixSet X hObs₁ hFix₁).FixedValues, Rule2JointOverlap M₁ X hObs₁ hFix₁ Z (union_subset (Finset.image_subset_iff.mpr hObs₁) hZ₁) s) (hOverlap₂ : ∀ s : (M₂.fixSet X hObs₂ hFix₂).FixedValues, Rule2JointOverlap M₂ X hObs₂ hFix₂ Z (union_subset (Finset.image_subset_iff.mpr hObs₂) hZ₂) s) (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₁ hDisj_YXr hDisj_XrZ s0₁ hOverlap₁ 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₂ hDisj_YXr hDisj_XrZ s0₁ hOverlap₂ 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:424 · uses SCM , BackdoorPositivityAE , FixedValues , Rule2JointOverlap , ObservedValues , doKernelY , fixSet , obsKernel , treatmentMarginal , SWIGGraph , backdoorCriterion , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

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:132
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:142
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:161
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:189
backdoor_completeness_ae_compProd theorem — Joint (compProd) completeness — primary form.

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 :

M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z

hDisj_YXr :

Disjoint Y (X.image SWIGNode.random)

hDisj_XrZ :

Disjoint (X.image SWIGNode.random) Z

s0 :

M.FixedValues

hOverlap :

∀ s : (M.fixSet X hObs hFix).FixedValues,
Rule2JointOverlap M X hObs hFix Z (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s

_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 : M.toSWIGGraph.backdoorCriterion X hObs hFix Y Z) (hDisj_YXr : Disjoint Y (X.image SWIGNode.random)) (hDisj_XrZ : Disjoint (X.image SWIGNode.random) Z) (s0 : M.FixedValues) (hOverlap : ∀ s : (M.fixSet X hObs hFix).FixedValues, Rule2JointOverlap M X hObs hFix Z (union_subset (Finset.image_subset_iff.mpr hObs) hZ) s) (_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.backdoor_rule2_ae M X hObs hFix Y Z hY hZ hXr hXrZ hDisj_YXr hDisj_XrZ _h_bd s0 hOverlap 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:216

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:25 · 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:34 · uses SWIGNode , ValuesOn , swigΩ

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:45 · uses SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

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

=> 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:63 · 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:79 · uses SCM , SWIGNode

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 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:94 · uses CausalQuery , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

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.

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:122 · uses SCM , interventionalQuery , interventionalQueryValid , standardFixedValues , doKernelY , isStandard , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

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:147 · uses SCM , interventionalQueryValid , SWIGGraph , SWIGNode

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:136

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:37 · uses SCM , FixedValues , fixSet , SWIGNode , ValuesOn , instMeasurableSpaceSwigΩ , swigΩ

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:61 · uses SCM , FixedValues , doObsKernelYMarginal , doKernelY , fixSet , SWIGGraph , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

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:69 · uses SCM , FixedValues , fixSet , SWIGNode , ValuesOn , instMeasurableSpaceSwigΩ , swigΩ

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:152 · uses SCM , FixedValues , fixSet , SWIGNode , ValuesOn , instMeasurableSpaceSwigΩ , swigΩ

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:283 · uses SCM , FixedValues , ObservedValues , backdoorAdjustment , fixSet , obsKernel , SWIGGraph , SWIGNode , ValuesOn , instMeasurableSpaceSwigΩ , swigΩ

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 :

hY₁ :

Y ⊆ M₁.observed

hZ₁ :

Z ⊆ M₁.observed

hY₂ :

Y ⊆ M₂.observed

hZ₂ :

Z ⊆ M₂.observed

conclusion

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

Proof (Lean source)

theorem frontdoorAdjustment_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₁.frontdoorAdjustment X hX_obs₁ hX_fixed₁ Y Z hY₁ hZ₁) (M₂.frontdoorAdjustment X hX_obs₂ hX_fixed₂ Y Z hY₂ hZ₂) := by -- Mirror the `backdoorAdjustment_invariant` strategy: destructure both -- SCMs, `cases h_swig` to align SWIGGraph indices, then `congr` through -- the `⊗ₖ` / `.map` / `.comap` plumbing. Every leg uses only -- `M.obsKernel` (transported via `_h_obs`) plus SWIGGraph-derived -- projections. 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 apply heq_of_eq have h_ok : _ = _ := eq_of_heq _h_obs unfold SCM.frontdoorAdjustment simp only -- The body is `((xMarginal ⊗ₖ zCondX) ⊗ₖ yCondXZ.comap …).map snd`. -- Each leg either uses `obsKernel` directly (xMarginal) or `obsCondKernel` -- (zCondX, yCondXZ). Unfolding `obsCondKernel` exposes the joint -- `obsKernel.map (·, ·)` whose `condKernel` is taken. All legs reduce -- to a single `obsKernel` argument that we rewrite via `h_ok`. unfold SCM.obsCondKernel SCM.obsCondPairKernel simp_rw [h_ok] -- After `simp_rw [h_ok]` the obsKernel mentions are unified. The -- remaining record-identity differences in `fixSetProj` etc. are -- proof-irrelevance noise (only SWIGGraph fields are used, all unified -- after `cases h_swig`); `rfl` closes the goal. rfl

Causalean.SCM.frontdoorAdjustment_invariant · Causalean/SCM/ID/Adjustment.lean:352 · uses SCM , FixedValues , ObservedValues , fixSet , frontdoorAdjustment , obsKernel , SWIGGraph , SWIGNode , ValuesOn , instMeasurableSpaceSwigΩ , swigΩ

3 supporting declarations (lemmas, instances)

instIsMarkovKernelObsCondKernel instance — For a finite, distinguishable node population with measurable, standard-Borel, nonempty node-value spaces and a structural causal model, a finite observed outcome-node set, and a finite observed conditioning-node set, the observational conditional kernel from the conditioning values to the outcome values is a Markov kernel: each of its values is a probability measure.

parameters

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

Y CC :

Finset (SWIGNode N)

hY :

Y ⊆ M.observed

hCC :

CC ⊆ M.observed

instance

instIsMarkovKernelObsCondKernel M Y CC hY hCC :
IsMarkovKernel (M.obsCondKernel Y CC hY hCC)

given by

by unfold SCM.obsCondKernel; infer_instance

Causalean.SCM.instIsMarkovKernelObsCondKernel · Causalean/SCM/ID/Adjustment.lean:61
instIsFiniteKernelBackdoorAdjustment 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, and finite observed outcome and adjustment-node sets, the backdoor-adjustment functional is a finite kernel.

parameters

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

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

instance

instIsFiniteKernelBackdoorAdjustment M X hX_obs hX_fixed Y Z hY hZ :
IsFiniteKernel (M.backdoorAdjustment X hX_obs hX_fixed Y Z hY hZ)

given by

by rw [SCM.backdoorAdjustment]; infer_instance

Causalean.SCM.instIsFiniteKernelBackdoorAdjustment · Causalean/SCM/ID/Adjustment.lean:142
instIsFiniteKernelFrontdoorAdjustment 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, and finite observed outcome and mediator-node sets, the frontdoor-adjustment functional is a finite kernel.

parameters

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

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

instance

instIsFiniteKernelFrontdoorAdjustment M X hX_obs hX_fixed Y Z hY hZ :
IsFiniteKernel (M.frontdoorAdjustment X hX_obs hX_fixed Y Z hY hZ)

given by

by rw [SCM.frontdoorAdjustment]; infer_instance

Causalean.SCM.instIsFiniteKernelFrontdoorAdjustment · Causalean/SCM/ID/Adjustment.lean:273

Frontdoor 4 core · 3 supporting This file states the frontdoor completeness / identification result tying the graph-level functional SCM.frontdoorAdjustment (defined in SCM/ID/Adjustment.lean) to the true post-intervention Y-marginal (M.fixSet X).obsKe ★ frontdoor_completeness_ae_compProd★ frontdoor_identifiable_ae

Frontdoor identification, a.e. in the treatment value

This file states the frontdoor completeness / identification result tying the graph-level functional SCM.frontdoorAdjustment (defined in SCM/ID/Adjustment.lean) to the true post-intervention Y-marginal (M.fixSet X).obsKernel.map π_Y, under the three frontdoor graph clauses recorded by SWIGGraph.frontdoorCriterion.

It is the frontdoor analogue of SCM/ID/Backdoor.lean, and is stated in the same regime-uniform a.e. style: the identity holds for νX-almost-every treatment value t (where νX is the observational treatment marginal), via the version-safe joint identity νX ⊗ₘ Kdo = νX ⊗ₘ Kfd (ProbabilityTheory.Kernel.ae_eq_of_compProd_eq).

Mediator representation

The mediator set is a base node set W : Finset N (so that it is intervenable — the frontdoor derivation routes through do(W)). Wherever frontdoorAdjustment expects a Finset (SWIGNode N) mediator it is instantiated at W.image SWIGNode.random.

Proof skeleton (for the main theorem; do-calculus Rules 2 and 3)

Pearl's derivation, in three legs, mirrored at the kernel level:

* Leg A — mediator (Rule 2, FD2). P(Z | do(X)) = P(Z | X): the Z-marginal of the post-intervention kernel equals the observational conditional P(Z | X = x_do), because there is no unblocked back-door path X → Z (the fd_no_backdoor_XZ clause). State this leg νX-a.e. (or in compProd form), never pointwise in the treatment slice — the pointwise conditional reads obsCondKernel on a νX-null {X = t} slice and is too strong for continuous treatment (see SCM/ID/Backdoor.lean). * Leg B — outcome (FD1 + FD3). Because Z intercepts every directed X → Y path (criterion fd_intercept), P(Y | do(X), Z) = P(Y | do(Z)); and since X is a valid back-door adjustment set for Z → Y (criterion fd_backdoor_ZY), P(Y | do(Z)) = ∫_{x'} P(Y | X = x', Z) dP(x'). This leg is exactly backdoor_completeness_ae_compProd instantiated with treatment := W, adjustment set := X.image SWIGNode.random, outcome := Y. * Composition. Chaining Leg A and Leg B reproduces the frontdoorAdjustment body ∫_z (∫_{x'} P(Y | X=x', Z=z) dP(x')) dP(Z | X=x_do).

The FD1 bridge is exposed as an explicit compProd substrate hypothesis, keeping the theorem focused on assembling the frontdoor functional from Rule 2, Rule 3, and the backdoor marginal-invariance leg rather than re-deriving disintegration inside the final theorem.

def frontdoorCriterion reviewed

Causalean.SWIGGraph

For a finite node population, a SWIG graph, a treatment-variable set whose random copies are observed and whose fixed copies are not already fixed, a mediator-variable set whose random copies are observed and whose fixed copies are not already fixed, and an outcome-node set, the frontdoor criterion holds exactly when the mediator random copies d-separate the outcomes from the treatment fixed copies after intervening on the treatments, the empty set satisfies the back-door criterion for treatment and mediator, the treatment random copies satisfy the back-door criterion for mediator and outcome, and the mediator random copies are disjoint from both treatment random copies and outcomes.

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

W :

hW_obs :

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

hW_fix :

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

Y :

def

frontdoorCriterion G X hX_obs hX_fix W hW_obs hW_fix Y :

Prop

given by

clause 1

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

clause 2

G.backdoorCriterion X hX_obs hX_fix (W.image SWIGNode.random) ∅

clause 3

G.backdoorCriterion W hW_obs hW_fix Y (X.image SWIGNode.random)

clause 4

Disjoint (W.image SWIGNode.random) (X.image SWIGNode.random)

clause 5

Disjoint (W.image SWIGNode.random) Y

Causalean.SWIGGraph.frontdoorCriterion · Causalean/SCM/ID/Frontdoor.lean:65 · uses SWIGGraph , SWIGNode

def frontdoorKernelY reviewed

Causalean.SCM

For a finite node population with measurable, nonempty standard-Borel node-value spaces, a structural causal model, a treatment-variable set whose random copies are observed and whose fixed copies are not already fixed, an outcome-node set, a mediator-node set, the requirement that every outcome node is observed, the requirement that every mediator node is observed, and an assignment to the model's original fixed nodes, the frontdoor-adjustment conditional law of outcomes indexed by treatment values is the frontdoor-adjustment law evaluated after extending the fixed-node assignment by that treatment value. It is defined by reindexing the graph-level frontdoor-adjustment law along this extension.

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 W :

hY :

Y ⊆ M.observed

hW :

W ⊆ M.observed

s0 :

M.FixedValues

def

frontdoorKernelY M X hObs hFix Y W hY hW s0 :

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

given by

(M.frontdoorAdjustment X hObs hFix Y W hY hW).comap (M.fixSetExtend X hObs hFix s0) (M.measurable_fixSetExtend X hObs hFix s0)

Causalean.SCM.frontdoorKernelY · Causalean/SCM/ID/Frontdoor.lean:134 · uses SCM , FixedValues , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ

theorem frontdoor_completeness_ae_compProd reviewed

Causalean.SCM

Frontdoor completeness — joint (compProd), version-safe primary form. Let X be a valid intervention set — observed and not already fixed, and Wbase likewise a valid intervention set of mediators, with the outcome set Y observed, the random copies of Wbase observed, and the random copies of X observed. Suppose the frontdoor criterion holds for (X, Wbase, Y), that Y is disjoint from the random copies of Wbase and the random copies of Wbase are disjoint from those of X, and that each of the three legs of the frontdoor decomposition — the do(X) leg, the do(Wbase) leg adjusting for X, and the nested do(X)-then-do(Wbase) leg — satisfies the matching backdoor overlap and positivity conditions. Then the joint law of the treatment marginal with the post-intervention Y-marginal equals the joint law of the treatment marginal with the frontdoor-adjustment functional.

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

Wbase :

hWobs :

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

hWfix :

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

Y :

hY :

Y ⊆ M.observed

hWr :

Wbase.image SWIGNode.random ⊆ M.observed

hXr :

X.image SWIGNode.random ⊆ M.observed

_hFD :

M.toSWIGGraph.frontdoorCriterion X hObs hFix Wbase hWobs hWfix Y

hDisj_YWr :

Disjoint Y (Wbase.image SWIGNode.random)

hDisj_WrXr :

Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)

s0 :

M.FixedValues

hOverlapA :

∀ s : (M.fixSet X hObs hFix).FixedValues,

Rule2JointOverlap M X hObs hFix (∅ : Finset (SWIGNode N)) (by simpa using hXr) s

hPositivityA :

M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using hXr) s0

hOverlapB :

∀ s : (M.fixSet Wbase hWobs hWfix).FixedValues,

Rule2JointOverlap M Wbase hWobs hWfix (X.image SWIGNode.random) (union_subset hWr hXr) s

hPositivityB :

M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) hXr (union_subset hWr hXr) s0

hOverlapFD1 :

∀ s : ((M.fixSet X hObs hFix).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))).FixedValues,

Rule2JointOverlap (M.fixSet X hObs hFix) Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm)) (∅ : Finset (SWIGNode N)) (by simpa [union_empty, SCM.fixSet_observed] using hWr) s

hPositivityFD1 :

∀ s : (M.fixSet X hObs hFix).FixedValues,

((((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [SCM.fixSet_observed] using hWr)) ⊗ₘ const _ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (empty_subset _)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [union_empty, SCM.fixSet_observed] using hWr)))

conclusion

(M.treatmentMarginal X hXr s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0)

= (M.treatmentMarginal X hXr s0) ⊗ₘ (M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0)

Proof (Lean source)

theorem frontdoor_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) (Wbase : Finset N) (hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed) (hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hWr : Wbase.image SWIGNode.random ⊆ M.observed) (hXr : X.image SWIGNode.random ⊆ M.observed) (_hFD : M.toSWIGGraph.frontdoorCriterion X hObs hFix Wbase hWobs hWfix Y) (hDisj_YWr : Disjoint Y (Wbase.image SWIGNode.random)) (hDisj_WrXr : Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random)) (s0 : M.FixedValues) (hOverlapA : ∀ s : (M.fixSet X hObs hFix).FixedValues, Rule2JointOverlap M X hObs hFix (∅ : Finset (SWIGNode N)) (by simpa using hXr) s) (hPositivityA : M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using hXr) s0) (hOverlapB : ∀ s : (M.fixSet Wbase hWobs hWfix).FixedValues, Rule2JointOverlap M Wbase hWobs hWfix (X.image SWIGNode.random) (union_subset hWr hXr) s) (hPositivityB : M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) hXr (union_subset hWr hXr) s0) (hOverlapFD1 : ∀ s : ((M.fixSet X hObs hFix).fixSet Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm))).FixedValues, Rule2JointOverlap (M.fixSet X hObs hFix) Wbase (by intro D hD; simpa [SCM.fixSet_observed] using hWobs D hD) (fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix ((disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm)) (∅ : Finset (SWIGNode N)) (by simpa [union_empty, SCM.fixSet_observed] using hWr) s) (hPositivityFD1 : ∀ s : (M.fixSet X hObs hFix).FixedValues, ((((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [SCM.fixSet_observed] using hWr)) ⊗ₘ const _ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (empty_subset _)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [union_empty, SCM.fixSet_observed] using hWr)))) : (M.treatmentMarginal X hXr s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0) = (M.treatmentMarginal X hXr s0) ⊗ₘ (M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0) := by exact frontdoor_fd1_interception_compProd M X hObs hFix Wbase hWobs hWfix Y hY hWr hXr _hFD hDisj_YWr hDisj_WrXr s0 hOverlapA hPositivityA hOverlapB hPositivityB hOverlapFD1 hPositivityFD1

Causalean.SCM.frontdoor_completeness_ae_compProd · Causalean/SCM/ID/Frontdoor.lean:1091 · uses SCM , BackdoorPositivityAE , FixedValues , Rule2JointOverlap , ObservedValues , disjoint_base_of_disjoint_random_image , doKernelY , fixSet , fixSet_fixed_not_mem_of_disjoint , frontdoorKernelY , obsKernel , treatmentMarginal , frontdoorCriterion , SWIGNode , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection , valuesUnionMk

theorem frontdoor_identifiable_ae reviewed

Causalean.SCM

Frontdoor identification, a.e. in the treatment value. Let X be a valid intervention set — observed and not already fixed, and Wbase likewise a valid intervention set of mediators, with the outcome set Y observed, the random copies of Wbase observed, and the random copies of X observed. Suppose the frontdoor criterion holds for (X, Wbase, Y), that Y is disjoint from the random copies of Wbase and the random copies of Wbase are disjoint from those of X, and that each of the three legs of the frontdoor decomposition — the do(X) leg, the do(Wbase) leg adjusting for X, and the nested do(X)-then-do(Wbase) leg — satisfies the matching backdoor overlap and positivity conditions. Then for treatmentMarginal-almost-every treatment value t, the post-intervention Y-marginal doKernelY at t equals the frontdoor-adjustment functional frontdoorKernelY 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

Wbase :

hWobs :

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

hWfix :

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

Y :