SCM.Do

The do-calculus on structural causal models: the three rules, global/local Markov properties, semi-graphoid axioms, and the kernel-level Rule 2 development.

Rule2­Kernel 21 core · 28 supporting · 8 submodules Kernel-level proof of do-calculus Rule 2: conditional kernels under intervention, levelset compatibility, and the rectangle-identity bridge.
Full­Cond­Indep 3 core · 6 supporting This file defines conditional independence on the full random state of a structural causal model, including both observed variables and latent variables. ★ fullCondIndep_weak_union★ fullCondIndep_contraction

Full Conditional Independence

This file defines conditional independence on the full random state of a structural causal model, including both observed variables and latent variables. It also develops the semi-graphoid rules needed before projecting full-distribution Markov statements down to observational distributions.

def FullCondIndep reviewed
Causalean.SCM

Full conditional independence on RandomValues M (= V ∪ L).

Definition (Lean source)
def FullCondIndep (M : SCM N Ω) [StandardBorelSpace M.RandomValues] (X Y Z : Finset (SWIGNode N)) (hX : X ⊆ M.randomVars) (hY : Y ⊆ M.randomVars) (hZ : Z ⊆ M.randomVars) (μ : Measure M.RandomValues) [IsFiniteMeasure μ] : Prop := CondIndepFun (comap (valuesProjection hZ) inferInstance) (comap_valuesProjection_le hZ) (valuesProjection hX) (valuesProjection hY) μ
Causalean.SCM.FullCondIndep · Causalean/SCM/Do/FullCondIndep.lean:32 · uses SCM , RandomValues , randomVars , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem fullCondIndep_weak_union reviewed
Causalean.SCM

Weak union for full conditional independence. Let M be a structural causal model and let μ be a finite measure on the full random state (observed together with latent variables). Suppose X, Y ∪ W, and Z ∪ W are all sets of M's random variables, and that, under μ, X is conditionally independent of Y ∪ W given Z. Then X is conditionally independent of Y given Z ∪ W.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.RandomValues
X Y W Z :
Finset (SWIGNode N)
hX :
X ⊆ M.randomVars
hYW :
(Y ∪ W) ⊆ M.randomVars
hZW :
(Z ∪ W) ⊆ M.randomVars
μ :
Measure M.RandomValues
IsFiniteMeasure μ
h :
FullCondIndep M X (Y ∪ W) Z hX hYW (Finset.subset_union_left.trans hZW) μ
conclusion
FullCondIndep M X Y (Z ∪ W) hX (Finset.subset_union_left.trans hYW) hZW μ
Proof (Lean source)
theorem fullCondIndep_weak_union (M : SCM N Ω) [StandardBorelSpace M.RandomValues] {X Y W Z : Finset (SWIGNode N)} (hX : X ⊆ M.randomVars) (hYW : (Y ∪ W) ⊆ M.randomVars) (hZW : (Z ∪ W) ⊆ M.randomVars) {μ : Measure M.RandomValues} [IsFiniteMeasure μ] (h : FullCondIndep M X (Y ∪ W) Z hX hYW (Finset.subset_union_left.trans hZW) μ) : FullCondIndep M X Y (Z ∪ W) hX (Finset.subset_union_left.trans hYW) hZW μ := by let hY : Y ⊆ M.randomVars := Finset.subset_union_left.trans hYW let hZ : Z ⊆ M.randomVars := Finset.subset_union_left.trans hZW unfold FullCondIndep at h ⊢ exact condIndep_valuesProjection_weak_union_axiom hX hYW hZ h
Causalean.SCM.fullCondIndep_weak_union · Causalean/SCM/Do/FullCondIndep.lean:96 · uses SCM , FullCondIndep , RandomValues , randomVars , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem fullCondIndep_contraction reviewed
Causalean.SCM

Contraction for full conditional independence. Let M be a structural causal model and let μ be a finite measure on the full random state. Suppose X, Y, W, and Z are all sets of M's random variables, and that, under μ, X is conditionally independent of Y given Z ∪ W and X is conditionally independent of W given Z. Then X is conditionally independent of Y ∪ W given Z.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.RandomValues
X Y W Z :
Finset (SWIGNode N)
hX :
X ⊆ M.randomVars
hY :
Y ⊆ M.randomVars
hW :
W ⊆ M.randomVars
hZ :
Z ⊆ M.randomVars
μ :
Measure M.RandomValues
IsFiniteMeasure μ
h1 :
FullCondIndep M X Y (Z ∪ W) hX hY (union_subset hZ hW) μ
h2 :
FullCondIndep M X W Z hX hW hZ μ
conclusion
FullCondIndep M X (Y ∪ W) Z hX (union_subset hY hW) hZ μ
Proof (Lean source)
theorem fullCondIndep_contraction (M : SCM N Ω) [StandardBorelSpace M.RandomValues] {X Y W Z : Finset (SWIGNode N)} (hX : X ⊆ M.randomVars) (hY : Y ⊆ M.randomVars) (hW : W ⊆ M.randomVars) (hZ : Z ⊆ M.randomVars) {μ : Measure M.RandomValues} [IsFiniteMeasure μ] (h1 : FullCondIndep M X Y (Z ∪ W) hX hY (Finset.union_subset hZ hW) μ) (h2 : FullCondIndep M X W Z hX hW hZ μ) : FullCondIndep M X (Y ∪ W) Z hX (Finset.union_subset hY hW) hZ μ := by let hYW : (Y ∪ W) ⊆ M.randomVars := Finset.union_subset hY hW let hZW : (Z ∪ W) ⊆ M.randomVars := Finset.union_subset hZ hW unfold FullCondIndep at h1 h2 ⊢ exact condIndep_valuesProjection_contraction_axiom hX hY hW hZ h1 h2
Causalean.SCM.fullCondIndep_contraction · Causalean/SCM/Do/FullCondIndep.lean:115 · uses SCM , FullCondIndep , RandomValues , randomVars , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
6 supporting declarations (lemmas, instances)
Semi­Graphoid 4 core · 7 supporting This file defines ObsCondIndep, conditional independence for projections of the observed state of a structural causal model under an arbitrary finite observational measure. ★ obsCondIndep_decomposition★ obsCondIndep_weak_union★ obsCondIndep_contraction

Observational Conditional Independence

This file defines ObsCondIndep, conditional independence for projections of the observed state of a structural causal model under an arbitrary finite observational measure. It also proves the semi-graphoid rules used by the Markov and do-calculus layers: obsCondIndep_symm, obsCondIndep_subset_right, obsCondIndep_decomposition, obsCondIndep_weak_union, and obsCondIndep_contraction. The corresponding condIndep_valuesProjection_* theorems expose the same coordinate-projection facts directly for finite product spaces.

def ObsCondIndep reviewed
Causalean.SCM

Observational conditional independence.

Definition (Lean source)
def ObsCondIndep (M : SCM N Ω) [StandardBorelSpace M.ObservedValues] (X Y Z : Finset (SWIGNode N)) (hX : X ⊆ M.observed) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (μ : Measure M.ObservedValues) [IsFiniteMeasure μ] : Prop := CondIndepFun (comap (valuesProjection hZ) inferInstance) (comap_valuesProjection_le hZ) (valuesProjection hX) (valuesProjection hY) μ
Causalean.SCM.ObsCondIndep · Causalean/SCM/Do/SemiGraphoid.lean:40 · uses SCM , ObservedValues , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem obsCondIndep_decomposition reviewed
Causalean.SCM

Decomposition. Let X, Y, W, Z be finite node sets of the structural causal model M, with X and the union of Y and W contained in the observed nodes, and Z contained in the observed nodes, under a finite measure μ on the observed values. If X is conditionally independent of the union of Y and W given Z, then X is conditionally independent of Y given Z.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.ObservedValues
X Y W Z :
Finset (SWIGNode N)
hX :
X ⊆ M.observed
hYW :
(Y ∪ W) ⊆ M.observed
hZ :
Z ⊆ M.observed
μ :
Measure M.ObservedValues
IsFiniteMeasure μ
h :
ObsCondIndep M X (Y ∪ W) Z hX hYW hZ μ
conclusion
ObsCondIndep M X Y Z hX (Finset.subset_union_left.trans hYW) hZ μ
Proof (Lean source)
theorem obsCondIndep_decomposition (M : SCM N Ω) [StandardBorelSpace M.ObservedValues] {X Y W Z : Finset (SWIGNode N)} (hX : X ⊆ M.observed) (hYW : (Y ∪ W) ⊆ M.observed) (hZ : Z ⊆ M.observed) {μ : Measure M.ObservedValues} [IsFiniteMeasure μ] (h : ObsCondIndep M X (Y ∪ W) Z hX hYW hZ μ) : ObsCondIndep M X Y Z hX (Finset.subset_union_left.trans hYW) hZ μ := by unfold ObsCondIndep at h ⊢ exact condIndep_valuesProjection_decomposition (μ := μ) hX hYW hZ h
Causalean.SCM.obsCondIndep_decomposition · Causalean/SCM/Do/SemiGraphoid.lean:218 · uses SCM , ObsCondIndep , ObservedValues , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem obsCondIndep_weak_union reviewed
Causalean.SCM

Weak union. Let X, Y, W, Z be finite node sets of the structural causal model M, with X and the union of Y and W contained in the observed nodes, and Z contained in the observed nodes, under a finite measure μ on the observed values. If X is conditionally independent of the union of Y and W given Z, then X is conditionally independent of Y given the union of Z and W.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.ObservedValues
X Y W Z :
Finset (SWIGNode N)
hX :
X ⊆ M.observed
hYW :
(Y ∪ W) ⊆ M.observed
hZ :
Z ⊆ M.observed
μ :
Measure M.ObservedValues
IsFiniteMeasure μ
h :
ObsCondIndep M X (Y ∪ W) Z hX hYW hZ μ
conclusion
ObsCondIndep M X Y (Z ∪ W) hX (Finset.subset_union_left.trans hYW) (union_subset hZ (Finset.subset_union_right.trans hYW)) μ
Proof (Lean source)
theorem obsCondIndep_weak_union (M : SCM N Ω) [StandardBorelSpace M.ObservedValues] {X Y W Z : Finset (SWIGNode N)} (hX : X ⊆ M.observed) (hYW : (Y ∪ W) ⊆ M.observed) (hZ : Z ⊆ M.observed) {μ : Measure M.ObservedValues} [IsFiniteMeasure μ] (h : ObsCondIndep M X (Y ∪ W) Z hX hYW hZ μ) : ObsCondIndep M X Y (Z ∪ W) hX (Finset.subset_union_left.trans hYW) (union_subset hZ (Finset.subset_union_right.trans hYW)) μ := by unfold ObsCondIndep at h ⊢ exact condIndep_valuesProjection_weak_union_axiom hX hYW hZ h
Causalean.SCM.obsCondIndep_weak_union · Causalean/SCM/Do/SemiGraphoid.lean:235 · uses SCM , ObsCondIndep , ObservedValues , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem obsCondIndep_contraction reviewed
Causalean.SCM

Contraction. Fix subsets X, Y, W, Z of the node set of the structural causal model M, with X, Y, W, and Z each contained in the observed nodes, and let μ be a finite measure on the observed values. If X is conditionally independent of Y given the union of Z and W and X is conditionally independent of W given Z, then X is conditionally independent of the union of Y and W given Z.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.ObservedValues
X Y W Z :
Finset (SWIGNode N)
hX :
X ⊆ M.observed
hY :
Y ⊆ M.observed
hW :
W ⊆ M.observed
hZ :
Z ⊆ M.observed
μ :
Measure M.ObservedValues
IsFiniteMeasure μ
h1 :
ObsCondIndep M X Y (Z ∪ W) hX hY (union_subset hZ hW) μ
h2 :
ObsCondIndep M X W Z hX hW hZ μ
conclusion
ObsCondIndep M X (Y ∪ W) Z hX (union_subset hY hW) hZ μ
Proof (Lean source)
theorem obsCondIndep_contraction (M : SCM N Ω) [StandardBorelSpace M.ObservedValues] {X Y W Z : Finset (SWIGNode N)} (hX : X ⊆ M.observed) (hY : Y ⊆ M.observed) (hW : W ⊆ M.observed) (hZ : Z ⊆ M.observed) {μ : Measure M.ObservedValues} [IsFiniteMeasure μ] (h1 : ObsCondIndep M X Y (Z ∪ W) hX hY (union_subset hZ hW) μ) (h2 : ObsCondIndep M X W Z hX hW hZ μ) : ObsCondIndep M X (Y ∪ W) Z hX (union_subset hY hW) hZ μ := by unfold ObsCondIndep at h1 h2 ⊢ exact condIndep_valuesProjection_contraction_axiom hX hY hW hZ h1 h2
Causalean.SCM.obsCondIndep_contraction · Causalean/SCM/Do/SemiGraphoid.lean:252 · uses SCM , ObsCondIndep , ObservedValues , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
7 supporting declarations (lemmas, instances)
Local­Markov 2 core · 2 supporting This file proves that each observed variable in a structural causal model is conditionally independent of its non-descendants, given all of its parents, under the full joint distribution over observed and latent variable ★ full_local_markov★ full_local_markov_latent

Full Local Markov Property

This file proves that each observed variable in a structural causal model is conditionally independent of its non-descendants, given all of its parents, under the full joint distribution over observed and latent variables. It also proves the latent-root analogue and records the pushforward bridge used to move conditional independence through the evaluation map.

The main public results are:

* SCM.condIndepFun_of_map, which transports conditional independence through a measurable pushforward. * SCM.full_local_markov, the observed-node local Markov property for jointKernel. * SCM.full_local_markov_latent, the corresponding independence statement for latent root nodes.

theorem full_local_markov reviewed
Causalean.SCM

Full Local Markov Property. If v is an observed node of the model, then under the joint distribution over all random (observed and latent) coordinates at fixed value s, the v-coordinate is conditionally independent of its non-descendants — restricted to random nodes — given all of its parents, including any latent parents, likewise restricted to random nodes.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.RandomValues
StandardBorelSpace M.LatentValues
v :
SWIGNode N
hv :
v ∈ M.observed
StandardBorelSpace (ValuesOn ({v} : Finset (SWIGNode N)) (swigΩ Ω))
Nonempty (ValuesOn ({v} : Finset (SWIGNode N)) (swigΩ Ω))
StandardBorelSpace (ValuesOn (M.dag.nonDescendants v ∩ M.randomVars) (swigΩ Ω))
Nonempty (ValuesOn (M.dag.nonDescendants v ∩ M.randomVars) (swigΩ Ω))
s :
M.FixedValues
conclusion
FullCondIndep M {v} (M.dag.nonDescendants v ∩ M.randomVars) (M.dag.parents v ∩ M.randomVars) (Finset.singleton_subset_iff.mpr (observed_subset_randomVars M hv)) inter_subset_right inter_subset_right (M.jointKernel s)
Proof (Lean source)
theorem full_local_markov (M : SCM N Ω) [StandardBorelSpace M.RandomValues] [StandardBorelSpace M.LatentValues] (v : SWIGNode N) (hv : v ∈ M.observed) [StandardBorelSpace (ValuesOn ({v} : Finset (SWIGNode N)) (swigΩ Ω))] [Nonempty (ValuesOn ({v} : Finset (SWIGNode N)) (swigΩ Ω))] [StandardBorelSpace (ValuesOn (M.dag.nonDescendants v ∩ M.randomVars) (swigΩ Ω))] [Nonempty (ValuesOn (M.dag.nonDescendants v ∩ M.randomVars) (swigΩ Ω))] (s : M.FixedValues) : FullCondIndep M {v} (M.dag.nonDescendants v ∩ M.randomVars) (M.dag.parents v ∩ M.randomVars) (Finset.singleton_subset_iff.mpr (observed_subset_randomVars M hv)) Finset.inter_subset_right Finset.inter_subset_right (M.jointKernel s) := by -- Outline: -- 1. `jointKernel M s = latentProduct.map (evalMap s)` (`jointKernel_apply_eq`). -- 2. `condIndepFun_of_map` with `φ = evalMap s` reduces the goal to CI on -- `LatentValues M` under `latentProduct`. -- 3. On `LatentValues`, `π_{{v}} ∘ evalMap s` factors through -- `π_{Pa(v) ∩ RV} ∘ evalMap s` via `evalMap_observed_unfold` (parent tuple -- of `structFun v` reads only from fixed values `s` and from parent-restricted -- random values), hence is measurable w.r.t. the conditioning σ-algebra. -- 4. `condIndepFun_of_measurable_left` closes the LatentValues-level CI. set hv_sub : ({v} : Finset (SWIGNode N)) ⊆ M.randomVars := Finset.singleton_subset_iff.mpr (observed_subset_randomVars M hv) with hv_sub_def set hPa_sub : M.dag.parents v ∩ M.randomVars ⊆ M.randomVars := Finset.inter_subset_right with hPa_sub_def set hND_sub : M.dag.nonDescendants v ∩ M.randomVars ⊆ M.randomVars := Finset.inter_subset_right with hND_sub_def -- Step 1: identify jointKernel s with latentProduct.map (evalMap s). have hjk : M.jointKernel s = M.latentProduct.map (fun ℓ => M.evalMap s ℓ) := M.jointKernel_apply_eq s have hφ_meas : Measurable (fun ℓ : M.LatentValues => M.evalMap s ℓ) := by have : (fun ℓ : M.LatentValues => M.evalMap s ℓ) = fun ℓ => uncurry M.evalMap (s, ℓ) := rfl rw [this] exact M.evalMap_measurable.comp (prodMk measurable_const measurable_id) haveI : IsFiniteMeasure (M.latentProduct.map (fun ℓ => M.evalMap s ℓ)) := hjk ▸ (inferInstance : IsFiniteMeasure (M.jointKernel s)) -- Step 2: build the LatentValues-level CI via `condIndepFun_of_measurable_left`. have hlat_ci : CondIndepFun (comap (valuesProjection hPa_sub ∘ (fun ℓ => M.evalMap s ℓ)) inferInstance) (comap_le ((measurable_valuesProjection hPa_sub).comp hφ_meas)) (valuesProjection hv_sub ∘ (fun ℓ => M.evalMap s ℓ)) (valuesProjection hND_sub ∘ (fun ℓ => M.evalMap s ℓ)) M.latentProduct := by refine ProbabilityTheory.condIndepFun_of_measurable_left ?_ ?_ · -- `π_{{v}} ∘ evalMap s` factors through `π_{Pa(v) ∩ RV} ∘ evalMap s` via -- the parent-factorization lemma `evalMap_factors_through_parents`. obtain ⟨g, hg_meas, hg_eq⟩ := M.evalMap_factors_through_parents s v hv -- Wrap `g : ValuesOn (Pa ∩ RV) → swigΩ Ω v` into the singleton product -- `g' : ValuesOn (Pa ∩ RV) → ValuesOn {v} (swigΩ Ω)` via a `cast` on the -- unique coordinate `w.val = v`. let g' : ValuesOn (M.dag.parents v ∩ M.randomVars) (swigΩ Ω) → ValuesOn ({v} : Finset (SWIGNode N)) (swigΩ Ω) := fun t w => cast (congrArg (swigΩ Ω) (Finset.mem_singleton.mp w.property).symm) (g t) have hg'_meas : Measurable g' := by refine measurable_pi_lambda _ ?_ rintro ⟨w, hw⟩ have hwv : w = v := Finset.mem_singleton.mp hw subst hwv -- After `subst`, `Finset.mem_singleton.mp hw : v = v = rfl` by proof -- irrelevance; `cast rfl = id`, so the singleton-wrapped function at -- the v-coord is just `g`. exact hg_meas -- Pointwise factorization of `valuesProjection hv_sub ∘ evalMap s`. have hfactor : (valuesProjection hv_sub ∘ (fun ℓ => M.evalMap s ℓ)) = g' ∘ (valuesProjection hPa_sub ∘ (fun ℓ => M.evalMap s ℓ)) := by funext ℓ w rcases w with ⟨w, hw⟩ have hwv : w = v := Finset.mem_singleton.mp hw subst hwv -- Both sides reduce: LHS = evalMap s ℓ ⟨v, hv_sub hw⟩, RHS unfolds -- `g'` and collapses the `cast` (proof-irrel on `v = v`). The -- factorization equation `hg_eq ℓ` closes the goal (membership-proof -- irrelevance on the subtype witnesses). exact hg_eq ℓ rw [hfactor] -- `g' ∘ φ` is `comap φ`-measurable because `φ` is comap-measurable by -- definition of `comap` (preimages of measurables generate the σ-algebra). refine hg'_meas.comp ?_ intro B hB exact ⟨B, hB, rfl⟩ · -- `π_{NonDesc(v) ∩ RV} ∘ evalMap s` is measurable (projection ∘ measurable). exact (measurable_valuesProjection hND_sub).comp hφ_meas -- Step 3: transport to RandomValues under `latentProduct.map (evalMap s)`. have hrand_ci : CondIndepFun (comap (valuesProjection hPa_sub) inferInstance) (comap_valuesProjection_le hPa_sub) (valuesProjection hv_sub) (valuesProjection hND_sub) (M.latentProduct.map (fun ℓ => M.evalMap s ℓ)) := condIndepFun_of_map (φ := fun ℓ => M.evalMap s ℓ) hφ_meas (measurable_valuesProjection hv_sub) (measurable_valuesProjection hND_sub) (measurable_valuesProjection hPa_sub) hlat_ci -- Finish: rewrite `latentProduct.map (evalMap s)` as `jointKernel s`. unfold FullCondIndep convert hrand_ci using 2
Causalean.SCM.full_local_markov · Causalean/SCM/Do/LocalMarkov.lean:108 · uses nonDescendants , parents , SCM , FixedValues , FullCondIndep , LatentValues , RandomValues , instIsMarkovKernelJointKernel , jointKernel , observed_subset_randomVars , randomVars , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem full_local_markov_latent reviewed
Causalean.SCM

Latent Local Markov Property. If a is a latent (unobserved) node of the model, then under the joint distribution over all random coordinates at fixed value s, the a-coordinate is unconditionally independent of its non-descendants — restricted to random nodes — i.e. conditionally independent given the empty conditioning set.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.RandomValues
StandardBorelSpace M.LatentValues
a :
SWIGNode N
ha :
a ∈ M.unobserved
StandardBorelSpace (ValuesOn ({a} : Finset (SWIGNode N)) (swigΩ Ω))
Nonempty (ValuesOn ({a} : Finset (SWIGNode N)) (swigΩ Ω))
StandardBorelSpace (ValuesOn (M.dag.nonDescendants a ∩ M.randomVars) (swigΩ Ω))
Nonempty (ValuesOn (M.dag.nonDescendants a ∩ M.randomVars) (swigΩ Ω))
s :
M.FixedValues
conclusion
FullCondIndep M {a} (M.dag.nonDescendants a ∩ M.randomVars) (∅ : Finset (SWIGNode N)) (Finset.singleton_subset_iff.mpr (mem_union_right _ ha)) inter_subset_right (empty_subset _) (M.jointKernel s)
Proof (Lean source)
theorem full_local_markov_latent (M : SCM N Ω) [StandardBorelSpace M.RandomValues] [StandardBorelSpace M.LatentValues] (a : SWIGNode N) (ha : a ∈ M.unobserved) [StandardBorelSpace (ValuesOn ({a} : Finset (SWIGNode N)) (swigΩ Ω))] [Nonempty (ValuesOn ({a} : Finset (SWIGNode N)) (swigΩ Ω))] [StandardBorelSpace (ValuesOn (M.dag.nonDescendants a ∩ M.randomVars) (swigΩ Ω))] [Nonempty (ValuesOn (M.dag.nonDescendants a ∩ M.randomVars) (swigΩ Ω))] (s : M.FixedValues) : FullCondIndep M {a} (M.dag.nonDescendants a ∩ M.randomVars) (∅ : Finset (SWIGNode N)) (Finset.singleton_subset_iff.mpr (mem_union_right _ ha)) Finset.inter_subset_right (empty_subset _) (M.jointKernel s) := by classical set hv_sub : ({a} : Finset (SWIGNode N)) ⊆ M.randomVars := Finset.singleton_subset_iff.mpr (mem_union_right _ ha) with hv_sub_def set hND_sub : M.dag.nonDescendants a ∩ M.randomVars ⊆ M.randomVars := Finset.inter_subset_right with hND_sub_def set hE : (∅ : Finset (SWIGNode N)) ⊆ M.randomVars := empty_subset _ with hE_def -- Step A: jointKernel s = latentProduct.map (evalMap s) and measurability of evalMap s. have hjk : M.jointKernel s = M.latentProduct.map (fun ℓ => M.evalMap s ℓ) := M.jointKernel_apply_eq s have hφ_meas : Measurable (fun ℓ : M.LatentValues => M.evalMap s ℓ) := by have : (fun ℓ : M.LatentValues => M.evalMap s ℓ) = fun ℓ => uncurry M.evalMap (s, ℓ) := rfl rw [this] exact M.evalMap_measurable.comp (prodMk measurable_const measurable_id) -- Step B: jointKernel s is a probability measure (pushforward of Measure.pi of probability -- measures is probability). haveI hP_joint : IsProbabilityMeasure (M.jointKernel s) := by rw [hjk] exact isProbabilityMeasure_map hφ_meas.aemeasurable -- Step C: The conditioning σ-algebra collapses to ⊥ because the codomain -- `ValuesOn ∅ (swigΩ Ω)` is a subsingleton (empty index Finset). have h_subs : Subsingleton (ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) := by refine ⟨fun f g => ?_⟩ funext ⟨w, hw⟩ exact absurd hw (notMem_empty _) have h_bot : comap (valuesProjection (Ω := swigΩ Ω) hE) inferInstance = (⊥ : MeasurableSpace M.RandomValues) := @comap_eq_bot_of_subsingleton _ _ _ h_subs _ -- Step D: Reduce the goal to `CondIndepFun ⊥ bot_le …`. The conditioning -- σ-algebra `comap (valuesProjection hE) inferInstance` equals `⊥` (h_bot), -- so we prove the `⊥`-version and transport via `convert`. suffices h_ci : CondIndepFun (⊥ : MeasurableSpace M.RandomValues) bot_le (valuesProjection hv_sub) (valuesProjection hND_sub) (M.jointKernel s) by unfold FullCondIndep convert h_ci using 2 apply condIndepFun_bot_of_indepFun (measurable_valuesProjection hv_sub) (measurable_valuesProjection hND_sub) -- Remaining: IndepFun (valuesProjection hv_sub) (valuesProjection hND_sub) (M.jointKernel s). -- Step E: rewrite jointKernel and reduce to IndepFun on latentProduct. rw [hjk] refine indepFun_of_map hφ_meas.aemeasurable (measurable_valuesProjection hv_sub) (measurable_valuesProjection hND_sub) ?_ -- Step F: disjoint latent coordinate index sets. set A : {u // u ∈ M.unobserved} := ⟨a, ha⟩ with hA_def let S_idx : Finset {u // u ∈ M.unobserved} := {A} let T_idx : Finset {u // u ∈ M.unobserved} := Finset.univ.erase A have h_disj : Disjoint S_idx T_idx := Finset.disjoint_singleton_left.mpr (Finset.notMem_erase _ _) -- Step G: LHS singleton wrap (mirrors the g' pattern in `full_local_markov`). let wrap_a : ((i : {i // i ∈ S_idx}) → swigΩ Ω i.val.val) → ValuesOn ({a} : Finset (SWIGNode N)) (swigΩ Ω) := fun r w => cast (congrArg (swigΩ Ω) (Finset.mem_singleton.mp w.property).symm) (r ⟨A, Finset.mem_singleton.mpr rfl⟩) have hwrap_meas : Measurable wrap_a := by refine measurable_pi_lambda _ ?_ rintro ⟨w, hw⟩ have hwv : w = a := Finset.mem_singleton.mp hw subst hwv exact measurable_pi_apply _ have h_LHS : (valuesProjection hv_sub ∘ fun ℓ : M.LatentValues => M.evalMap s ℓ) = wrap_a ∘ fun ℓ : M.LatentValues => fun i : {i // i ∈ S_idx} => ℓ i.val := by funext ℓ w rcases w with ⟨w, hw⟩ have hwv : w = a := Finset.mem_singleton.mp hw subst hwv -- Note: `subst` substitutes `a := w` (not `w := a`), so within this -- block the theorem's `a`, `ha` are renamed to `w`, `ha`. Both sides -- reduce to `ℓ ⟨w, ha⟩` via `evalMap_unobserved`; the `cast` in `wrap_a` -- collapses on `rfl` (proof-irrelevance on `w = w`). exact evalMap_unobserved M s ℓ ⟨w, hv_sub hw⟩ ha -- Step H: RHS factorization via the helper. have h_T_excl : ∀ v ∈ M.dag.nonDescendants a ∩ M.randomVars, ¬ M.dag.isAncestor a v ∧ v ≠ a := by intro v hv have hv_nd : v ∈ M.dag.nonDescendants a := (Finset.mem_inter.mp hv).1 exact (Finset.mem_filter.mp hv_nd).2 obtain ⟨g_T, hg_T_meas, hg_T_eq⟩ := M.evalMap_factors_excluding_latent s a ha (M.dag.nonDescendants a ∩ M.randomVars) hND_sub h_T_excl have h_RHS : (valuesProjection hND_sub ∘ fun ℓ : M.LatentValues => M.evalMap s ℓ) = g_T ∘ fun ℓ : M.LatentValues => fun i : {i // i ∈ T_idx} => ℓ i.val := by funext ℓ exact hg_T_eq ℓ -- Step I: base IndepFun from `indepFun_pi_of_disjoint` over disjoint -- latent index sets. haveI : ∀ i, IsProbabilityMeasure (M.latentDist i) := M.isProbability_latent letI f_unobs : Fintype {i // i ∈ M.unobserved} := Fintype.ofFinite _ have h_base_pi : IndepFun (fun (ℓ : M.LatentValues) (i : {i // i ∈ S_idx}) => ℓ i.val) (fun (ℓ : M.LatentValues) (i : {i // i ∈ T_idx}) => ℓ i.val) (pi M.latentDist) := indepFun_pi_of_disjoint M.latentDist h_disj have h_fintype : f_unobs = fintype M.unobserved := Subsingleton.elim _ _ have h_base : IndepFun (fun (ℓ : M.LatentValues) (i : {i // i ∈ S_idx}) => ℓ i.val) (fun (ℓ : M.LatentValues) (i : {i // i ∈ T_idx}) => ℓ i.val) M.latentProduct := by rw [h_fintype] at h_base_pi simpa only [latentProduct] using h_base_pi -- Step J: post-compose via `IndepFun.comp` with `wrap_a`, `g_T`. rw [h_LHS, h_RHS] exact h_base.comp hwrap_meas hg_T_meas
Causalean.SCM.full_local_markov_latent · Causalean/SCM/Do/LocalMarkov.lean:242 · uses nonDescendants , SCM , FixedValues , FullCondIndep , LatentValues , RandomValues , instIsMarkovKernelJointKernel , jointKernel , randomVars , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
2 supporting declarations (lemmas, instances)
Cutset­DSep 2 core · 10 supporting This file transfers d-separation from a target set Y to the latent cutset that drives Y while avoiding an overridden block. ★ cutsetLatent_dSep_of_dSep★ cutsetLatent_dSep_of_fixSet_dSep

Concatenation d-separation for the latent cutset

This file transfers d-separation from a target set Y to the latent cutset that drives Y while avoiding an overridden block. If Y is d-separated from the randomised do-block Zr given the adjustment set W together with a block of fixed nodes F, then the same separation holds for the latent cutset cutsetLatent Y (Zr ∪ W). The proof concatenates an active path from Zr to a cutset node c with the directed cutset arm c → … → Y: the join at the latent node c is a fork, so the glued path is active and reaches Y from Zr, contradicting the assumed separation.

Main results

* SCM.cutsetLatent_dSep_of_dSep — the concatenation d-separation: dSep Y Zr (W ∪ F) → dSep (cutsetLatent Y (Zr ∪ W)) Zr (W ∪ F). * SCM.cutsetLatent_dSep_of_fixSet_dSep — the cross-model variant: separation of Y from Zr in the intervened graph fixSet Z (given W ∪ fixSet.fixed), together with backdoor criterion (i) for W (no w ∈ W is a base-graph descendant of any treatment random D, D ∈ Z), yields the same latent-cutset separation in the base graph M. The base-graph active path is transported edge-by-edge into fixSet Z; criterion (i) guarantees no treatment out-edge is needed.

theorem cutsetLatent_dSep_of_dSep reviewed
Causalean.SCM

Concatenation d-separation for the latent cutset. Suppose W consists of observed nodes and F consists of fixed nodes, and that the target set Y is d-separated from the randomised do-block Zr given W together with F. Then the latent cutset cutsetLatent Y (Zr ∪ W) — the latent roots reaching Y along a directed path whose interior avoids Zr ∪ W — is likewise d-separated from Zr given the same W ∪ F.

Formal statement
hypotheses
M :
SCM N Ω
Y Zr W F :
Finset (SWIGNode N)
hW :
W ⊆ M.observed
hF :
F ⊆ M.fixed
hdSep :
M.dag.dSep Y Zr (W ∪ F)
conclusion
M.dag.dSep (M.cutsetLatent Y (Zr ∪ W)) Zr (W ∪ F)
Proof (Lean source)
theorem cutsetLatent_dSep_of_dSep (M : SCM N Ω) (Y Zr W F : Finset (SWIGNode N)) (hW : W ⊆ M.observed) (hF : F ⊆ M.fixed) (hdSep : M.dag.dSep Y Zr (W ∪ F)) : M.dag.dSep (M.cutsetLatent Y (Zr ∪ W)) Zr (W ∪ F) := by classical have hdYZr : Disjoint Y Zr := hdSep.1 have hdZrWF : Disjoint Zr (W ∪ F) := hdSep.2.2.1 -- Work with the symmetric form `dSep Zr · (W ∪ F)`. refine (M.dag.dSep_symm _ _ _ ?_) refine ⟨?_, ?_, ?_, ?_⟩ · rw [Finset.disjoint_left] intro c hcZr hcCut rcases (M.mem_cutsetLatent.mp hcCut) with ⟨_, y, hyY, hcy⟩ rcases hcy with hcEqy | hcAv · exact Finset.disjoint_left.mp hdYZr (by simpa [hcEqy] using hyY) hcZr · obtain ⟨q, hq_len, hq_head, hq_last, hq_edge, hq_int⟩ := hcAv.exists_path have hq_intWF : ∀ (i : ℕ) (hi : i + 2 < q.length), q.get ⟨i + 1, by omega⟩ ∉ W ∪ F := by intro i hi hmem rcases Finset.mem_union.mp hmem with hmW | hmF · exact hq_int i hi (mem_union_right _ hmW) · have hedge : M.dag.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, by omega⟩) := hq_edge i (by omega) have hpar : q.get ⟨i, by omega⟩ ∈ M.dag.parents (q.get ⟨i + 1, by omega⟩) := M.dag.mem_parents.mpr hedge have hroot : M.dag.parents (q.get ⟨i + 1, by omega⟩) = ∅ := M.fixed_are_roots _ (hF hmF) rw [hroot] at hpar exact absurd hpar (notMem_empty _) have hq_act : M.dag.IsActivePath (W ∪ F) q := M.dag.isActivePath_of_directed hq_edge hq_intWF have hyReachZr : y ∈ M.dag.bbReachableVertices (W ∪ F) Zr := by rw [M.dag.bbReachableVertices_iff_activePath] exact ⟨c, hcZr, q, hq_len, hq_act, hq_head, hq_last⟩ have hdSepZr : M.dag.dSep Zr Y (W ∪ F) := M.dag.dSep_symm _ _ _ hdSep exact Finset.disjoint_left.mp hdSepZr.2.2.2 hyReachZr hyY · exact hdZrWF · rw [Finset.disjoint_left] intro c hcCut hcWF have hc_lat : c ∈ M.unobserved := (M.mem_cutsetLatent.mp hcCut).1 rcases Finset.mem_union.mp hcWF with hcW | hcF · exact not_obs_of_unobs M.toSWIGGraph hc_lat (hW hcW) · obtain ⟨m, hm⟩ := M.fixed_is_fixed c (hF hcF) obtain ⟨k, hk⟩ := M.unobserved_is_random c hc_lat rw [hm] at hk cases hk · rw [Finset.disjoint_left] intro c hcReach hcCut -- `c` is reachable from `Zr` given `W ∪ F`, and lies in the cutset. have hdSepZr : M.dag.dSep Zr Y (W ∪ F) := M.dag.dSep_symm _ _ _ hdSep -- Unpack the cutset membership: an avoiding arm to some `y ∈ Y`. rcases (M.mem_cutsetLatent.mp hcCut) with ⟨hc_lat, y, hyY, hcy⟩ -- Active `Zr → c` path. rw [M.dag.bbReachableVertices_iff_activePath] at hcReach obtain ⟨zr, hzrZr, pa, hpa_len, hpa_act, hpa_head, hpa_last⟩ := hcReach -- `c ∉ W ∪ F`: latent nodes are neither observed nor fixed. have hc_notWF : c ∉ W ∪ F := by intro hcWF rcases Finset.mem_union.mp hcWF with hcW | hcF · exact not_obs_of_unobs M.toSWIGGraph hc_lat (hW hcW) · -- `c ∈ F ⊆ fixed` is `.fixed`-form, but `c ∈ unobserved` is `.random`-form. obtain ⟨m, hm⟩ := M.fixed_is_fixed c (hF hcF) obtain ⟨k, hk⟩ := M.unobserved_is_random c hc_lat rw [hm] at hk cases hk rcases hcy with hcEqy | hcAv · -- Degenerate: `c = y ∈ Y`, but `c` is reachable from `Zr`. refine Finset.disjoint_left.mp hdSepZr.2.2.2 ?_ (hcEqy ▸ hyY) rw [M.dag.bbReachableVertices_iff_activePath] exact ⟨zr, hzrZr, pa, hpa_len, hpa_act, hpa_head, hpa_last⟩ · -- Build the directed arm `c → … → y` and concatenate. obtain ⟨q, hq_len, hq_head, hq_last, hq_edge, hq_int⟩ := hcAv.exists_path -- Interior nodes of `q` avoid `W ∪ F`. have hq_intWF : ∀ (i : ℕ) (hi : i + 2 < q.length), q.get ⟨i + 1, by omega⟩ ∉ W ∪ F := by intro i hi hmem rcases Finset.mem_union.mp hmem with hmW | hmF · -- `q[i+1] ∈ W ⊆ Zr ∪ W`, contradicting interior-avoidance. exact hq_int i hi (mem_union_right _ hmW) · -- `q[i+1] ∈ F ⊆ fixed`, but it has an incoming edge, so it is not a root. have hedge : M.dag.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, by omega⟩) := hq_edge i (by omega) have hpar : q.get ⟨i, by omega⟩ ∈ M.dag.parents (q.get ⟨i + 1, by omega⟩) := M.dag.mem_parents.mpr hedge have hroot : M.dag.parents (q.get ⟨i + 1, by omega⟩) = ∅ := M.fixed_are_roots _ (hF hmF) rw [hroot] at hpar exact absurd hpar (notMem_empty _) -- Concatenate via the public active-path extension lemma. have hyReach : y ∈ M.dag.bbReachableVertices (W ∪ F) ({zr} : Finset (SWIGNode N)) := M.dag.bbReachable_extend_directed_arm hpa_len hpa_head hpa_last hpa_act hq_len hq_head hq_last hq_edge hq_intWF hc_notWF have hyReachZr : y ∈ M.dag.bbReachableVertices (W ∪ F) Zr := M.dag.bbReachableVertices_mono_source (Finset.singleton_subset_iff.mpr hzrZr) hyReach exact Finset.disjoint_left.mp hdSepZr.2.2.2 hyReachZr hyY
Causalean.SCM.cutsetLatent_dSep_of_dSep · Causalean/SCM/Do/CutsetDSep.lean:44 · uses dSep , SCM , cutsetLatent , SWIGNode , instFintype , instDecidableEqSWIGNode
theorem cutsetLatent_dSep_of_fixSet_dSep reviewed
Causalean.SCM

Cross-model concatenation d-separation for the latent cutset. Suppose that, in the intervened model M.fixSet Z _ _, the target set Y is d-separated from the randomised do-block Zr = Z.image .random given the adjustment set W together with the post-intervention fixed block, where W consists of observed nodes and no w ∈ W is, in the base graph M.dag, a descendant of any treatment's random copy .random D (D ∈ Z) — backdoor criterion (i). Then, in the base model M, the latent cutset cutsetLatent Y (Zr ∪ W) is d-separated from Zr given W ∪ M.fixed.

Formal statement
hypotheses
Y W :
Finset (SWIGNode N)
hW :
W ⊆ M.observed
hWNonDescM1 :
∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w
hdSep2 :
(M.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M.fixSet Z hZ_obs hZ_fixed).fixed)
conclusion
M.dag.dSep (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (Z.image SWIGNode.random) (W ∪ M.fixed)
Proof (Lean source)
theorem cutsetLatent_dSep_of_fixSet_dSep (Y W : Finset (SWIGNode N)) (hW : W ⊆ M.observed) (hWNonDescM1 : ∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w) (hdSep2 : (M.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M.fixSet Z hZ_obs hZ_fixed).fixed)) : M.dag.dSep (M.cutsetLatent Y (Z.image SWIGNode.random ∪ W)) (Z.image SWIGNode.random) (W ∪ M.fixed) := by classical -- The post-intervention conditioning set equals `C2 = W ∪ M.fixed ∪ Zfix`. have hCeq : W ∪ (M.fixSet Z hZ_obs hZ_fixed).fixed = W ∪ M.fixed ∪ Z.image SWIGNode.fixed := by rw [fixSet_fixed, ← union_assoc] -- Symmetric form of the goal: no cutset node is reachable from `Zr`. refine (M.dag.dSep_symm _ _ _ ?_) refine ⟨?_, ?_, ?_, ?_⟩ · rw [Finset.disjoint_left] intro zr hzrZr hzrCut obtain ⟨D, hD, hzrEq⟩ := Finset.mem_image.mp hzrZr have hzrObs : zr ∈ M.observed := by rw [← hzrEq] exact hZ_obs D hD exact not_obs_of_unobs M.toSWIGGraph ((M.mem_cutsetLatent.mp hzrCut).1) hzrObs · refine Disjoint.mono_right ?_ hdSep2.2.2.1 intro v hv rcases Finset.mem_union.mp hv with hvW | hvM · exact mem_union_left _ hvW · exact mem_union_right _ (by rw [fixSet_fixed] exact mem_union_left _ hvM) · rw [Finset.disjoint_left] intro c hcCut hcWF have hc_lat : c ∈ M.unobserved := (M.mem_cutsetLatent.mp hcCut).1 rcases Finset.mem_union.mp hcWF with hcW | hcF · exact not_obs_of_unobs M.toSWIGGraph hc_lat (hW hcW) · obtain ⟨m, hm⟩ := M.fixed_is_fixed c hcF obtain ⟨k, hk⟩ := M.unobserved_is_random c hc_lat rw [hm] at hk cases hk · rw [Finset.disjoint_left] intro c hcReach hcCut -- From the reachable cutset node, build an in-edge `M`-active path `Zr ⤳ Y`. obtain ⟨P, hPlen, hPact, hPhead, hPlast, hPin⟩ := exists_inEdge_activePath_to_Y M Z hZ_obs Y W hW hWNonDescM1 hcCut hcReach -- Transport it to `M.fixSet Z`, given `C2`. have hPact2 : (M.fixSet Z hZ_obs hZ_fixed).dag.IsActivePath (W ∪ M.fixed ∪ Z.image SWIGNode.fixed) P := path_fixSet_active M Z hZ_obs hZ_fixed W hWNonDescM1 hPact hPin -- Recover head/last elements. obtain ⟨zr, hzrZr, hzr_head⟩ := Finset.mem_image.mp hPhead obtain ⟨y, hyY, hy_last⟩ := Finset.mem_image.mp hPlast -- `P` witnesses reachability of `y` from `Zr` in `M.fixSet Z` given `C2`. have hyReach2 : y ∈ (M.fixSet Z hZ_obs hZ_fixed).dag.bbReachableVertices (W ∪ M.fixed ∪ Z.image SWIGNode.fixed) (Z.image SWIGNode.random) := ((M.fixSet Z hZ_obs hZ_fixed).dag.bbReachableVertices_iff_activePath (Z.image SWIGNode.random) (W ∪ M.fixed ∪ Z.image SWIGNode.fixed) y).mpr ⟨zr, hzrZr, P, hPlen, hPact2, hzr_head.symm, hy_last.symm⟩ -- Contradiction with `hdSep2` (symmetrised: no node reachable from `Zr` is in `Y`). rw [hCeq] at hdSep2 have hdSep2' := (M.fixSet Z hZ_obs hZ_fixed).dag.dSep_symm _ _ _ hdSep2 exact Finset.disjoint_left.mp hdSep2'.2.2.2 hyReach2 hyY
Causalean.SCM.cutsetLatent_dSep_of_fixSet_dSep · Causalean/SCM/Do/CutsetDSep.lean:768 · uses dSep , isAncestor , SCM , cutsetLatent , fixSet , SWIGNode , instFintype , instDecidableEqSWIGNode
10 supporting declarations (lemmas, instances)
  • edge_fixSet_of_edge lemma — A directed edge in the original graph remains an edge after fixing treatments when its source is not the random copy of any treatment being fixed.
    hypotheses
    u v :
    SWIGNode N
    he :
    M.dag.edge u v
    hu :
    ∀ D ∈ Z, u ≠ SWIGNode.random D
    conclusion
    (M.fixSet Z hZ_obs hZ_fixed).dag.edge u v
    Proof (Lean source)
    lemma edge_fixSet_of_edge {u v : SWIGNode N} (he : M.dag.edge u v) (hu : ∀ D ∈ Z, u ≠ SWIGNode.random D) : (M.fixSet Z hZ_obs hZ_fixed).dag.edge u v := by have h_eqrel : (M.fixSet Z hZ_obs hZ_fixed).dag.edge u v ↔ SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge Z u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] rw [h_eqrel] cases u with | random u' => by_cases h : u' ∈ Z · exact absurd rfl (hu u' h) · simpa only [SWIGGraph.splitMonoEdgeRel, if_neg h] using he | fixed d => by_cases h : d ∈ Z · -- `.fixed d` (`d ∈ Z`) is isolated in `M` (`hZ_fixed`), so `he` is impossible. have hfix_notin : SWIGNode.fixed d ∉ M.fixed := hZ_fixed d h have hiso := (M.fixed_outside_fixed_isolated d hfix_notin).2 have hch : v ∈ M.dag.children (SWIGNode.fixed d) := M.dag.mem_children.mpr he rw [hiso] at hch exact absurd hch (notMem_empty _) · simpa only [SWIGGraph.splitMonoEdgeRel, if_neg h] using he
    Causalean.SCM.edge_fixSet_of_edge · Causalean/SCM/Do/CutsetDSep.lean:165
  • edge_of_edge_fixSet lemma — Every directed edge after fixing treatments is either an original edge or the redirected outgoing edge from the fixed copy of a treatment being fixed.
    hypotheses
    u v :
    SWIGNode N
    he :
    (M.fixSet Z hZ_obs hZ_fixed).dag.edge u v
    conclusion
    M.dag.edge u v ∨ (∃ D ∈ Z, u = SWIGNode.fixed D ∧ M.dag.edge (SWIGNode.random D) v)
    Proof (Lean source)
    lemma edge_of_edge_fixSet {u v : SWIGNode N} (he : (M.fixSet Z hZ_obs hZ_fixed).dag.edge u v) : M.dag.edge u v ∨ (∃ D ∈ Z, u = SWIGNode.fixed D ∧ M.dag.edge (SWIGNode.random D) v) := by have h_eqrel : (M.fixSet Z hZ_obs hZ_fixed).dag.edge u v ↔ SWIGGraph.splitMonoEdgeRel M.toSWIGGraph.dag.edge Z u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG] rw [h_eqrel] at he cases u with | random u' => by_cases h : u' ∈ Z · simp only [SWIGGraph.splitMonoEdgeRel, if_pos h] at he · exact inl (by simpa only [SWIGGraph.splitMonoEdgeRel, if_neg h] using he) | fixed d => by_cases h : d ∈ Z · exact inr ⟨d, h, rfl, by simpa only [SWIGGraph.splitMonoEdgeRel, if_pos h] using he⟩ · exact inl (by simpa only [SWIGGraph.splitMonoEdgeRel, if_neg h] using he)
    Causalean.SCM.edge_of_edge_fixSet · Causalean/SCM/Do/CutsetDSep.lean:190
  • isAncestor_fixSet_of_isAncestor lemma — A directed ancestry path in a causal graph remains after intervening on a set when every possible edge source along that path is not a random copy of an intervened variable. Thus the original ancestor remains an ancestor in the intervened graph.
    hypotheses
    u v :
    SWIGNode N
    hanc :
    M.dag.isAncestor u v
    hNoT :
    ∀ s
    if
    (s = u ∨ M.dag.isAncestor u s)
    and
    M.dag.isAncestor s v
    then
    ∀ D ∈ Z, s ≠ SWIGNode.random D
    conclusion
    (M.fixSet Z hZ_obs hZ_fixed).dag.isAncestor u v
    Proof (Lean source)
    lemma isAncestor_fixSet_of_isAncestor {u v : SWIGNode N} (hanc : M.dag.isAncestor u v) (hNoT : ∀ s, (s = u ∨ M.dag.isAncestor u s) → M.dag.isAncestor s v → ∀ D ∈ Z, s ≠ SWIGNode.random D) : (M.fixSet Z hZ_obs hZ_fixed).dag.isAncestor u v := by induction hanc with | @edge b he => exact DAG.isAncestor.edge (edge_fixSet_of_edge M Z hZ_obs hZ_fixed he (hNoT u (inl rfl) (DAG.isAncestor.edge he))) | @trans w b hrec he ih => -- `u ⤳ w → b`. The last edge source `w` is `u` or a proper ancestor of `b` -- reachable from `u`, and an ancestor of `b`; so `hNoT` gives `w` non-treatment. have hwNoT : ∀ D ∈ Z, w ≠ SWIGNode.random D := hNoT w (inr hrec) (DAG.isAncestor.edge he) refine DAG.isAncestor.trans ?_ (edge_fixSet_of_edge M Z hZ_obs hZ_fixed he hwNoT) refine ih ?_ intro s hs hsw exact hNoT s hs (DAG.isAncestor.trans hsw he)
    Causalean.SCM.isAncestor_fixSet_of_isAncestor · Causalean/SCM/Do/CutsetDSep.lean:211
  • treatment_not_isAncestor_cond lemma — Under the backdoor non-descendancy condition, a treatment node cannot be a proper ancestor of any node in the observed-or-fixed conditioning block.
    hypotheses
    W :
    Finset (SWIGNode N)
    hWNonDescM1 :
    ∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w
    D :
    N
    hD :
    D ∈ Z
    c :
    SWIGNode N
    hc :
    c ∈ W ∪ M.fixed
    hanc :
    M.dag.isAncestor (SWIGNode.random D) c
    conclusion
    False
    Proof (Lean source)
    lemma treatment_not_isAncestor_cond (W : Finset (SWIGNode N)) (hWNonDescM1 : ∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w) {D : N} (hD : D ∈ Z) {c : SWIGNode N} (hc : c ∈ W ∪ M.fixed) (hanc : M.dag.isAncestor (SWIGNode.random D) c) : False := by rcases Finset.mem_union.mp hc with hcW | hcF · exact hWNonDescM1 D hD c hcW hanc · -- `c ∈ M.fixed` is a root, hence has no incoming edge: but `· ⤳ c` ends with -- an edge `· → c`, contradiction. have hpar : ∃ p, M.dag.edge p c := by cases hanc with | edge he => exact ⟨_, he⟩ | trans _ he => exact ⟨_, he⟩ obtain ⟨p, hpc⟩ := hpar have hpmem : p ∈ M.dag.parents c := M.dag.mem_parents.mpr hpc rw [M.fixed_are_roots c hcF] at hpmem exact absurd hpmem (notMem_empty _)
    Causalean.SCM.treatment_not_isAncestor_cond · Causalean/SCM/Do/CutsetDSep.lean:236
  • bbZAncestors_fixSet_transport lemma — A node in the Bayes-ball ancestor set of a target set and the model's fixed nodes remains in the corresponding ancestor set after intervention, once the fixed treatment copies are added to the target set, provided no treatment's random copy is an ancestor of a target node.
    hypotheses
    W :
    Finset (SWIGNode N)
    hWNonDescM1 :
    ∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w
    m :
    SWIGNode N
    hm :
    m ∈ M.dag.bbZAncestors (W ∪ M.fixed)
    conclusion
    m ∈ (M.fixSet Z hZ_obs hZ_fixed).dag.bbZAncestors (W ∪ M.fixed ∪ Z.image SWIGNode.fixed)
    Proof (Lean source)
    lemma bbZAncestors_fixSet_transport (W : Finset (SWIGNode N)) (hWNonDescM1 : ∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w) {m : SWIGNode N} (hm : m ∈ M.dag.bbZAncestors (W ∪ M.fixed)) : m ∈ (M.fixSet Z hZ_obs hZ_fixed).dag.bbZAncestors (W ∪ M.fixed ∪ Z.image SWIGNode.fixed) := by simp only [DAG.bbZAncestors, DAG.ancestralSet, DAG.ancestorsSet, mem_union, mem_filter, Finset.mem_univ, true_and] at hm ⊢ rcases hm with hmC | ⟨c, hcC, hanc⟩ · exact inl (inl hmC) · -- `m ⤳ c` in `M`; transport the directed path to `M.fixSet Z`. refine inr ⟨c, inl hcC, ?_⟩ have hcC' : c ∈ W ∪ M.fixed := Finset.mem_union.mpr hcC refine isAncestor_fixSet_of_isAncestor M Z hZ_obs hZ_fixed hanc ?_ intro s _ hsc D hD hsEq subst hsEq exact treatment_not_isAncestor_cond M Z W hWNonDescM1 hD hcC' hsc
    Causalean.SCM.bbZAncestors_fixSet_transport · Causalean/SCM/Do/CutsetDSep.lean:256
  • not_fixedTreatment_of_uadj lemma — A node incident to a directed edge in the base graph cannot be the fixed copy of a treatment variable that is newly fixed by the intervention.
    hypotheses
    hZ_fixed :
    ∀ D ∈ Z, SWIGNode.fixed D ∉ M.fixed
    a v :
    SWIGNode N
    h :
    M.dag.UAdj a v
    D :
    N
    hD :
    D ∈ Z
    conclusion
    v ≠ SWIGNode.fixed D
    Proof (Lean source)
    lemma not_fixedTreatment_of_uadj (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M.fixed) {a v : SWIGNode N} (h : M.dag.UAdj a v) {D : N} (hD : D ∈ Z) : v ≠ SWIGNode.fixed D := by intro hveq have hiso := M.fixed_outside_fixed_isolated D (hZ_fixed D hD) rw [hveq] at h rcases h with hav | hva · -- `edge a (fixed D)`: `a` is a parent of `fixed D`, but `fixed D` is a root. have hmem : a ∈ M.dag.parents (SWIGNode.fixed D) := M.dag.mem_parents.mpr hav rw [hiso.1] at hmem; exact absurd hmem (notMem_empty _) · -- `edge (fixed D) a`: `a` is a child of `fixed D`, but `fixed D` is isolated. have hmem : a ∈ M.dag.children (SWIGNode.fixed D) := M.dag.mem_children.mpr hva rw [hiso.2] at hmem; exact absurd hmem (notMem_empty _)
    Causalean.SCM.not_fixedTreatment_of_uadj · Causalean/SCM/Do/CutsetDSep.lean:278
  • path_fixSet_active lemma — An active path in the original structural causal model remains active after fixing the treatment set, when each of its directed edges has a non-treatment source.
    hypotheses
    W :
    Finset (SWIGNode N)
    hWNonDescM1 :
    ∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w
    P :
    List (SWIGNode N)
    hact :
    M.dag.IsActivePath (W ∪ M.fixed) P
    hInEdge :
    ∀ (i : ℕ) (hi : i + 1 < P.length),
    (M.dag.edge (P.get ⟨i, by omega⟩) (P.get ⟨i + 1, hi⟩) → ∀ D ∈ Z, P.get ⟨i, by omega⟩ ≠ SWIGNode.random D) ∧
    (M.dag.edge (P.get ⟨i + 1, hi⟩) (P.get ⟨i, by omega⟩) → ∀ D ∈ Z, P.get ⟨i + 1, hi⟩ ≠ SWIGNode.random D)
    conclusion
    (M.fixSet Z hZ_obs hZ_fixed).dag.IsActivePath (W ∪ M.fixed ∪ Z.image SWIGNode.fixed) P
    Proof (Lean source)
    lemma path_fixSet_active (W : Finset (SWIGNode N)) (hWNonDescM1 : ∀ D ∈ Z, ∀ w ∈ W, ¬ M.dag.isAncestor (SWIGNode.random D) w) {P : List (SWIGNode N)} (hact : M.dag.IsActivePath (W ∪ M.fixed) P) (hInEdge : ∀ (i : ℕ) (hi : i + 1 < P.length), (M.dag.edge (P.get ⟨i, by omega⟩) (P.get ⟨i + 1, hi⟩) → ∀ D ∈ Z, P.get ⟨i, by omega⟩ ≠ SWIGNode.random D) ∧ (M.dag.edge (P.get ⟨i + 1, hi⟩) (P.get ⟨i, by omega⟩) → ∀ D ∈ Z, P.get ⟨i + 1, hi⟩ ≠ SWIGNode.random D)) : (M.fixSet Z hZ_obs hZ_fixed).dag.IsActivePath (W ∪ M.fixed ∪ Z.image SWIGNode.fixed) P := by obtain ⟨hadj, hcoll⟩ := hact set M2 := M.fixSet Z hZ_obs hZ_fixed with hM2 -- Adjacency survives. have hadj2 : ∀ (i : ℕ) (hi : i + 1 < P.length), M2.dag.UAdj (P.get ⟨i, by omega⟩) (P.get ⟨i + 1, hi⟩) := by intro i hi rcases hadj i hi with he | he · exact inl (edge_fixSet_of_edge M Z hZ_obs hZ_fixed he ((hInEdge i hi).1 he)) · exact inr (edge_fixSet_of_edge M Z hZ_obs hZ_fixed he ((hInEdge i hi).2 he)) refine ⟨hadj2, fun i hi => ?_⟩ -- The triple (l, m, r) at index i. set l := P.get ⟨i, by omega⟩ with hl set m := P.get ⟨i + 1, by omega⟩ with hm set r := P.get ⟨i + 2, hi⟩ with hr have hc := hcoll i hi simp only at hc ⊢ -- M2-collider ↔ M1-collider on the path triple. have hColl_iff : M2.dag.IsCollider l m r ↔ M.dag.IsCollider l m r := by constructor · rintro ⟨hlm, hrm⟩ refine ⟨?_, ?_⟩ · rcases edge_of_edge_fixSet M Z hZ_obs hZ_fixed hlm with h | ⟨D, hD, hlEq, _⟩ · exact h · -- `l = .fixed D` (D ∈ Z) is impossible: `l` is path-adjacent to `m`. exact absurd hlEq (not_fixedTreatment_of_uadj M Z hZ_fixed (M.dag.UAdj_symm (hadj i (by omega))) hD) · rcases edge_of_edge_fixSet M Z hZ_obs hZ_fixed hrm with h | ⟨D, hD, hrEq, _⟩ · exact h · have hadj_mr : M.dag.UAdj m r := hadj (i + 1) (by omega) exact absurd hrEq (not_fixedTreatment_of_uadj M Z hZ_fixed hadj_mr hD) · rintro ⟨hlm, hrm⟩ exact ⟨edge_fixSet_of_edge M Z hZ_obs hZ_fixed hlm ((hInEdge i (by omega)).1 hlm), edge_fixSet_of_edge M Z hZ_obs hZ_fixed hrm ((hInEdge (i + 1) (by omega)).2 hrm)⟩ by_cases hC : M.dag.IsCollider l m r · rw [if_pos (hColl_iff.mpr hC)] rw [if_pos hC] at hc exact bbZAncestors_fixSet_transport M Z hZ_obs hZ_fixed W hWNonDescM1 hc · rw [if_neg (fun h => hC (hColl_iff.mp h))] rw [if_neg hC] at hc -- `m ∉ W ∪ M.fixed`; also `m ∉ Z.image .fixed` since `m` is on the path. intro hmem rcases Finset.mem_union.mp hmem with hm1 | hm2 · exact hc hm1 · obtain ⟨D, hD, hDeq⟩ := Finset.mem_image.mp hm2 exact not_fixedTreatment_of_uadj M Z hZ_fixed (hadj i (by omega)) hD (hm ▸ hDeq.symm)
    Causalean.SCM.path_fixSet_active · Causalean/SCM/Do/CutsetDSep.lean:294
  • activePath_forwardRun_absurd lemma — An active path that starts with an arrow flowing away from an ancestor cannot end at a root when that ancestor has no directed route to any activated conditioning ancestor. The result rules out a forward run that must either enter a root or create an activated collider.
    hypotheses
    V :
    Type*
    DecidableEq V
    Fintype V
    G :
    DAG V
    C :
    Finset V
    s :
    V
    hTreat :
    ∀ k
    if
    k ∈ G.bbZAncestors C
    then
    ¬ G.isAncestor s k
    conclusion
    ∀ (prev m : V) (rest : List V)
    if
    G.IsActivePath C (prev :: m :: rest)
    and
    G.edge prev m
    and
    (s = prev ∨ G.isAncestor s prev)
    and
    (∀ p, ¬ G.edge p ((prev :: m :: rest).getLast (by simp)))
    then
    False
    Proof (Lean source)
    lemma DAG.activePath_forwardRun_absurd {V : Type*} [DecidableEq V] [Fintype V] (G : DAG V) {C : Finset V} {s : V} (hTreat : ∀ k, k ∈ G.bbZAncestors C → ¬ G.isAncestor s k) : ∀ (prev m : V) (rest : List V), G.IsActivePath C (prev :: m :: rest) → G.edge prev m → (s = prev ∨ G.isAncestor s prev) → (∀ p, ¬ G.edge p ((prev :: m :: rest).getLast (by simp))) → False := by intro prev m rest induction rest generalizing prev m with | nil => intro hact hpm _hsprev hroot -- The run is `[prev, m]`; `m` is the last node and a root, but `prev → m`. exact hroot prev (by simpa using hpm) | cons t rest ih => intro hact hpm hsprev hroot -- `s ⤳ m` from `s ⤳ prev → m`. have hsm : G.isAncestor s m := by rcases hsprev with hEq | hanc · exact hEq ▸ DAG.isAncestor.edge hpm · exact DAG.isAncestor.trans hanc hpm obtain ⟨hadj, hcoll⟩ := hact -- Adjacency of `m` and `t` (triple index 0 in the path). have hmt : G.UAdj m t := by have h := hadj 1 (by simp) simpa using h -- The active-path triple condition at index 0: triple (prev, m, t). have htri := hcoll 0 (by simp) simp only [List.get_eq_getElem, List.getElem_cons_zero, List.getElem_cons_succ] at htri rcases hmt with hmt | htm · -- Forward `m → t`: recurse with `prev := m`, dropping `prev`. -- The tail `m :: t :: rest` is active. have hact_tail : G.IsActivePath C (m :: t :: rest) := by refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · have h := hadj (i + 1) (by simpa [Nat.add_assoc] using Nat.succ_lt_succ hi) simpa using h · have h := hcoll (i + 1) (by simpa [Nat.add_assoc] using Nat.succ_lt_succ hi) simpa [Nat.add_assoc] using h have hroot' : ∀ p, ¬ G.edge p ((m :: t :: rest).getLast (by simp)) := by simpa using hroot exact ih m t hact_tail hmt (inr hsm) hroot' · -- Backward `t → m`: `m` is a collider on the triple `(prev, m, t)`. have hC : G.IsCollider prev m t := ⟨hpm, htm⟩ rw [if_pos hC] at htri -- `htri : m ∈ bbZAncestors C`; but `s ⤳ m`. exact hTreat m htri hsm
    Causalean.DAG.activePath_forwardRun_absurd · Causalean/SCM/Do/CutsetDSep.lean:357
  • isActivePath_drop lemma — Removing any initial segment of an active graph path leaves a path that is still active under the same conditioning set.
    hypotheses
    V :
    Type*
    DecidableEq V
    Fintype V
    G :
    DAG V
    C :
    Finset V
    p :
    List V
    j :
    ℕ
    hact :
    G.IsActivePath C p
    conclusion
    G.IsActivePath C (p.drop j)
    Proof (Lean source)
    lemma DAG.isActivePath_drop {V : Type*} [DecidableEq V] [Fintype V] (G : DAG V) {C : Finset V} {p : List V} (j : ℕ) (hact : G.IsActivePath C p) : G.IsActivePath C (p.drop j) := by obtain ⟨hadj, hcoll⟩ := hact have hlen : (p.drop j).length = p.length - j := List.length_drop .. refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · have hi' : j + i + 1 < p.length := by rw [hlen] at hi; omega have e0 : (p.drop j).get ⟨i, by omega⟩ = p.get ⟨j + i, by omega⟩ := by simp [List.getElem_drop] have e1 : (p.drop j).get ⟨i + 1, hi⟩ = p.get ⟨j + (i + 1), by omega⟩ := by simp [List.getElem_drop] rw [e0, e1] have := hadj (j + i) (by omega) exact this · have hi' : j + i + 2 < p.length := by rw [hlen] at hi; omega have e0 : (p.drop j).get ⟨i, by omega⟩ = p.get ⟨j + i, by omega⟩ := by simp [List.getElem_drop] have e1 : (p.drop j).get ⟨i + 1, by omega⟩ = p.get ⟨j + (i + 1), by omega⟩ := by simp [List.getElem_drop] have e2 : (p.drop j).get ⟨i + 2, hi⟩ = p.get ⟨j + (i + 2), by omega⟩ := by simp [List.getElem_drop] rw [e0, e1, e2] have := hcoll (j + i) (by omega) exact this
    Causalean.DAG.isActivePath_drop · Causalean/SCM/Do/CutsetDSep.lean:409
  • get_appendTail lemma — Appending the tail of one nonempty list to another nonempty list preserves the first list's entries and then reads the remaining entries from the second list with a one-place shift.
    hypotheses
    V :
    Type*
    pa q :
    List V
    _hpa :
    pa ≠ []
    hq :
    q ≠ []
    conclusion
    (pa ++ q.tail).length = pa.length + q.length - 1 ∧
    (∀ (j : ℕ) (hj : j < pa.length), (pa ++ q.tail).get ⟨j, by rw [length_append]; have := length_tail (l := q); omega⟩ = pa.get ⟨j, hj⟩) ∧
    (∀ (j : ℕ) (hjL : pa.length ≤ j) (hj : j < (pa ++ q.tail).length), (pa ++ q.tail).get ⟨j, hj⟩ = q.get ⟨j - pa.length + 1, by rw [length_append, length_tail] at hj have : 1 ≤ q.length := List.length_pos_iff.mpr hq omega⟩)
    Proof (Lean source)
    lemma get_appendTail {V : Type*} (pa q : List V) (_hpa : pa ≠ []) (hq : q ≠ []) : (pa ++ q.tail).length = pa.length + q.length - 1 ∧ (∀ (j : ℕ) (hj : j < pa.length), (pa ++ q.tail).get ⟨j, by rw [length_append]; have := List.length_tail (l := q); omega⟩ = pa.get ⟨j, hj⟩) ∧ (∀ (j : ℕ) (hjL : pa.length ≤ j) (hj : j < (pa ++ q.tail).length), (pa ++ q.tail).get ⟨j, hj⟩ = q.get ⟨j - pa.length + 1, by rw [length_append, List.length_tail] at hj have : 1 ≤ q.length := List.length_pos_iff.mpr hq omega⟩) := by have htail_len : q.tail.length = q.length - 1 := List.length_tail have hqpos : 1 ≤ q.length := List.length_pos_iff.mpr hq refine ⟨?_, ?_, ?_⟩ · rw [length_append, htail_len]; omega · intro j hj simp only [List.get_eq_getElem, List.getElem_append_left (h := hj)] · intro j hjL hj have hjr : j - pa.length < q.tail.length := by rw [length_append] at hj; omega have e1 : (pa ++ q.tail).get ⟨j, hj⟩ = q.tail[j - pa.length]'hjr := by simp only [List.get_eq_getElem] rw [List.getElem_append_right (by omega)] rw [e1, List.getElem_tail] simp [List.get_eq_getElem]
    Causalean.SCM.get_appendTail · Causalean/SCM/Do/CutsetDSep.lean:446
Do­Calculus 3 core · 0 supporting This file states the three rules of Pearl's do-calculus for structural causal models in a single-intervention form. ★ do_rule1★ do_rule2_kernel★ do_rule3

Do-Calculus for Structural Causal Models

This file states the three rules of Pearl's do-calculus for structural causal models in a single-intervention form. The results connect graphical separation conditions in intervention graphs to observational conditional independences and conditional-kernel equalities used by the identification layer.

theorem do_rule1 reviewed
Causalean.SCM

Rule 1: Insertion/deletion of observations (single-SCM form). On any structural causal model M', suppose Y, Z, and W are all observed nodes of M', and that Y is d-separated from Z given W together with the fixed nodes M'.fixed, in the split graph M'.dag. Then, at any fixed-value point s, Y and Z are conditionally independent given W under the observational kernel M'.obsKernel s.

Formal statement
hypotheses
M' :
SCM N Ω
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
Y Z W :
Finset (SWIGNode N)
StandardBorelSpace (ValuesOn Y (swigΩ Ω))
Nonempty (ValuesOn Y (swigΩ Ω))
StandardBorelSpace (ValuesOn Z (swigΩ Ω))
Nonempty (ValuesOn Z (swigΩ Ω))
hY :
Y ⊆ M'.observed
hZ :
Z ⊆ M'.observed
hW :
W ⊆ M'.observed
hdSep :
M'.dag.dSep Y Z (W ∪ M'.fixed)
s :
M'.FixedValues
conclusion
ObsCondIndep M' Y Z W hY hZ hW (M'.obsKernel s)
Proof (Lean source)
theorem do_rule1 (M' : SCM N Ω) [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] (Y Z W : Finset (SWIGNode N)) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [StandardBorelSpace (ValuesOn Z (swigΩ Ω))] [Nonempty (ValuesOn Z (swigΩ Ω))] (hY : Y ⊆ M'.observed) (hZ : Z ⊆ M'.observed) (hW : W ⊆ M'.observed) (hdSep : M'.dag.dSep Y Z (W ∪ M'.fixed)) (s : M'.FixedValues) : ObsCondIndep M' Y Z W hY hZ hW (M'.obsKernel s) := by have hDisj_YZ : Disjoint Y Z := hdSep.1 have hDisj_YW : Disjoint Y W := Disjoint.mono_right Finset.subset_union_left hdSep.2.1 have hDisj_ZW : Disjoint Z W := Disjoint.mono_right Finset.subset_union_left hdSep.2.2.1 exact M'.globalMarkov_with_fixed Y Z W M'.fixed hY hZ hW (refl _) hdSep s
Causalean.SCM.do_rule1 · Causalean/SCM/Do/DoCalculus.lean:57 · uses dSep , SCM , FixedValues , ObsCondIndep , ObservedValues , instIsMarkovKernelObsKernel , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem do_rule2_kernel reviewed
Causalean.SCM

Rule 2: Action/observation exchange (single-SCM form, kernel-native). Fix a structural causal model M' and a treatment set Z for which each member's random copy is already observed in M' and each member's fixed copy is not yet among M''s fixed nodes, with outcome and conditioning sets Y and W, and with the random copies of Z and their union with W all observed in M'. Suppose that, in the model intervened on Z, Y is d-separated from the random copies of Z given W together with the post-intervention fixed nodes, that no fixed copy of a Z-variable is a post-intervention ancestor of any node in W, and that no random copy of a Z-variable is an M'-ancestor of any node in W, so W is not downstream of the intervention in either graph. At a fixed-value point s0, assume the law obtained by independently pairing a treatment value drawn from the observational marginal of Z's random copies with a conditioning value drawn from the observational marginal of W is absolutely continuous with respect to the actual observational joint law of Z's random copies and W. Then for almost every such independently-paired pair (t, w), the Y-given-W conditional kernel of the model intervened at t, evaluated at the fixed value extended by t and at w, equals the Y-given-(Z ∪ W) conditional kernel of M' evaluated at s0 and the point filled by combining t and w.

Formal statement
hypotheses
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
Y W :
Finset (SWIGNode N)
hY :
Y ⊆ M'.observed
hW :
W ⊆ M'.observed
hZr :
Z.image SWIGNode.random ⊆ M'.observed
hZrW :
Z.image SWIGNode.random ∪ W ⊆ M'.observed
hdSep :
(M'.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M'.fixSet Z hZ_obs hZ_fixed).fixed)
hWNonDesc :
∀ z ∈ Z, ∀ v ∈ W, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v
hWNonDescM1 :
∀ D ∈ Z, ∀ w ∈ W, ¬ M'.dag.isAncestor (SWIGNode.random D) w
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
CountableOrCountablyGenerated M'.FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))
MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
s0 :
M'.FixedValues
hPositivity_ae :
(((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M'.obsKernel s0).map (valuesProjection hZrW))
conclusion
∀ᵐ p ∂((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))),
(M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (M'.fixSetExtend Z hZ_obs hZ_fixed s0 p.1, p.2)
= M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, valuesUnionMk p.1 p.2)
Proof (Lean source)
theorem do_rule2_kernel (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (Y W : Finset (SWIGNode N)) (hY : Y ⊆ M'.observed) (hW : W ⊆ M'.observed) (hZr : Z.image SWIGNode.random ⊆ M'.observed) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) (hdSep : (M'.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M'.fixSet Z hZ_obs hZ_fixed).fixed)) (hWNonDesc : ∀ z ∈ Z, ∀ v ∈ W, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v) (hWNonDescM1 : ∀ D ∈ Z, ∀ w ∈ W, ¬ M'.dag.isAncestor (SWIGNode.random D) w) [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] [CountableOrCountablyGenerated M'.FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))] [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s0 : M'.FixedValues) (hPositivity_ae : (((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M'.obsKernel s0).map (valuesProjection hZrW))) : ∀ᵐ p ∂((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))), (M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (M'.fixSetExtend Z hZ_obs hZ_fixed s0 p.1, p.2) = M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, valuesUnionMk p.1 p.2) := SCM.obsCondKernel_fixSet_eq_ae_witness M' Z hZ_obs hZ_fixed Y W hY hW hZr hZrW hdSep hWNonDesc hWNonDescM1 s0 hPositivity_ae
Causalean.SCM.do_rule2_kernel · Causalean/SCM/Do/DoCalculus.lean:95 · uses dSep , isAncestor , SCM , FixedValues , ObservedValues , fixSet , fixSetExtend , fixSet_observed , obsCondKernel , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection , valuesUnionMk
theorem do_rule3 reviewed
Causalean.SCM

Rule 3: insertion/deletion of actions (simplified joint-marginal form). Fix a structural causal model M' and a treatment set Z for which each member's random copy is already observed in M' and each member's fixed copy is not yet among M''s fixed nodes, together with outcome and conditioning sets Y and W, both observed in M'. Suppose no node of Y ∪ W is, in the model intervened on Z, a descendant of the fixed copy of any variable in Z. Then the joint law of (Y, W) under the intervened model, at any post-intervention fixed value, equals the joint law of (Y, W) under the base model M' at the corresponding pre-intervention fixed value.

Formal statement
hypotheses
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
Y W :
Finset (SWIGNode N)
hY :
Y ⊆ M'.observed
hW :
W ⊆ M'.observed
hNoDesc :
∀ v ∈ Y ∪ W, ∀ d ∈ Z, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed d) v
s' :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
conclusion
((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s').map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ union_subset hY hW))
= (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')).map (valuesProjection (union_subset hY hW))
Proof (Lean source)
theorem do_rule3 (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (Y W : Finset (SWIGNode N)) (hY : Y ⊆ M'.observed) (hW : W ⊆ M'.observed) (hNoDesc : ∀ v ∈ Y ∪ W, ∀ d ∈ Z, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed d) v) (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) : ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s').map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ union_subset hY hW)) = (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')).map (valuesProjection (union_subset hY hW)) := SCM.condDistrib_intervention_ancestral_eq M' Z hZ_obs hZ_fixed (Y ∪ W) (union_subset hY hW) (fun z hz v hv => hNoDesc v hv z hz) s'
Causalean.SCM.do_rule3 · Causalean/SCM/Do/DoCalculus.lean:181 · uses isAncestor , SCM , FixedValues , ObservedValues , fixSet , fixSetProj , fixSet_observed , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection
Global­Markov 4 core · 5 supporting This file proves the full global Markov property: d-separation in the causal graph implies conditional independence under the joint distribution over observed and latent variables. ★ full_globalMarkov_with_fixed★ full_globalMarkov

Full Global Markov Property

This file proves the full global Markov property: d-separation in the causal graph implies conditional independence under the joint distribution over observed and latent variables. The result is the full-distribution input from which the observational Markov property is obtained by projection.

The main exported theorem is SCM.full_globalMarkov, with SCM.full_globalMarkov_with_fixed providing the form used by do-calculus proofs where fixed intervention nodes appear in the graphical conditioning set but only random coordinates remain in the probabilistic conditioning set. The file also exposes SCM.reindexSubtypeProj and SCM.indepFun_valuesProjection_latentProduct, the product-measure independence tools used internally by the Markov proof.

def latentAncestorsOfSet reviewed
Causalean.SCM

The latent ancestors of a node set are the unobserved nodes that either belong to the set or are ancestors of one of its nodes.

Definition (Lean source)
noncomputable def latentAncestorsOfSet (M : SCM N Ω) (T : Finset (SWIGNode N)) : Finset (SWIGNode N) := letI : DecidablePred (fun u : SWIGNode N => ∃ v ∈ T, u = v ∨ M.dag.isAncestor u v) := Classical.decPred _ M.unobserved.filter (fun u => ∃ v ∈ T, u = v ∨ M.dag.isAncestor u v)
Causalean.SCM.latentAncestorsOfSet · Causalean/SCM/Do/GlobalMarkov.lean:38 · uses SCM , SWIGNode
def reindexSubtypeProj reviewed
Causalean.SCM

Measurable reindexing equivalence between the coordinate tuple on the subtype-image S.subtype (· ∈ P) of S ⊆ P and the coordinate tuple on S itself. It is the identity on values, only relabelling the index from the doubly-nested subtype to the direct subtype {j // j ∈ S}.

Definition (Lean source)
noncomputable def reindexSubtypeProj {M' : Type*} [DecidableEq M'] [Fintype M'] {Ω' : M' → Type*} [∀ n, MeasurableSpace (Ω' n)] {P : Finset M'} (S : Finset M') (hS : S ⊆ P) : ((i : {i // i ∈ (S.subtype (· ∈ P))}) → Ω' i.val.val) ≃ᵐ ((j : {j // j ∈ S}) → Ω' j.val) where toFun := fun f j => f ⟨⟨j.val, hS j.property⟩, by simp only [Finset.mem_subtype]; exact j.property⟩ invFun := fun g i => g ⟨i.val.val, by have := i.property; rw [Finset.mem_subtype] at this; exact this⟩ left_inv := fun _ => rfl right_inv := fun _ => rfl measurable_toFun := by apply measurable_pi_lambda; intro j; exact measurable_pi_apply _ measurable_invFun := by apply measurable_pi_lambda; intro i; exact measurable_pi_apply _
Causalean.SCM.reindexSubtypeProj · Causalean/SCM/Do/GlobalMarkov.lean:312
theorem full_globalMarkov_with_fixed reviewed
Causalean.SCM

Full Global Markov with fixed-node conditioning shadow. If X, Y, and Z_rand are sets of nodes drawn from the model's random (observed and latent) nodes and Z_fix is a set of the model's fixed (intervened) nodes, and X is d-separated from Y by the union Z_rand ∪ Z_fix in the model's causal graph, then under the joint distribution over all random coordinates at fixed value s, the X-coordinates and the Y-coordinates are conditionally independent given only the Z_rand-coordinates — the fixed nodes contribute to the graphical separation but, since their values are already pinned by s, drop out of the probabilistic conditioning set.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.RandomValues
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
X Y Z_rand Z_fix :
Finset (SWIGNode N)
hX :
X ⊆ M.randomVars
hY :
Y ⊆ M.randomVars
hZ_rand :
Z_rand ⊆ M.randomVars
hZ_fix :
Z_fix ⊆ M.fixed
hdSep :
M.dag.dSep X Y (Z_rand ∪ Z_fix)
s :
M.FixedValues
conclusion
FullCondIndep M X Y Z_rand hX hY hZ_rand (M.jointKernel s)
Proof (Lean source)
theorem full_globalMarkov_with_fixed (M : SCM N Ω) [StandardBorelSpace M.RandomValues] [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] (X Y Z_rand Z_fix : Finset (SWIGNode N)) (hX : X ⊆ M.randomVars) (hY : Y ⊆ M.randomVars) (hZ_rand : Z_rand ⊆ M.randomVars) (hZ_fix : Z_fix ⊆ M.fixed) (hdSep : M.dag.dSep X Y (Z_rand ∪ Z_fix)) (s : M.FixedValues) : FullCondIndep M X Y Z_rand hX hY hZ_rand (M.jointKernel s) := by -- Strong induction on `X` (subset well-founded) with topologically-last selection. revert hX hdSep induction X using Finset.strongInductionOn with | _ X ih => intro hX hdSep have hDisj_XY : Disjoint X Y := hdSep.1 have hDisj_XZ : Disjoint X Z_rand := Disjoint.mono_right Finset.subset_union_left hdSep.2.1 have hDisj_YZ : Disjoint Y Z_rand := Disjoint.mono_right Finset.subset_union_left hdSep.2.2.1 by_cases hempty : X = ∅ · -- Base X = ∅: ∅-projection is constant, so CondIndepFun is trivial. subst hempty unfold FullCondIndep let c : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω) := fun w => absurd w.property (notMem_empty _) have hconst : valuesProjection hX = fun _ => c := by funext ξ w; exact absurd w.property (notMem_empty _) rw [hconst] exact ProbabilityTheory.condIndepFun_const_left c (valuesProjection hY) · -- Inductive step: pick `a ∈ X` with maximal topoOrder. have hne : X.Nonempty := Finset.nonempty_iff_ne_empty.mpr hempty obtain ⟨a, ha_mem, ha_max⟩ : ∃ a ∈ X, ∀ b ∈ X, M.dag.topoOrder b ≤ M.dag.topoOrder a := X.exists_max_image M.dag.topoOrder hne set A' := X.erase a with hA'_def have hA'_ssub : A' ⊂ X := Finset.erase_ssubset ha_mem have hA'_sub : A' ⊆ X := Finset.erase_subset a X have hA' : A' ⊆ M.randomVars := hA'_sub.trans hX have ha_rv : a ∈ M.randomVars := hX ha_mem have hXeq : insert a A' = X := Finset.insert_erase ha_mem -- Topological-max fact: every b ∈ A' is strictly earlier than a. -- This is the ordering input used by the singleton step. have _ha_strict : ∀ b ∈ A', M.dag.topoOrder b < M.dag.topoOrder a := by intro b hb have hbX : b ∈ X := hA'_sub hb have hbne : b ≠ a := Finset.ne_of_mem_erase hb exact lt_of_le_of_ne (ha_max b hbX) (fun h => hbne (M.dag.topoOrder_injective h)) -- Step (i): d-sep monotonicity + IH on A' ⊂ X. have h_A'_dsep : M.dag.dSep A' Y (Z_rand ∪ Z_fix) := DAG.dSep_subset_left M.dag hA'_sub hdSep have hDisj_A'Y : Disjoint A' Y := Disjoint.mono_left hA'_sub hDisj_XY have hDisj_A'Z : Disjoint A' Z_rand := Disjoint.mono_left hA'_sub hDisj_XZ have h_A'_ci : FullCondIndep M A' Y Z_rand hA' hY hZ_rand (M.jointKernel s) := ih A' hA'_ssub hA' h_A'_dsep -- Step (ii): dSep_source_to_cond → dSep {a} Y ((Z_rand ∪ A') ∪ Z_fix). have h_aA'_eq : ({a} ∪ A' : Finset (SWIGNode N)) = X := by rw [Finset.singleton_union]; exact hXeq have h_a_dsep' : M.dag.dSep {a} Y ((Z_rand ∪ Z_fix) ∪ A') := by apply DAG.dSep_source_to_cond M.dag (X := {a}) (S := A') · exact Finset.disjoint_singleton_left.mpr (Finset.notMem_erase a X) · rw [h_aA'_eq]; exact hdSep have h_a_dsep : M.dag.dSep {a} Y ((Z_rand ∪ A') ∪ Z_fix) := by simpa [union_assoc, Finset.union_left_comm, union_comm] using h_a_dsep' -- Derive `{a} ⊥ Y | (Z_rand ∪ A')` from the singleton-source d-sep auxiliary. have h_a_ci : FullCondIndep M {a} Y (Z_rand ∪ A') (Finset.singleton_subset_iff.mpr ha_rv) hY (union_subset hZ_rand hA') (M.jointKernel s) := fullCondIndep_singleton_of_dSep_with_fixed M a Y (Z_rand ∪ A') Z_fix ha_rv hY (union_subset hZ_rand hA') hZ_fix h_a_dsep s -- Step (iii): contraction + symmetry. have h_Y_A' := h_A'_ci.symm have h_Y_a := h_a_ci.symm have h_aA'_rv : ({a} ∪ A') ⊆ M.randomVars := union_subset (Finset.singleton_subset_iff.mpr ha_rv) hA' have h_combined := fullCondIndep_contraction M hY (Finset.singleton_subset_iff.mpr ha_rv) hA' hZ_rand h_Y_a h_Y_A' -- h_combined : Y ⊥ ({a} ∪ A') | Z_rand. Symmetrize and transport `{a} ∪ A' = X`. exact fullCondIndep_congr_left M h_aA'_eq h_combined.symm
Causalean.SCM.full_globalMarkov_with_fixed · Causalean/SCM/Do/GlobalMarkov.lean:640 · uses dSep , SCM , FixedValues , FullCondIndep , RandomValues , instIsMarkovKernelJointKernel , jointKernel , randomVars , SWIGNode , instFintype , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem full_globalMarkov reviewed
Causalean.SCM

Full Global Markov Property. If X, Y, and Z are sets of nodes drawn from the model's random (observed and latent) nodes and X is d-separated from Y by Z in the model's causal graph, then under the joint distribution over all random coordinates at fixed value s, the X-coordinates and the Y-coordinates are conditionally independent given the Z-coordinates.

Formal statement
hypotheses
M :
SCM N Ω
StandardBorelSpace M.RandomValues
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
X Y Z :
Finset (SWIGNode N)
hX :
X ⊆ M.randomVars
hY :
Y ⊆ M.randomVars
hZ :
Z ⊆ M.randomVars
hdSep :
M.dag.dSep X Y Z
s :
M.FixedValues
conclusion
FullCondIndep M X Y Z hX hY hZ (M.jointKernel s)
Proof (Lean source)
theorem full_globalMarkov (M : SCM N Ω) [StandardBorelSpace M.RandomValues] [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] (X Y Z : Finset (SWIGNode N)) (hX : X ⊆ M.randomVars) (hY : Y ⊆ M.randomVars) (hZ : Z ⊆ M.randomVars) (hdSep : M.dag.dSep X Y Z) (s : M.FixedValues) : FullCondIndep M X Y Z hX hY hZ (M.jointKernel s) := by simpa using (full_globalMarkov_with_fixed M X Y Z ∅ hX hY hZ (empty_subset _) (by simpa using hdSep) s)
Causalean.SCM.full_globalMarkov · Causalean/SCM/Do/GlobalMarkov.lean:753 · uses dSep , SCM , FixedValues , FullCondIndep , RandomValues , instIsMarkovKernelJointKernel , jointKernel , randomVars , SWIGNode , instFintype , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
5 supporting declarations (lemmas, instances)
Obs­Markov 2 core · 1 supporting This file transfers conditional independence from the full distribution over random and latent coordinates to the observational distribution over observed coordinates. ★ globalMarkov★ globalMarkov_with_fixed

Observational Markov Property

This file transfers conditional independence from the full distribution over random and latent coordinates to the observational distribution over observed coordinates. It then packages graphical separation hypotheses as observational conditional independences for use in do-calculus arguments.

theorem globalMarkov reviewed
Causalean.SCM

Global Markov Property. If X, Y, and Z are sets of observed nodes and X is d-separated from Y by Z in the model's full causal graph, which also includes any latent nodes, then under the observational distribution — the law of the observed coordinates alone, at fixed value s — the X-coordinates and Y-coordinates are conditionally independent given the Z-coordinates.

Formal statement
hypotheses
M :
SCM N Ω
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
X Y Z :
Finset (SWIGNode N)
StandardBorelSpace (ValuesOn X (swigΩ Ω))
Nonempty (ValuesOn X (swigΩ Ω))
StandardBorelSpace (ValuesOn Y (swigΩ Ω))
Nonempty (ValuesOn Y (swigΩ Ω))
hX :
X ⊆ M.observed
hY :
Y ⊆ M.observed
hZ :
Z ⊆ M.observed
hdSep :
M.dag.dSep X Y Z
s :
M.FixedValues
conclusion
ObsCondIndep M X Y Z hX hY hZ (M.obsKernel s)
Proof (Lean source)
theorem globalMarkov (M : SCM N Ω) [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] (X Y Z : Finset (SWIGNode N)) [StandardBorelSpace (ValuesOn X (swigΩ Ω))] [Nonempty (ValuesOn X (swigΩ Ω))] [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] (hX : X ⊆ M.observed) (hY : Y ⊆ M.observed) (hZ : Z ⊆ M.observed) (hdSep : M.dag.dSep X Y Z) (s : M.FixedValues) : ObsCondIndep M X Y Z hX hY hZ (M.obsKernel s) := by -- Stage 1: full global Markov at full distribution level have hfull := full_globalMarkov M X Y Z (hX.trans (observed_subset_randomVars M)) (hY.trans (observed_subset_randomVars M)) (hZ.trans (observed_subset_randomVars M)) hdSep s -- Stage 2: project to observational level exact obs_condIndep_of_full M hX hY hZ s hfull
Causalean.SCM.globalMarkov · Causalean/SCM/Do/ObsMarkov.lean:96 · uses dSep , SCM , FixedValues , ObsCondIndep , ObservedValues , instIsMarkovKernelObsKernel , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
theorem globalMarkov_with_fixed reviewed
Causalean.SCM

Global Markov with fixed-node conditioning. If X, Y, and Z_obs are sets of observed nodes and Z_fix is a set of the model's fixed (intervened) nodes, and X is d-separated from Y by the union Z_obs ∪ Z_fix in the model's full causal graph, then under the observational distribution at fixed value s, the X-coordinates and Y-coordinates are conditionally independent given only the Z_obs-coordinates — the fixed nodes contribute to the graphical separation but, since their values are already pinned by s, drop out of the probabilistic conditioning set.

Formal statement
hypotheses
M :
SCM N Ω
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
X Y Z_obs Z_fix :
Finset (SWIGNode N)
StandardBorelSpace (ValuesOn X (swigΩ Ω))
Nonempty (ValuesOn X (swigΩ Ω))
StandardBorelSpace (ValuesOn Y (swigΩ Ω))
Nonempty (ValuesOn Y (swigΩ Ω))
hX :
X ⊆ M.observed
hY :
Y ⊆ M.observed
hZ_obs :
Z_obs ⊆ M.observed
hZ_fix :
Z_fix ⊆ M.fixed
hdSep :
M.dag.dSep X Y (Z_obs ∪ Z_fix)
s :
M.FixedValues
conclusion
ObsCondIndep M X Y Z_obs hX hY hZ_obs (M.obsKernel s)
Proof (Lean source)
theorem globalMarkov_with_fixed (M : SCM N Ω) [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] (X Y Z_obs Z_fix : Finset (SWIGNode N)) [StandardBorelSpace (ValuesOn X (swigΩ Ω))] [Nonempty (ValuesOn X (swigΩ Ω))] [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] (hX : X ⊆ M.observed) (hY : Y ⊆ M.observed) (hZ_obs : Z_obs ⊆ M.observed) (hZ_fix : Z_fix ⊆ M.fixed) (hdSep : M.dag.dSep X Y (Z_obs ∪ Z_fix)) (s : M.FixedValues) : ObsCondIndep M X Y Z_obs hX hY hZ_obs (M.obsKernel s) := by have hDisj_XY : Disjoint X Y := hdSep.1 have hDisj_XZ : Disjoint X Z_obs := Disjoint.mono_right Finset.subset_union_left hdSep.2.1 have hDisj_YZ : Disjoint Y Z_obs := Disjoint.mono_right Finset.subset_union_left hdSep.2.2.1 have hfull := full_globalMarkov_with_fixed M X Y Z_obs Z_fix (hX.trans (observed_subset_randomVars M)) (hY.trans (observed_subset_randomVars M)) (hZ_obs.trans (observed_subset_randomVars M)) hZ_fix hdSep s exact obs_condIndep_of_full M hX hY hZ_obs s hfull
Causalean.SCM.globalMarkov_with_fixed · Causalean/SCM/Do/ObsMarkov.lean:125 · uses dSep , SCM , FixedValues , ObsCondIndep , ObservedValues , instIsMarkovKernelObsKernel , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ
1 supporting declaration (lemmas, instances)
Rule2­AE 1 core · 1 supporting The retired pointwise Rule 2 form quantified a.e. ★ obsCondKernel_fixSet_eq_ae_witness

Rule 2, a.e. in the treatment value (product form + positivity)

The retired pointwise Rule 2 form quantified a.e. in the conditioning value w but pointwise in the treatment value (the Z.random do-value spliced via fillZrW). For non-atomic treatment that point lies on a μ_C-null slice where Mathlib's obsCondKernel representative is unpinned, so the pointwise form is too strong.

The honest generalization quantifies a.e. over the product νZ ⊗ₘ μW of the observational treatment marginal νZ := (M'.obsKernel s0).map π_{Zr} and conditioning marginal μW := (M'.obsKernel s0).map π_W, under a positivity hypothesis (νZ ⊗ₘ μW) ∘ fill⁻¹ ≪ μ_C. Both regimes are covered: atomic νZ makes "a.e." pointwise on the support.

Why the product (not the joint μ_C): the do-side (M'.fixSet Z).obsCondKernel Y W is pinned only under the do-model W-marginal (= μW via Rule 3), i.e. under the product; the obs-side M'.obsCondKernel is pinned under μ_C. Positivity (product ≪ μ_C) lifts the obs-side onto the product, where the do-side is natively pinned. The proof lifts the discrete d-sep collapse and cross-SCM bridge (obsCondKernel_dSep_collapse_ae, obsCondKernel_cross_SCM_ae_eq_on_fillZrW, obsKernel_fixSet_W_marginal_eq_M1_marginal) from the per-treatment slice to the product via Fubini over the treatment + the product↔joint AC transfer.

theorem obsCondKernel_fixSet_eq_ae_witness reviewed
Causalean.SCM

Rule 2, a.e. in the treatment value (product form + positivity). Consider intervening on the finite set of names Z, where each name's random copy is already observed in the base model and its fixed copy is not yet part of the base model's fixed coordinates, with outcome set Y and conditioning set W contained in the observed variables, together with the random copies of Z and their union with W. Assume in the post-intervention SWIG DAG, Y is d-separated from the random copies of Z given W together with the post-intervention fixed set, no fixed copy of a name in Z is an ancestor of any node of W in the post-intervention DAG, no random copy of a name in Z is an ancestor of any node of W in the original DAG, and positivity: the pushforward of the product of the treatment and conditioning marginals under the fill map is absolutely continuous with respect to the base model's law on Z.random ∪ W. Then for almost every pair (t, w) under that product measure, the W-conditional kernel of the model intervened at treatment value t, evaluated together with w, restricted to Y, equals the base model's conditional distribution of Y given Z.random ∪ W evaluated at the combined point (t, w).

Formal statement
hypotheses
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
Y W :
Finset (SWIGNode N)
hY :
Y ⊆ M'.observed
hW :
W ⊆ M'.observed
hZr :
Z.image SWIGNode.random ⊆ M'.observed
hZrW :
Z.image SWIGNode.random ∪ W ⊆ M'.observed
hdSep :
(M'.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M'.fixSet Z hZ_obs hZ_fixed).fixed)
hWNonDesc :
∀ z ∈ Z, ∀ v ∈ W, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v
hWNonDescM1 :
∀ D ∈ Z, ∀ w ∈ W, ¬ M'.dag.isAncestor (SWIGNode.random D) w
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
CountableOrCountablyGenerated M'.FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))
MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
s0 :
M'.FixedValues
hPositivity_ae :
(((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M'.obsKernel s0).map (valuesProjection hZrW))
conclusion
∀ᵐ p ∂((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ const _ ((M'.obsKernel s0).map (valuesProjection hW))),
(M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (M'.fixSetExtend Z hZ_obs hZ_fixed s0 p.1, p.2)
= M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, valuesUnionMk p.1 p.2)
Proof (Lean source)
theorem obsCondKernel_fixSet_eq_ae_witness (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (Y W : Finset (SWIGNode N)) (hY : Y ⊆ M'.observed) (hW : W ⊆ M'.observed) (hZr : Z.image SWIGNode.random ⊆ M'.observed) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) (hdSep : (M'.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M'.fixSet Z hZ_obs hZ_fixed).fixed)) (hWNonDesc : ∀ z ∈ Z, ∀ v ∈ W, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v) (hWNonDescM1 : ∀ D ∈ Z, ∀ w ∈ W, ¬ M'.dag.isAncestor (SWIGNode.random D) w) [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] [CountableOrCountablyGenerated M'.FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))] [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s0 : M'.FixedValues) (hPositivity_ae : (((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ ProbabilityTheory.Kernel.const _ ((M'.obsKernel s0).map (valuesProjection hW))).map (fun p => valuesUnionMk p.1 p.2)) ≪ ((M'.obsKernel s0).map (valuesProjection hZrW))) : ∀ᵐ p ∂((M'.obsKernel s0).map (valuesProjection hZr) ⊗ₘ ProbabilityTheory.Kernel.const _ ((M'.obsKernel s0).map (valuesProjection hW))), (M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (M'.fixSetExtend Z hZ_obs hZ_fixed s0 p.1, p.2) = M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, valuesUnionMk p.1 p.2) := by have hDisj_YZr : Disjoint Y (Z.image SWIGNode.random) := hdSep.1 have hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W := Disjoint.mono_right subset_union_left hdSep.2.2.1 -- Abbreviations matching the statement. set M2 := M'.fixSet Z hZ_obs hZ_fixed with hM2 set sT := fun t => M'.fixSetExtend Z hZ_obs hZ_fixed s0 t with hsT -- Transported subset proofs for the do-model M2. set hY_M2 : Y ⊆ M2.observed := (SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY with hhY_M2 set hW_M2 : W ⊆ M2.observed := (SCM.fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW with hhW_M2 -- The product measure λ = νZ ⊗ₘ const μW and the fill map G. set νZ := (M'.obsKernel s0).map (valuesProjection hZr) with hνZ set μW := (M'.obsKernel s0).map (valuesProjection hW) with hμW set lam := νZ ⊗ₘ ProbabilityTheory.Kernel.const _ μW with hlam set G : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω) → ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) := fun p => valuesUnionMk p.1 p.2 with hG have hG_meas : Measurable G := measurable_valuesUnionMk -- Obs-side: pin M1's `obsCondKernel` to `condDistrib`, then transport from -- μC onto λ via positivity. have h_obs_cd := obsCondKernel_ae_eq_condDistrib M' Y (Z.image SWIGNode.random ∪ W) hY hZrW s0 -- `λ.map G ≪ μC`, where `μC` is the measure `h_obs_cd` is a.e. for. have h_obs_ae_mapG : (fun c => M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, c)) =ᵐ[lam.map G] condDistrib (valuesProjection hY) (valuesProjection hZrW) (M'.obsKernel s0) := MeasureTheory.Measure.AbsolutelyContinuous.ae_eq hPositivity_ae h_obs_cd have h_obs_prod : ∀ᵐ p ∂lam, M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (s0, G p) = condDistrib (valuesProjection hY) (valuesProjection hZrW) (M'.obsKernel s0) (G p) := MeasureTheory.ae_of_ae_map hG_meas.aemeasurable h_obs_ae_mapG -- The isolated hard bridge: do-side `obsCondKernel` = obs-side `condDistrib`, joint-a.e. have h_bridge := condDistrib_fixSet_cross_SCM_bridge M' Z hZ_obs hZ_fixed Y W hY hW hZr hZrW hdSep hWNonDesc hWNonDescM1 s0 hPositivity_ae -- Assemble: do-side =[bridge] obs `condDistrib` =[obs, reversed] M1.obsCondKernel. filter_upwards [h_obs_prod, h_bridge] with p hobs hbr rw [hbr, ← hobs]
Causalean.SCM.obsCondKernel_fixSet_eq_ae_witness · Causalean/SCM/Do/Rule2AE.lean:139 · uses dSep , isAncestor , SCM , FixedValues , ObservedValues , fixSet , fixSetExtend , fixSet_observed , obsCondKernel , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection , valuesUnionMk
1 supporting declaration (lemmas, instances)
Rule3 1 core · 4 supporting This file proves the kernel-level form of Rule 3 of do-calculus for structural causal models. ★ condDistrib_intervention_ancestral_eq

Rule 3 Kernel Identity

This file proves the kernel-level form of Rule 3 of do-calculus for structural causal models. The transport theorem fixSet_latentProduct_compat identifies the latent-product measure before and after an additional intervention, fixSet_evalMap_nonAnc_compat proves pointwise agreement of evaluation at nodes with no fixed-intervention ancestors, and condDistrib_intervention_ancestral_eq packages these facts as equality of observed marginal kernels for targets not descended from the added intervention nodes.

theorem condDistrib_intervention_ancestral_eq reviewed
Causalean.SCM

Rule 3 core — intervention on non-ancestors of T is irrelevant (Option B in the design; covers the simplified Z_Y = Z case of the tex's Rule 3, sufficient for backdoor / frontdoor demos). Fix a do-set Z of nodes whose random copies are observed in the base model and whose fixed nodes have not already been intervened on and a target block T of observed variables. If none of the fixed copies of Z's nodes is an ancestor, in the intervention SWIG graph, of any node in T, then the T-marginal law of the intervened model equals the T-marginal law of the base model evaluated at the corresponding fixed values.

Formal statement
hypotheses
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
T :
Finset (SWIGNode N)
hT :
T ⊆ M'.observed
hNoDesc :
∀ z ∈ Z, ∀ v ∈ T, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v
s' :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
conclusion
((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s').map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hT))
= (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')).map (valuesProjection hT)
Proof (Lean source)
theorem condDistrib_intervention_ancestral_eq (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (T : Finset (SWIGNode N)) (hT : T ⊆ M'.observed) (hNoDesc : ∀ z ∈ Z, ∀ v ∈ T, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v) (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) : ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s').map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hT)) = (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')).map (valuesProjection hT) := by classical -- Measurability bookkeeping. have hf_2 : Measurable (fun ℓ : LatentValues (M'.fixSet Z hZ_obs hZ_fixed) => (M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ) := (M'.fixSet Z hZ_obs hZ_fixed).evalMap_measurable.comp (prodMk measurable_const measurable_id) have hf_1 : Measurable (fun ℓ : LatentValues M' => M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') ℓ) := M'.evalMap_measurable.comp (prodMk measurable_const measurable_id) have hRTO_2 : Measurable (M'.fixSet Z hZ_obs hZ_fixed).randomToObserved := (M'.fixSet Z hZ_obs hZ_fixed).measurable_randomToObserved have hRTO_1 : Measurable M'.randomToObserved := M'.measurable_randomToObserved have hπ_2 : Measurable (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hT) : ObservedValues (M'.fixSet Z hZ_obs hZ_fixed) → ValuesOn T (swigΩ Ω)) := measurable_valuesProjection _ have hπ_1 : Measurable (valuesProjection hT : ObservedValues M' → ValuesOn T (swigΩ Ω)) := measurable_valuesProjection _ -- Step 1: unfold `obsKernel` and `jointKernel` to expose the latent push-forwards. unfold obsKernel rw [ProbabilityTheory.Kernel.map_apply _ hRTO_2, ProbabilityTheory.Kernel.map_apply _ hRTO_1, jointKernel_apply_eq (M'.fixSet Z hZ_obs hZ_fixed) s', jointKernel_apply_eq M' (M'.fixSetProj Z hZ_obs hZ_fixed s')] -- Step 2: compose the three nested `Measure.map`s on each side. rw [MeasureTheory.Measure.map_map hRTO_2 hf_2, MeasureTheory.Measure.map_map hπ_2 (hRTO_2.comp hf_2), MeasureTheory.Measure.map_map hRTO_1 hf_1, MeasureTheory.Measure.map_map hπ_1 (hRTO_1.comp hf_1)] -- Step 3: bridge the source measures via `fixSet_latentProduct_compat` -- (the `M2.latentProduct → M'.latentProduct` cast through `valuesProjection`). -- This converts the RHS `M'.latentProduct.map G_1` into -- `M2.latentProduct.map (G_1 ∘ cast)`, aligning both sides to the same source. have hcast : Measurable (valuesProjection (le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm) : LatentValues (M'.fixSet Z hZ_obs hZ_fixed) → LatentValues M') := measurable_valuesProjection _ rw [← fixSet_latentProduct_compat M' Z hZ_obs hZ_fixed, MeasureTheory.Measure.map_map (hπ_1.comp (hRTO_1.comp hf_1)) hcast] -- Step 4: both sides are `M2.latentProduct.map (...)`; reduce to pointwise -- equality of the composed pushforward functions. congr 1 funext ℓ simp only [Function.comp_apply] funext v simp only [randomToObserved, valuesProjection] -- Step 5: pointwise discharge via the cross-SCM evalMap bridge. exact fixSet_evalMap_nonAnc_compat M' Z hZ_obs hZ_fixed s' ℓ ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hT v.property) (fun z hz => hNoDesc z hz v.val v.property)
Causalean.SCM.condDistrib_intervention_ancestral_eq · Causalean/SCM/Do/Rule3.lean:338 · uses isAncestor , SCM , FixedValues , ObservedValues , fixSet , fixSetProj , fixSet_observed , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection
4 supporting declarations (lemmas, instances)
  • fixSet_latentProduct_compat theorem — Cross-SCM latent-product transport for Rule 3.
    hypotheses
    M' :
    SCM N Ω
    Z :
    Finset N
    hZ_obs :
    ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
    hZ_fixed :
    ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
    conclusion
    ((M'.fixSet Z hZ_obs hZ_fixed).latentProduct).map (valuesProjection (le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm))
    = M'.latentProduct
    Proof (Lean source)
    theorem fixSet_latentProduct_compat (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) : ((M'.fixSet Z hZ_obs hZ_fixed).latentProduct).map (valuesProjection (le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm)) = M'.latentProduct := by set M2 := M'.fixSet Z hZ_obs hZ_fixed with hM2 have h_unobs : M2.unobserved = M'.unobserved := fixSet_unobserved M' Z hZ_obs hZ_fixed -- Under the monolithic `fixSet := fixMono`, `M2.unobserved = M'.unobserved` by -- `rfl` and `M2.latentDist = M'.latentDist` pointwise by `rfl`. So the -- `valuesProjection`-transport across the identity type-equality is the -- identity, and the measure identity reduces to `rfl` on `Measure.pi`. change (M2.latentProduct).map (valuesEquivOfEq (Ω := swigΩ Ω) h_unobs) = M'.latentProduct unfold latentProduct letI := M2.isProbability_latent letI := M'.isProbability_latent rw [(measurePreserving_valuesEquivOfEq (Ω := swigΩ Ω) h_unobs (fun u => M2.latentDist u)).map_eq] congr 1
    Causalean.SCM.fixSet_latentProduct_compat · Causalean/SCM/Do/Rule3.lean:30
  • hNoDesc_implies_no_fixed_parent lemma — If none of the fixed intervention nodes is an ancestor of a node, none is a parent of that node.
    hypotheses
    M2 :
    SCM N Ω
    Z :
    Finset N
    v :
    SWIGNode N
    hNoDesc :
    ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) v
    conclusion
    ∀ z ∈ Z, SWIGNode.fixed z ∉ M2.dag.parents v
    Proof (Lean source)
    lemma hNoDesc_implies_no_fixed_parent {M2 : SCM N Ω} {Z : Finset N} {v : SWIGNode N} (hNoDesc : ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) v) : ∀ z ∈ Z, SWIGNode.fixed z ∉ M2.dag.parents v := fun z hz hP => hNoDesc z hz (DAG.isAncestor.edge (M2.dag.mem_parents.mp hP))
    Causalean.SCM.hNoDesc_implies_no_fixed_parent · Causalean/SCM/Do/Rule3.lean:72
  • hNoDesc_descend_to_parent lemma — If none of the fixed intervention nodes is an ancestor of a node, then none is an ancestor of any parent of that node.
    hypotheses
    M2 :
    SCM N Ω
    Z :
    Finset N
    v w :
    SWIGNode N
    hwP :
    w ∈ M2.dag.parents v
    hNoDesc :
    ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) v
    conclusion
    ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) w
    Proof (Lean source)
    lemma hNoDesc_descend_to_parent {M2 : SCM N Ω} {Z : Finset N} {v w : SWIGNode N} (hwP : w ∈ M2.dag.parents v) (hNoDesc : ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) v) : ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) w := fun z hz hanc => hNoDesc z hz (DAG.isAncestor.trans hanc (M2.dag.mem_parents.mp hwP))
    Causalean.SCM.hNoDesc_descend_to_parent · Causalean/SCM/Do/Rule3.lean:80
  • fixSet_evalMap_nonAnc_compat theorem — Cross-SCM evalMap bridge for Rule 3.
    hypotheses
    M' :
    SCM N Ω
    Z :
    Finset N
    hZ_obs :
    ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
    hZ_fixed :
    ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
    s' :
    (M'.fixSet Z hZ_obs hZ_fixed).FixedValues
    ℓ :
    (M'.fixSet Z hZ_obs hZ_fixed).LatentValues
    v :
    SWIGNode N
    hv :
    v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed
    hNoDesc :
    ∀ z ∈ Z, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v
    conclusion
    (M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ ⟨v, mem_union_left _ hv⟩
    = M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') (valuesProjection (le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm) ℓ) ⟨v, mem_union_left _ (le_of_eq (fixSet_observed M' Z hZ_obs hZ_fixed) hv)⟩
    Proof (Lean source)
    theorem fixSet_evalMap_nonAnc_compat (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) (ℓ : (M'.fixSet Z hZ_obs hZ_fixed).LatentValues) {v : SWIGNode N} (hv : v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed) (hNoDesc : ∀ z ∈ Z, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed z) v) : (M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ ⟨v, mem_union_left _ hv⟩ = M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') (valuesProjection (le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm) ℓ) ⟨v, mem_union_left _ (le_of_eq (fixSet_observed M' Z hZ_obs hZ_fixed) hv)⟩ := by classical -- Abbreviations (via `let` to avoid `set`'s hypothesis-shadowing behaviour -- on dependent arguments). let M2 := M'.fixSet Z hZ_obs hZ_fixed have h_obs_eq : M2.observed = M'.observed := rfl have h_unobs : M2.unobserved = M'.unobserved := rfl let s_M1 : M'.FixedValues := M'.fixSetProj Z hZ_obs hZ_fixed s' let ℓ_M1 : M'.LatentValues := valuesProjection (le_of_eq h_unobs.symm) ℓ -- Strong recursion on `M2.observedIndex ⟨v, hv⟩`, with the no-ancestor -- hypothesis carried through the recursion. Under the monolithic -- `fixSet := fixMono`, `M2.observed = M'.observed` and `M2.unobserved = -- M'.unobserved` hold by `rfl`, so the coercions in the goal are identities. suffices h_obs : ∀ (n : ℕ) (w : SWIGNode N) (hw : w ∈ M2.observed) (_hNoD : ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) w), (M2.observedIndex ⟨w, hw⟩).val = n → M2.evalMap s' ℓ ⟨w, mem_union_left _ hw⟩ = M'.evalMap s_M1 ℓ_M1 ⟨w, mem_union_left _ hw⟩ by exact h_obs _ v hv hNoDesc rfl intro n induction n using Nat.strongRecOn with | _ n ih => intro v hv hNoD hidx -- No `.fixed D` (D ∈ Z) is a parent of v in M2 (contrapositive of hNoD). have hNoFP : ∀ D ∈ Z, SWIGNode.fixed D ∉ M2.dag.parents v := fun D hD hP => hNoD D hD (DAG.isAncestor.edge (M2.dag.mem_parents.mp hP)) have h_parents_eq : M2.dag.parents v = M'.dag.parents v := fixSet_parents_eq_of_no_fixed_parent M' Z hZ_obs hZ_fixed hNoFP have hv_M1 : v ∈ M'.observed := hv -- Unfold both `evalMap`s via `evalMap_observed_unfold`. rw [SCM.evalMap_observed_unfold M2 s' ℓ ⟨v, hv⟩, SCM.evalMap_observed_unfold M' s_M1 ℓ_M1 ⟨v, hv_M1⟩] -- LHS's outer `M2.structFun ⟨v, hv⟩` is definitionally -- `M'.structFun ⟨v, hv_M1⟩` precomposed with `fixMonoParentMap`. -- After `congr 1`, the goal reduces to pointwise equality of the two -- parent tuples over `M'.dag.parents v`. change M'.structFun ⟨v, hv_M1⟩ (fixMonoParentMap M'.toSWIGGraph Z hZ_obs hZ_fixed v (fun w : {w // w ∈ (M'.splitMono Z hZ_obs hZ_fixed).dag.parents v} => if huo : w.val ∈ M2.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M2.fixed then s' ⟨w.val, hfix⟩ else have hedge : M2.dag.edge w.val v := M2.dag.mem_parents.mp w.property have hobs : w.val ∈ M2.observed := by rcases Finset.mem_union.mp (M2.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo M2.evalMap s' ℓ ⟨w.val, mem_union_left _ hobs⟩)) = M'.structFun ⟨v, hv_M1⟩ (fun w : {w // w ∈ M'.dag.parents v} => if huo : w.val ∈ M'.unobserved then ℓ_M1 ⟨w.val, huo⟩ else if hfix : w.val ∈ M'.fixed then s_M1 ⟨w.val, hfix⟩ else have hedge : M'.dag.edge w.val v := M'.dag.mem_parents.mp w.property have hobs : w.val ∈ M'.observed := by rcases Finset.mem_union.mp (M'.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo M'.evalMap s_M1 ℓ_M1 ⟨w.val, mem_union_left _ hobs⟩) congr 1 -- Pointwise equality of the two parent tuples. funext w -- Bridge: w : {w // w ∈ M'.dag.parents v}, and the LHS tuple is indexed -- by `M'.dag.parents v` too (output of `fixMonoParentMap`). On the LHS, -- unfold `fixMonoParentMap` according to w.val's constructor. have hNoRD : ∀ D ∈ Z, SWIGNode.random D ∉ M'.dag.parents v := by intro D hD hRD apply hNoFP D hD have hP_M2 := (SWIGGraph.splitMono_parents_char M'.toSWIGGraph Z hZ_obs hZ_fixed v (SWIGNode.fixed D)).2 (inr ⟨D, hD, rfl, hRD⟩) exact hP_M2 -- Per-parent three-way case split on `w.val`. rcases w with ⟨wVal, hwVal_M1⟩ -- wVal's position in the LHS (fixMonoParentMap) depends on its form. have hwVal_M2 : wVal ∈ M2.dag.parents v := h_parents_eq.symm ▸ hwVal_M1 -- Compute the LHS at wVal. cases wVal with | random u => have hu_notZ : u ∉ Z := by intro hu exact hNoRD u hu hwVal_M1 -- fixMonoParentMap at ⟨.random u, hwVal_M1⟩ with u ∉ Z: -- reads the ξ at ⟨.random u, (splitMono_parents_char …).2 (inl …)⟩. rw [fixMonoParentMap_apply_random_notMem M'.toSWIGGraph Z hZ_obs hZ_fixed v _ u hu_notZ hwVal_M1] -- Now both sides are `if-elif-else` on wVal = .random u. -- M2.unobserved = M'.unobserved (rfl), M2.fixed = M'.fixed ∪ Z.image .fixed. -- For .random u, it is never in Z.image .fixed, so being in M2.fixed iff M'.fixed. by_cases huo : (SWIGNode.random u : SWIGNode N) ∈ M'.unobserved · have huo_M2 : SWIGNode.random u ∈ M2.unobserved := huo simp only [dif_pos huo, dif_pos huo_M2] -- ℓ_M1 at ⟨.random u, huo⟩ = ℓ at ⟨.random u, huo_M2⟩ since -- ℓ_M1 := valuesProjection (le_of_eq rfl.symm) ℓ = (by rfl) ℓ. rfl · have huo_M2 : SWIGNode.random u ∉ M2.unobserved := huo simp only [dif_neg huo, dif_neg huo_M2] by_cases hfix : (SWIGNode.random u : SWIGNode N) ∈ M'.fixed · -- .random u ∈ M'.fixed — impossible since M'.fixed elements are .fixed nodes. exfalso rcases M'.fixed_is_fixed _ hfix with ⟨_, hfix_eq⟩ cases hfix_eq · have hfix_M2 : (SWIGNode.random u : SWIGNode N) ∉ M2.fixed := by intro h have : (SWIGNode.random u : SWIGNode N) ∈ M'.fixed ∪ Z.image SWIGNode.fixed := h rcases Finset.mem_union.mp this with h1 | h2 · exact hfix h1 · rcases Finset.mem_image.mp h2 with ⟨_, _, hEq⟩ cases hEq simp only [dif_neg hfix, dif_neg hfix_M2] -- Observed case: apply IH. -- Need to derive `M2.observedIndex ⟨.random u, hobs_M2⟩ < n`. have hobs_M1 : (SWIGNode.random u : SWIGNode N) ∈ M'.observed := by have hedge_M1 : M'.dag.edge (SWIGNode.random u) v := M'.dag.mem_parents.mp hwVal_M1 rcases Finset.mem_union.mp (M'.dag_edges_classified _ _ hedge_M1).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo have hobs_M2 : (SWIGNode.random u : SWIGNode N) ∈ M2.observed := hobs_M1 -- IH on w. have hNoD_w : ∀ z ∈ Z, ¬ M2.dag.isAncestor (SWIGNode.fixed z) (SWIGNode.random u) := by intro z hz hanc exact hNoD z hz (DAG.isAncestor.trans hanc (M2.dag.mem_parents.mp hwVal_M2)) have hidx_w : (M2.observedIndex ⟨SWIGNode.random u, hobs_M2⟩).val < (M2.observedIndex ⟨v, hv⟩).val := by have hedge_M2 : M2.dag.edge (SWIGNode.random u) v := M2.dag.mem_parents.mp hwVal_M2 have hv_eq : (M2.observedAt ⟨(M2.observedIndex ⟨v, hv⟩).val, (M2.observedIndex ⟨v, hv⟩).isLt⟩).val = v := by have := M2.observedAt_observedIndex ⟨v, hv⟩ convert this have hedge_M2' : M2.dag.edge (SWIGNode.random u) (M2.observedAt ⟨(M2.observedIndex ⟨v, hv⟩).val, (M2.observedIndex ⟨v, hv⟩).isLt⟩).val := by rw [hv_eq]; exact hedge_M2 exact M2.observed_parent_index_lt (M2.observedIndex ⟨v, hv⟩).isLt hedge_M2' hobs_M2 rw [hidx] at hidx_w exact ih _ hidx_w (SWIGNode.random u) hobs_M2 hNoD_w rfl | fixed d => -- fixMonoParentMap at ⟨.fixed d, hwVal_M1⟩: copies ξ at ⟨.fixed d, _⟩. rw [fixMonoParentMap_apply_fixed M'.toSWIGGraph Z hZ_obs hZ_fixed v _ d hwVal_M1] -- Both sides: .fixed d. Unobserved case: impossible (unobserved elts are .random). have huo : (SWIGNode.fixed d : SWIGNode N) ∉ M'.unobserved := by intro h rcases M'.unobserved_is_random _ h with ⟨_, hEq⟩ cases hEq have huo_M2 : (SWIGNode.fixed d : SWIGNode N) ∉ M2.unobserved := huo simp only [dif_neg huo, dif_neg huo_M2] -- Fixed case: .fixed d ∈ M'.fixed iff .fixed d ∈ M2.fixed (if d ∉ Z) -- or d ∈ Z (then .fixed d ∈ M2.fixed but may or may not be in M'.fixed). by_cases hfix_M1 : (SWIGNode.fixed d : SWIGNode N) ∈ M'.fixed · have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∈ M2.fixed := by change _ ∈ M'.fixed ∪ Z.image SWIGNode.fixed exact mem_union_left _ hfix_M1 simp only [dif_pos hfix_M1, dif_pos hfix_M2] -- s_M1 := fixSetProj s' = valuesProjection (fixSet_fixed_subset) s'. -- So s_M1 ⟨.fixed d, hfix_M1⟩ = s' ⟨.fixed d, fixSet_fixed_subset hfix_M1⟩ -- = s' ⟨.fixed d, hfix_M2⟩ (by proof irrelevance). rfl · -- .fixed d ∉ M'.fixed. Is it in M2.fixed? Only if d ∈ Z. by_cases hd_Z : d ∈ Z · -- .fixed d ∈ M2.fixed via Z.image. -- But wait — .fixed d being a parent of v in M'.dag would need d ∈ M'.fixed -- (since fixed nodes outside M'.fixed are isolated). exfalso have := M'.fixed_outside_fixed_isolated d hfix_M1 have hCh : v ∈ M'.dag.children (SWIGNode.fixed d) := M'.dag.mem_children.mpr (M'.dag.mem_parents.mp hwVal_M1) simp [this.2] at hCh · have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∉ M2.fixed := by intro h rcases Finset.mem_union.mp (show _ ∈ M'.fixed ∪ Z.image SWIGNode.fixed from h) with h1 | h2 · exact hfix_M1 h1 · rcases Finset.mem_image.mp h2 with ⟨d', hd'Z, hEq⟩ have : d = d' := SWIGNode.fixed.inj hEq.symm exact hd_Z (this ▸ hd'Z) simp only [dif_neg hfix_M1, dif_neg hfix_M2] -- Observed case — but `.fixed d ∉ M'.observed` since observed elts are .random. exfalso have hobs : (SWIGNode.fixed d : SWIGNode N) ∈ M'.observed := by have hedge_M1 : M'.dag.edge (SWIGNode.fixed d) v := M'.dag.mem_parents.mp hwVal_M1 rcases Finset.mem_union.mp (M'.dag_edges_classified _ _ hedge_M1).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix_M1 · exact hob · exact absurd h2 huo rcases M'.observed_is_random _ hobs with ⟨_, hEq⟩ cases hEq
    Causalean.SCM.fixSet_evalMap_nonAnc_compat · Causalean/SCM/Do/Rule3.lean:91
Rule3­Conditional 1 core · 4 supporting The joint-marginal Rule 3\* (do_rule3 / condDistrib_intervention_ancestral_eq) transports the *joint* law of an ancestrally-blocked outcome block across an intervention. ★ do_rule3_conditional

Conditional Rule 3 of do-Calculus (a.e. obsCondKernel form)

The joint-marginal Rule 3\* (do_rule3 / condDistrib_intervention_ancestral_eq) transports the joint law of an ancestrally-blocked outcome block across an intervention. This file upgrades it to the conditional Rule 3 — Pearl's p(Y | do(z), W) = p(Y | W) — in the honest almost-everywhere form, matching the style of do_rule2_kernel.

The mathematical content is a single disintegration fact: condDistrib depends only on the joint pushforward μ.map (X, Y), and Rule 3\* makes the two joint pushforwards (under do(Z) and under the base model) literally equal on the target/conditioning block. No positivity or ratio infrastructure is required because there is no do-side pinning here (unlike Rule 2); the intervention only transports a marginal.

Main declarations

  • condDistrib_eq_of_map_prod_eq — generic: equal joint pushforwards ⇒ equal condDistrib.
  • obsKernel_map_prodWY_eq — Rule 3\* specialized to the (W, Y) joint pushforward.
  • obsKernel_map_W_eq — Rule 3\* specialized to the W-marginal.
  • do_rule3_conditional_condDistrib — conditional Rule 3, literal condDistrib form.
  • do_rule3_conditional — conditional Rule 3, headline a.e. obsCondKernel form.

References

  • Basic Concepts.tex, Proposition (do-Calculus), Rule 3.
  • Pearl (2009), Causality, Chapter 3.
theorem do_rule3_conditional reviewed
Causalean.SCM

Conditional Rule 3 (headline, a.e. obsCondKernel form). Pearl's Rule 3 for the deletion of actions, stated against the project's jointly-measurable conditional kernel. Fix a do-set Z of nodes whose random copies are observed in the base model and whose fixed nodes have not already been intervened on, an outcome block Y and a conditioning block W of observed variables. If none of the fixed copies of Z's nodes is an ancestor, in the intervention SWIG graph, of any node in Y ∪ W, then for almost every value w of W under the intervened model's W-marginal, the Y-given-W conditional kernel of the model intervened at do(Z) equals the Y-given-W conditional kernel of the base model, both evaluated at the corresponding fixed values.

Formal statement
hypotheses
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
Y W :
Finset (SWIGNode N)
hY :
Y ⊆ M'.observed
hW :
W ⊆ M'.observed
StandardBorelSpace (ValuesOn Y (swigΩ Ω))
Nonempty (ValuesOn Y (swigΩ Ω))
CountableOrCountablyGenerated M'.FixedValues (ValuesOn W (swigΩ Ω))
CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))
hNoDesc :
∀ v ∈ Y ∪ W, ∀ d ∈ Z, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed d) v
s' :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
conclusion
(fun w => (M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (s', w))
=ᵐ[(M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')).map (valuesProjection hW)] (fun w => M'.obsCondKernel Y W hY hW (M'.fixSetProj Z hZ_obs hZ_fixed s', w))
Proof (Lean source)
theorem do_rule3_conditional (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (Y W : Finset (SWIGNode N)) (hY : Y ⊆ M'.observed) (hW : W ⊆ M'.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [CountableOrCountablyGenerated M'.FixedValues (ValuesOn W (swigΩ Ω))] [CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn W (swigΩ Ω))] (hNoDesc : ∀ v ∈ Y ∪ W, ∀ d ∈ Z, ¬ (M'.fixSet Z hZ_obs hZ_fixed).dag.isAncestor (SWIGNode.fixed d) v) (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) : (fun w => (M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y W ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) (s', w)) =ᵐ[(M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')).map (valuesProjection hW)] (fun w => M'.obsCondKernel Y W hY hW (M'.fixSetProj Z hZ_obs hZ_fixed s', w)) := by -- Bridge both `obsCondKernel`s to `condDistrib`, rewrite the do-side base to the -- common `W`-marginal (`obsKernel_map_W_eq`) and the do-side conditional to the -- base conditional (`do_rule3_conditional_condDistrib`), then chain a.e. equalities. have h1 := (M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel_ae_eq_condDistrib Y W ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW) s' have h2 := M'.obsCondKernel_ae_eq_condDistrib Y W hY hW (M'.fixSetProj Z hZ_obs hZ_fixed s') have hbase := obsKernel_map_W_eq M' Z hZ_obs hZ_fixed W hW (fun v hv d hd => hNoDesc v (mem_union_right _ hv) d hd) s' have hcd := do_rule3_conditional_condDistrib M' Z hZ_obs hZ_fixed Y W hY hW hNoDesc s' rw [hbase] at h1 rw [hcd] at h1 exact h1.trans h2.symm
Causalean.SCM.do_rule3_conditional · Causalean/SCM/Do/Rule3Conditional.lean:213 · uses isAncestor , SCM , FixedValues , ObservedValues , fixSet , fixSetProj , fixSet_observed , obsCondKernel , obsKernel , SWIGNode , instFintype , ValuesOn , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , valuesProjection
4 supporting declarations (lemmas, instances)
Values­Projection­CI 2 core · 5 supporting This file provides the finite-product projection infrastructure used by SCM conditional-independence proofs. ★ condIndep_valuesProjection_weak_union★ condIndep_valuesProjection_contraction

Conditional Independence for Finite-Product Projections

This file provides the finite-product projection infrastructure used by SCM conditional-independence proofs. It proves compositional and sigma-algebra facts for valuesProjection, defines valuesUnionMk for assembling two coordinate blocks into their union, and proves the specialized weak-union and contraction rules condIndep_valuesProjection_weak_union and condIndep_valuesProjection_contraction. These results specialize general conditional-expectation semi-graphoid identities to the value-block projections used by structural causal models.

theorem condIndep_valuesProjection_weak_union reviewed
Causalean

Weak union for coordinate projections. Let X, Y, W, Z be subsets of a finite index set I, with X, the union of Y and W, and the union of Z and W all contained in I, and let μ be a finite measure on the finite-product value space indexed by I. If X is conditionally independent of the union of Y and W given Z, then X is conditionally independent of Y given the union of Z and W, where independence is always of the corresponding coordinate projections under μ.

Formal statement
hypotheses
M :
Type uM
DecidableEq M
Finset M
M → Type uΩ
∀ n, MeasurableSpace (Ω n)
StandardBorelSpace (ValuesOn I Ω)
hX :
X ⊆ I
hYW :
(Y ∪ W) ⊆ I
hZW :
(Z ∪ W) ⊆ I
μ :
Measure (ValuesOn I Ω)
IsFiniteMeasure μ
h :
CondIndepFun (comap (valuesProjection (Ω := Ω) (Finset.subset_union_left.trans hZW)) inferInstance) (comap_valuesProjection_le (Ω' := Ω) (Finset.subset_union_left.trans hZW)) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hYW) μ
conclusion
CondIndepFun (comap (valuesProjection (Ω := Ω) hZW) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZW) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) (Finset.subset_union_left.trans hYW)) μ
Proof (Lean source)
theorem condIndep_valuesProjection_weak_union {M : Type uM} [DecidableEq M] {I X Y W Z : Finset M} {Ω : M → Type uΩ} [∀ n, MeasurableSpace (Ω n)] [StandardBorelSpace (ValuesOn I Ω)] (hX : X ⊆ I) (hYW : (Y ∪ W) ⊆ I) (hZW : (Z ∪ W) ⊆ I) {μ : Measure (ValuesOn I Ω)} [IsFiniteMeasure μ] (h : CondIndepFun (comap (valuesProjection (Ω := Ω) (Finset.subset_union_left.trans hZW)) inferInstance) (comap_valuesProjection_le (Ω' := Ω) (Finset.subset_union_left.trans hZW)) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hYW) μ) : CondIndepFun (comap (valuesProjection (Ω := Ω) hZW) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZW) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) (Finset.subset_union_left.trans hYW)) μ := by let hY : Y ⊆ I := Finset.subset_union_left.trans hYW let hZ : Z ⊆ I := Finset.subset_union_left.trans hZW have hW : W ⊆ I := fun w hw => hZW (mem_union_right Z hw) have hpair_meas : Measurable (fun ξ : ValuesOn (Y ∪ W) Ω => (valuesProjection (Ω := Ω) subset_union_left ξ, valuesProjection (Ω := Ω) subset_union_right ξ)) := (measurable_valuesProjection (Ω' := Ω) subset_union_left).prod (measurable_valuesProjection (Ω' := Ω) subset_union_right) have hpair : CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (fun ξ => (valuesProjection (Ω := Ω) hY ξ, valuesProjection (Ω := Ω) hW ξ)) μ := by exact h.comp measurable_id hpair_meas have hweak : CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance ⊔ comap (valuesProjection (Ω := Ω) hW) inferInstance) (sup_le (comap_valuesProjection_le (Ω' := Ω) hZ) (comap_valuesProjection_le (Ω' := Ω) hW)) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hY) μ := condIndepFun_weak_union_of_prodMk (m := comap (valuesProjection (Ω := Ω) hZ) inferInstance) (mΩ := inferInstance) (μ := μ) (comap_valuesProjection_le (Ω' := Ω) hZ) (W := valuesProjection (Ω := Ω) hX) (V := valuesProjection (Ω := Ω) hY) (A := valuesProjection (Ω := Ω) hW) (measurable_valuesProjection (Ω' := Ω) hX) (measurable_valuesProjection (Ω' := Ω) hY) (measurable_valuesProjection (Ω' := Ω) hW) hpair have hσ : comap (valuesProjection (Ω := Ω) hZW) inferInstance = comap (valuesProjection (Ω := Ω) hZ) inferInstance ⊔ comap (valuesProjection (Ω := Ω) hW) inferInstance := comap_valuesProjection_union_eq_sup (Ω' := Ω) hZ hW simpa [hσ] using hweak
Causalean.condIndep_valuesProjection_weak_union · Causalean/SCM/Do/ValuesProjectionCI.lean:131 · uses ValuesOn , comap_valuesProjection_le , valuesProjection
theorem condIndep_valuesProjection_contraction reviewed
Causalean

Contraction for coordinate projections. Let X, Y, W, Z be subsets of a common finite index set I, with X, Y, W, and Z all contained in I, and let μ be a finite measure on the resulting finite-product value space indexed by I. If X is conditionally independent of Y given the union of Z and W and X is conditionally independent of W given Z, then X is conditionally independent of the union of Y and W given Z, where independence is always of the corresponding coordinate projections under μ.

Formal statement
hypotheses
M :
Type uM
DecidableEq M
Finset M
M → Type uΩ
∀ n, MeasurableSpace (Ω n)
StandardBorelSpace (ValuesOn I Ω)
hX :
X ⊆ I
hY :
Y ⊆ I
hW :
W ⊆ I
hZ :
Z ⊆ I
μ :
Measure (ValuesOn I Ω)
IsFiniteMeasure μ
h1 :
CondIndepFun (comap (valuesProjection (Ω := Ω) (union_subset hZ hW)) inferInstance) (comap_valuesProjection_le (Ω' := Ω) (union_subset hZ hW)) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hY) μ
h2 :
CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hW) μ
conclusion
CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) (union_subset hY hW)) μ
Proof (Lean source)
theorem condIndep_valuesProjection_contraction {M : Type uM} [DecidableEq M] {I X Y W Z : Finset M} {Ω : M → Type uΩ} [∀ n, MeasurableSpace (Ω n)] [StandardBorelSpace (ValuesOn I Ω)] (hX : X ⊆ I) (hY : Y ⊆ I) (hW : W ⊆ I) (hZ : Z ⊆ I) {μ : Measure (ValuesOn I Ω)} [IsFiniteMeasure μ] (h1 : CondIndepFun (comap (valuesProjection (Ω := Ω) (Finset.union_subset hZ hW)) inferInstance) (comap_valuesProjection_le (Ω' := Ω) (Finset.union_subset hZ hW)) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hY) μ) (h2 : CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hW) μ) : CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) (Finset.union_subset hY hW)) μ := by let hYW : (Y ∪ W) ⊆ I := Finset.union_subset hY hW let hZW : (Z ∪ W) ⊆ I := Finset.union_subset hZ hW have hσ : comap (valuesProjection (Ω := Ω) hZW) inferInstance = comap (valuesProjection (Ω := Ω) hZ) inferInstance ⊔ comap (valuesProjection (Ω := Ω) hW) inferInstance := comap_valuesProjection_union_eq_sup (Ω' := Ω) hZ hW have h1' : CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance ⊔ comap (valuesProjection (Ω := Ω) hW) inferInstance) (sup_le (comap_valuesProjection_le (Ω' := Ω) hZ) (comap_valuesProjection_le (Ω' := Ω) hW)) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hY) μ := by simpa [hσ] using h1 have hpair : CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (fun ξ : ValuesOn I Ω => (valuesProjection (Ω := Ω) hY ξ, valuesProjection (Ω := Ω) hW ξ)) μ := condIndepFun_contraction_of_prodMk (m := comap (valuesProjection (Ω := Ω) hZ) inferInstance) (mΩ := inferInstance) (μ := μ) (comap_valuesProjection_le (Ω' := Ω) hZ) (measurable_valuesProjection (Ω' := Ω) hX) (measurable_valuesProjection (Ω' := Ω) hY) (measurable_valuesProjection (Ω' := Ω) hW) h1' h2 have hassembled : CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (fun ξ : ValuesOn I Ω => valuesUnionMk (Ω := Ω) (valuesProjection (Ω := Ω) hY ξ) (valuesProjection (Ω := Ω) hW ξ)) μ := hpair.comp measurable_id (measurable_valuesUnionMk (Ω := Ω)) simpa [Function.comp_def, valuesUnionMk_projection_comp (Ω' := Ω) hY hW] using hassembled
Causalean.condIndep_valuesProjection_contraction · Causalean/SCM/Do/ValuesProjectionCI.lean:206 · uses ValuesOn , comap_valuesProjection_le , valuesProjection
5 supporting declarations (lemmas, instances)
Values­Reindex 2 core · 4 supporting Equational laws for valuesUnionMk (combine two coordinate blocks into one on their union) under union reordering and ∅ collapse, stated as Eqs transported along valuesEquivOfEq (the canonical measurable equivalence for p ★ valuesUnionMk_comm★ valuesOn_heq_of_coord

ValuesOn reindexing layer (do-calculus identification toolkit)

Equational laws for valuesUnionMk (combine two coordinate blocks into one on their union) under union reordering and ∅ collapse, stated as Eqs transported along valuesEquivOfEq (the canonical measurable equivalence for propositionally-equal index Finsets) rather than as HEqs.

ValuesOn (A ∪ B) and ValuesOn (B ∪ A) are equal but not definitionally equal, which is what forces HEq/cast gymnastics in the identification proofs (e.g. the front-door derivation). Routing through valuesEquivOfEq keeps every statement an Eq, so rw/simp consume them directly and call sites never construct an HEq by hand. The valuesUnionMk_comm, valuesUnionMk_empty_right, and valuesOn_heq_of_coord lemmas are the public reindexing helpers used by do-calculus identification proofs.

lemma valuesUnionMk_comm reviewed
Causalean.SCM

Union commutativity. When A and B are disjoint, reindexing valuesUnionMk a b (a block on A ∪ B) along A ∪ B = B ∪ A yields valuesUnionMk b a.

Formal statement
hypotheses
M :
Type*
DecidableEq M
M → Type*
∀ m, MeasurableSpace (Ω m)
A B :
Finset M
hAB :
Disjoint A B
a :
ValuesOn A Ω
b :
ValuesOn B Ω
conclusion
valuesEquivOfEq (union_comm A B) (valuesUnionMk a b) = valuesUnionMk b a
Proof (Lean source)
lemma valuesUnionMk_comm {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ m, MeasurableSpace (Ω m)] {A B : Finset M} (hAB : Disjoint A B) (a : ValuesOn A Ω) (b : ValuesOn B Ω) : valuesEquivOfEq (union_comm A B) (valuesUnionMk a b) = valuesUnionMk b a := by funext ⟨v, hv⟩ have hvAB : v ∈ A ∪ B := by rwa [union_comm] show valuesUnionMk a b ⟨v, hvAB⟩ = valuesUnionMk b a ⟨v, hv⟩ by_cases hA : v ∈ A · have hB : v ∉ B := fun h => Finset.disjoint_left.mp hAB hA h simp only [valuesUnionMk, dif_pos hA, dif_neg hB] · have hB : v ∈ B := (Finset.mem_union.mp hv).resolve_right hA simp only [valuesUnionMk, dif_pos hB, dif_neg hA]
Causalean.SCM.valuesUnionMk_comm · Causalean/SCM/Do/ValuesReindex.lean:33 · uses ValuesOn , valuesEquivOfEq , valuesUnionMk
lemma valuesOn_heq_of_coord reviewed
Causalean.SCM

HEq of value assignments from coordinatewise agreement. Given two node sets I and J that are equal as sets and value assignments f on I and g on J, if f and g agree at every node common to both index sets, then f and g are heterogeneously equal (HEq).

Formal statement
hypotheses
M :
Type*
M → Type*
∀ m, MeasurableSpace (Ω m)
I J :
Finset M
hIJ :
I = J
f :
ValuesOn I Ω
g :
ValuesOn J Ω
h :
∀ (v : M) (hI : v ∈ I) (hJ : v ∈ J), f ⟨v, hI⟩ = g ⟨v, hJ⟩
conclusion
HEq f g
Proof (Lean source)
lemma valuesOn_heq_of_coord {M : Type*} {Ω : M → Type*} [∀ m, MeasurableSpace (Ω m)] {I J : Finset M} (hIJ : I = J) (f : ValuesOn I Ω) (g : ValuesOn J Ω) (h : ∀ (v : M) (hI : v ∈ I) (hJ : v ∈ J), f ⟨v, hI⟩ = g ⟨v, hJ⟩) : HEq f g := by apply Function.hfunext (congrArg (fun S : Finset M => {i // i ∈ S}) hIJ) rintro ⟨v, hvI⟩ ⟨v', hvJ⟩ hidx have hv_eq : v = v' := (Subtype.heq_iff_coe_eq (by intro x; rw [hIJ])).mp hidx subst hv_eq exact heq_of_eq (h v hvI hvJ)
Causalean.SCM.valuesOn_heq_of_coord · Causalean/SCM/Do/ValuesReindex.lean:93 · uses ValuesOn
4 supporting declarations (lemmas, instances)