SCM.ID.Frontdoor
Pearl's frontdoor adjustment for a structural causal model with treatment X, mediator W and outcome Y, stated for general (standard Borel) value spaces at the level of Markov kernels.
Setup 4 core · 6 supporting This file defines frontdoorCriterion, establishes the mediator and outcome legs used by frontdoor adjustment, and proves the kernel reindexing identities needed to compose them. ★ frontdoor_legA_mediator★ frontdoor_legB_outcome
Frontdoor criterion and component identities
This file defines frontdoorCriterion, establishes the mediator and outcome
legs used by frontdoor adjustment, and proves the kernel reindexing identities
needed to compose them. The mediator is represented by a base-node set so it
can be used as an intervention set.
def frontdoorCriterion reviewed
⚑ flagged
Causalean.SWIGGraph
For a finite node population, a SWIG graph, a treatment-variable set whose random copies are observed and whose fixed copies are not already fixed, a mediator-variable set whose random copies are observed and whose fixed copies are not already fixed, and an outcome-node set, the frontdoor criterion holds exactly when the mediator random copies d-separate the outcomes from the treatment fixed copies after intervening on the treatments, the empty set satisfies the back-door criterion for treatment and mediator, the treatment random copies satisfy the back-door criterion for mediator and outcome, and the mediator random copies are disjoint from both treatment random copies and outcomes.
Definition (Lean source)
parameters
N :
Type u_1
X :
Finset N
hX_obs :
∀ D ∈ X, SWIGNode.random D ∈ G.observed
hX_fix :
∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed
W :
Finset N
hW_obs :
∀ D ∈ W, SWIGNode.random D ∈ G.observed
hW_fix :
∀ D ∈ W, SWIGNode.fixed D ∉ G.fixed
def
frontdoorCriterion G X hX_obs hX_fix W hW_obs hW_fix Y :
Prop
given by
clause 1
(G.splitMono X hX_obs hX_fix).dag.dSep Y (X.image SWIGNode.fixed) (W.image SWIGNode.random)
clause 2
backdoorCriterion G X hX_obs hX_fix (W.image SWIGNode.random) ∅
clause 3
backdoorCriterion G W hW_obs hW_fix Y (X.image SWIGNode.random)
clause 4
Disjoint (W.image SWIGNode.random) (X.image SWIGNode.random)
clause 5
Disjoint (W.image SWIGNode.random) Y
def frontdoorKernelY reviewed
⚑ flagged
Causalean.SCM
For a finite node population with measurable, nonempty standard-Borel node-value spaces, a structural causal model, a treatment-variable set whose random copies are observed and whose fixed copies are not already fixed, an outcome-node set, a mediator-node set, the requirement that every outcome node is observed, the requirement that every mediator node is observed, and an assignment to the model's original fixed nodes, the frontdoor-adjustment conditional law of outcomes indexed by treatment values is the frontdoor-adjustment law evaluated after extending the fixed-node assignment by that treatment value. It is defined by reindexing the graph-level frontdoor-adjustment law along this extension.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hW :
W ⊆ M.observed
s0 :
M.FixedValues
def
given by
(M.frontdoorAdjustment X hObs hFix Y W hY hW).comap (M.fixSetExtend X hObs hFix s0) (M.measurable_fixSetExtend X hObs hFix s0)
theorem frontdoor_legA_mediator reviewed
⚑ flagged
Causalean.SCM
For a finite structural causal model with measurable node-value spaces, treatment nodes, observability of their random copies, absence of their fixed copies from the original fixed set, mediator nodes, observability of their random copies, absence of their fixed copies from the original fixed set, outcome nodes, the frontdoor criterion, an original fixed-node assignment, and the API's empty-adjustment absolute-continuity premise, the mediator law under treatment intervention equals the empty-adjustment back-door functional in treatment-indexed joint-law form. The premise is an empty-coordinate self-domination condition.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Wbase :
Finset N
hWobs :
∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed
hWfix :
∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed
hFD :
frontdoorCriterion M.toSWIGGraph X hObs hFix Wbase hWobs hWfix Y
s0 :
M.FixedValues
hPositivityA :
M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using (Finset.image_subset_iff.mpr hObs)) s0
conclusion
(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ (M.doKernelY X hObs hFix (Wbase.image SWIGNode.random) (Finset.image_subset_iff.mpr hWobs) s0)
= (M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ (M.adjustmentKernelY X hObs hFix (Wbase.image SWIGNode.random) (∅ : Finset (SWIGNode N)) (Finset.image_subset_iff.mpr hWobs) (empty_subset M.observed) s0)
Proof (Lean source)
theorem frontdoor_legA_mediator
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Wbase : Finset N)
(hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed)
(hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N))
(hFD : frontdoorCriterion M.toSWIGGraph
X hObs hFix Wbase hWobs hWfix Y)
(s0 : M.FixedValues)
(hPositivityA : M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N))
(empty_subset M.observed)
(by simpa using (Finset.image_subset_iff.mpr hObs)) s0) :
(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ
(M.doKernelY X hObs hFix (Wbase.image SWIGNode.random)
(Finset.image_subset_iff.mpr hWobs) s0)
=
(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ
(M.adjustmentKernelY X hObs hFix (Wbase.image SWIGNode.random)
(∅ : Finset (SWIGNode N)) (Finset.image_subset_iff.mpr hWobs)
(empty_subset M.observed) s0) := by
have hWr : Wbase.image SWIGNode.random ⊆ M.observed :=
Finset.image_subset_iff.mpr hWobs
exact M.backdoor_completeness_ae_compProd X hObs hFix
(Wbase.image SWIGNode.random) (∅ : Finset (SWIGNode N))
hWr (empty_subset M.observed) hFD.2.1 s0 hPositivityA
theorem frontdoor_legB_outcome reviewed
⚑ flagged
Causalean.SCM
For a finite structural causal model with measurable node-value spaces, treatment nodes, observability of their random copies, absence of their fixed copies from the original fixed set, mediator nodes, observability of their random copies, absence of their fixed copies from the original fixed set, outcome nodes, observability of outcomes, the frontdoor criterion, an original fixed-node assignment, and the corresponding positivity condition, the outcome law under mediator intervention equals the back-door functional adjusting for observed treatment in mediator-indexed joint-law form.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Wbase :
Finset N
hWobs :
∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed
hWfix :
∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hFD :
frontdoorCriterion M.toSWIGGraph X hObs hFix Wbase hWobs hWfix Y
s0 :
M.FixedValues
hPositivityB :
M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) (Finset.image_subset_iff.mpr hObs) (union_subset (Finset.image_subset_iff.mpr hWobs) (Finset.image_subset_iff.mpr hObs)) s0
conclusion
(M.treatmentMarginal Wbase (Finset.image_subset_iff.mpr hWobs) s0) ⊗ₘ (M.doKernelY Wbase hWobs hWfix Y hY s0)
= (M.treatmentMarginal Wbase (Finset.image_subset_iff.mpr hWobs) s0) ⊗ₘ (M.adjustmentKernelY Wbase hWobs hWfix Y (X.image SWIGNode.random) hY (Finset.image_subset_iff.mpr hObs) s0)
Proof (Lean source)
theorem frontdoor_legB_outcome
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Wbase : Finset N)
(hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed)
(hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N))
(hY : Y ⊆ M.observed)
(hFD : frontdoorCriterion M.toSWIGGraph
X hObs hFix Wbase hWobs hWfix Y)
(s0 : M.FixedValues)
(hPositivityB : M.BackdoorPositivityAE Wbase (X.image SWIGNode.random)
(Finset.image_subset_iff.mpr hObs)
(union_subset (Finset.image_subset_iff.mpr hWobs)
(Finset.image_subset_iff.mpr hObs)) s0) :
(M.treatmentMarginal Wbase (Finset.image_subset_iff.mpr hWobs) s0) ⊗ₘ
(M.doKernelY Wbase hWobs hWfix Y hY s0)
=
(M.treatmentMarginal Wbase (Finset.image_subset_iff.mpr hWobs) s0) ⊗ₘ
(M.adjustmentKernelY Wbase hWobs hWfix Y (X.image SWIGNode.random)
hY (Finset.image_subset_iff.mpr hObs) s0) := by
have hXr : X.image SWIGNode.random ⊆ M.observed :=
Finset.image_subset_iff.mpr hObs
exact M.backdoor_completeness_ae_compProd Wbase hWobs hWfix Y (X.image SWIGNode.random)
hY hXr hFD.2.2.1 s0 hPositivityB
6 supporting declarations (lemmas, instances)
-
instIsFiniteKernelFrontdoorKernelYinstance — For a finite, distinguishable node population with measurable, standard-Borel, nonempty node-value spaces and a structural causal model, a finite treatment set, the requirement that every corresponding random treatment node is observed, the requirement that no corresponding fixed treatment node is already fixed, finite observed outcome and mediator-node sets, and a fixed-node assignment, the treatment-indexed frontdoor-adjustment outcome kernel is finite.parametersN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhY :Y ⊆ M.observedhW :W ⊆ M.observeds0 :M.FixedValuesinstanceinstIsFiniteKernelFrontdoorKernelY M X hObs hFix Y W hY hW s0 :IsFiniteKernel (M.frontdoorKernelY X hObs hFix Y W hY hW s0)given byby rw [SCM.frontdoorKernelY]; infer_instance -
obsKernel_map_proj_eq_of_equivlemma — Structurally equivalent structural causal models assign the same observational marginal law to a shared set of observed variables when their fixed-variable assignments correspond.hypothesesh :SCM.Equiv M₁ M₂hY₁ :Y ⊆ M₁.observedhY₂ :Y ⊆ M₂.observeds₁ :M₁.FixedValuess₂ :M₂.FixedValueshs :HEq s₁ s₂conclusion(M₁.obsKernel s₁).map (valuesProjection hY₁)= (M₂.obsKernel s₂).map (valuesProjection hY₂)Proof (Lean source)
lemma obsKernel_map_proj_eq_of_equiv {M₁ M₂ : SCM N Ω} (h : SCM.Equiv M₁ M₂) (Y : Finset (SWIGNode N)) (hY₁ : Y ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (s₁ : M₁.FixedValues) (s₂ : M₂.FixedValues) (hs : HEq s₁ s₂) : (M₁.obsKernel s₁).map (valuesProjection hY₁) = (M₂.obsKernel s₂).map (valuesProjection hY₂) := by -- Extract the `obsKernel` HEq while `h` still has its `Equiv` type. have hok0 : HEq M₁.obsKernel M₂.obsKernel := SCM.Equiv.heq_obsKernel h.1 h.2.2.1 h.2.2.2 obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ rcases h.1 with ⟨_hEdge, rfl, rfl, rfl⟩ -- After unifying `observed`/`fixed`/`unobserved`, the `FixedValues` and -- `ObservedValues` types coincide, so the `HEq`s collapse to `Eq`. have hs_eq : s₁ = s₂ := eq_of_heq hs subst hs_eq have hok := eq_of_heq hok0 rw [hok] -
obsCondKernel_congr_cclemma — Given a finite structural causal model, target set, and two conditioning sets, if the conditioning sets are equal, all three coordinate sets are observed, and two conditioning assignments are equal after type transport, then the resulting observational conditional measures are equal.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhCCeq :CC₁ = CC₂hY :Y ⊆ M.observedhCC₁ :CC₁ ⊆ M.observedhCC₂ :CC₂ ⊆ M.observeds :M.FixedValueshc :HEq c₁ c₂conclusionM.obsCondKernel Y CC₁ hY hCC₁ (s, c₁) = M.obsCondKernel Y CC₂ hY hCC₂ (s, c₂)Proof (Lean source)
lemma obsCondKernel_congr_cc (M : SCM N Ω) (Y CC₁ CC₂ : Finset (SWIGNode N)) (hCCeq : CC₁ = CC₂) (hY : Y ⊆ M.observed) (hCC₁ : CC₁ ⊆ M.observed) (hCC₂ : CC₂ ⊆ M.observed) (s : M.FixedValues) (c₁ : ValuesOn CC₁ (swigΩ Ω)) (c₂ : ValuesOn CC₂ (swigΩ Ω)) (hc : HEq c₁ c₂) : M.obsCondKernel Y CC₁ hY hCC₁ (s, c₁) = M.obsCondKernel Y CC₂ hY hCC₂ (s, c₂) := by subst hCCeq have hc' : c₁ = c₂ := eq_of_heq hc subst hc' have hp : hCC₁ = hCC₂ := Subsingleton.elim _ _ subst hp rfl -
valuesUnionMk_union_comm_heqlemma — Given two disjoint finite coordinate sets and assignments on each, combining the assignments in either order gives equal values after type transport.hypotheseshDisj :Disjoint A BProof (Lean source)
lemma valuesUnionMk_union_comm_heq {A B : Finset (SWIGNode N)} (hDisj : Disjoint A B) (a : ValuesOn A (swigΩ Ω)) (b : ValuesOn B (swigΩ Ω)) : HEq (valuesUnionMk a b : ValuesOn (A ∪ B) (swigΩ Ω)) (valuesUnionMk b a : ValuesOn (B ∪ A) (swigΩ Ω)) := -- Now a one-line corollary of the `ValuesReindex` algebra layer. valuesUnionMk_comm_heq hDisj a b -
adjustmentKernelY_empty_eqlemma — With an empty adjustment set, the outcome adjustment kernel equals the observed conditional kernel of the outcome variables given the treated variables at the same fixed values.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhWr :Wr ⊆ M.observedhXr :X.image SWIGNode.random ⊆ M.observeds0 :M.FixedValuesconclusion= M.obsCondKernel Wr (X.image SWIGNode.random) hWr hXr (s0, t)Proof (Lean source)
lemma adjustmentKernelY_empty_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Wr : Finset (SWIGNode N)) (hWr : Wr ⊆ M.observed) (hXr : X.image SWIGNode.random ⊆ M.observed) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) : M.adjustmentKernelY X hObs hFix Wr (∅ : Finset (SWIGNode N)) hWr (empty_subset _) s0 t = M.obsCondKernel Wr (X.image SWIGNode.random) hWr hXr (s0, t) := by let sTt := M.fixSetExtend X hObs hFix s0 t let zMarginalPost : Kernel (M.fixSet X hObs hFix).FixedValues (ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) := (M.obsKernel.map (valuesProjection (empty_subset M.observed))).comap (M.fixSetProj X hObs hFix) (M.measurable_fixSetProj X hObs hFix) haveI : IsMarkovKernel (M.obsCondKernel Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) hWr (union_subset hXr (empty_subset M.observed))) := by unfold SCM.obsCondKernel infer_instance let condPost : Kernel ((M.fixSet X hObs hFix).FixedValues × ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) (ValuesOn Wr (swigΩ Ω)) := (M.obsCondKernel Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) hWr (union_subset hXr (empty_subset M.observed))).comap (fun p => (M.fixSetProj X hObs hFix p.1, M.fillZrW X hObs hFix (∅ : Finset (SWIGNode N)) p.1 p.2)) (prodMk ((M.measurable_fixSetProj X hObs hFix).comp measurable_fst) (M.measurable_fillZrW_prod X hObs hFix (∅ : Finset (SWIGNode N)))) haveI : IsSFiniteKernel zMarginalPost := by dsimp [zMarginalPost] infer_instance haveI : IsSFiniteKernel condPost := by dsimp [condPost] infer_instance have hcollapse : ((zMarginalPost ⊗ₖ condPost).map snd) sTt = condPost (sTt, (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) := by rw [compProd_map_snd_apply] have hz : zMarginalPost sTt = dirac (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) := by ext S hS by_cases hempty : S = ∅ · simp [hempty] · have h_univ : S = univ := by apply Set.eq_univ_of_forall intro x by_contra hx apply hempty ext y constructor · intro hy have : y = x := Subsingleton.elim y x exact False.elim (hx (this ▸ hy)) · intro hy simp at hy rw [h_univ] dsimp [zMarginalPost] rw [ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _)] rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection _) MeasurableSet.univ] simp [M.obsKernel_apply_univ (M.fixSetProj X hObs hFix sTt)] rw [hz] simpa [sectR] using (MeasureTheory.Measure.dirac_bind (a := (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) (f := condPost.sectR sTt) (hf := by fun_prop)) have hadj : M.adjustmentKernelY X hObs hFix Wr (∅ : Finset (SWIGNode N)) hWr (empty_subset _) s0 t = ((zMarginalPost ⊗ₖ condPost).map snd) sTt := by rw [SCM.adjustmentKernelY, ProbabilityTheory.Kernel.comap_apply] change M.backdoorAdjustment X hObs hFix Wr (∅ : Finset (SWIGNode N)) hWr (empty_subset _) sTt = ((zMarginalPost ⊗ₖ condPost).map snd) sTt rw [SCM.backdoorAdjustment] rw [hadj, hcollapse] have hcond : condPost (sTt, (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) = M.obsCondKernel Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) hWr (union_subset hXr (empty_subset M.observed)) (s0, valuesUnionMk t (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω))) := by simp [condPost, sTt, SCM.fixSetProj_fixSetExtend, SCM.fillZrW_fixSetExtend] rw [hcond] apply obsCondKernel_congr_cc M Wr (X.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N))) (X.image SWIGNode.random) (union_empty _) hWr (union_subset hXr (empty_subset M.observed)) hXr exact valuesOn_heq_of_coord (union_empty _) _ _ (fun v hvU hvX => valuesUnionMk_apply_left t (default : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω)) hvX) -
frontdoor_doubledo_dropX_marginallemma — Given a finite structural causal model, disjoint treatment and mediator sets with valid interventions, and an observed outcome set, if no fixed treatment copy is an ancestor of an outcome after both interventions, then for fixed, treatment, and mediator assignments, marginalizing the twice-intervened observational kernel to the outcome equals the outcome kernel under the mediator intervention.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedWbase :Finset NhWobs :∀ D ∈ Wbase, SWIGNode.random D ∈ M.observedhWfix :∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixedhY :Y ⊆ M.observedhDisjBaseXW :Disjoint X WbasehWobsX :∀ D ∈ Wbase, SWIGNode.random D ∈ (M.fixSet X hObs hFix).observedhWfixX :∀ D ∈ Wbase, SWIGNode.fixed D ∉ (M.fixSet X hObs hFix).fixedhXobsW :∀ D ∈ X, SWIGNode.random D ∈ (M.fixSet Wbase hWobs hWfix).observedhXfixW :∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixSet Wbase hWobs hWfix).fixedhG2 :∀ z ∈ X,∀ v ∈ Y,¬ ((M.fixSet Wbase hWobs hWfix).fixSet X hXobsW hXfixW).dag.isAncestor (SWIGNode.fixed z) vs0 :M.FixedValuesconclusion(((M.fixSet X hObs hFix).fixSet Wbase hWobsX hWfixX).obsKernel ((M.fixSet X hObs hFix).fixSetExtend Wbase hWobsX hWfixX (M.fixSetExtend X hObs hFix s0 t) w)).map (valuesProjection (by simpa [SCM.fixSet_observed] using hY))= M.doKernelY Wbase hWobs hWfix Y hY s0 wProof (Lean source)
lemma frontdoor_doubledo_dropX_marginal (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Wbase : Finset N) (hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed) (hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hDisjBaseXW : Disjoint X Wbase) (hWobsX : ∀ D ∈ Wbase, SWIGNode.random D ∈ (M.fixSet X hObs hFix).observed) (hWfixX : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ (M.fixSet X hObs hFix).fixed) (hXobsW : ∀ D ∈ X, SWIGNode.random D ∈ (M.fixSet Wbase hWobs hWfix).observed) (hXfixW : ∀ D ∈ X, SWIGNode.fixed D ∉ (M.fixSet Wbase hWobs hWfix).fixed) (hG2 : ∀ z ∈ X, ∀ v ∈ Y, ¬ ((M.fixSet Wbase hWobs hWfix).fixSet X hXobsW hXfixW).dag.isAncestor (SWIGNode.fixed z) v) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) (w : ValuesOn (Wbase.image SWIGNode.random) (swigΩ Ω)) : (((M.fixSet X hObs hFix).fixSet Wbase hWobsX hWfixX).obsKernel ((M.fixSet X hObs hFix).fixSetExtend Wbase hWobsX hWfixX (M.fixSetExtend X hObs hFix s0 t) w)).map (valuesProjection (by simpa [SCM.fixSet_observed] using hY)) = M.doKernelY Wbase hWobs hWfix Y hY s0 w := by let M₁ := (M.fixSet X hObs hFix).fixSet Wbase hWobsX hWfixX let M₂ := (M.fixSet Wbase hWobs hWfix).fixSet X hXobsW hXfixW let s₁ : M₁.FixedValues := (M.fixSet X hObs hFix).fixSetExtend Wbase hWobsX hWfixX (M.fixSetExtend X hObs hFix s0 t) w let s₃ : M₂.FixedValues := (M.fixSet Wbase hWobs hWfix).fixSetExtend X hXobsW hXfixW (M.fixSetExtend Wbase hWobs hWfix s0 w) t have hU1o : ∀ D ∈ X ∪ Wbase, SWIGNode.random D ∈ M.observed := by intro D hD rcases Finset.mem_union.mp hD with hD | hD · exact hObs D hD · exact hWobs D hD have hU1f : ∀ D ∈ X ∪ Wbase, SWIGNode.fixed D ∉ M.fixed := by intro D hD rcases Finset.mem_union.mp hD with hD | hD · exact hFix D hD · exact hWfix D hD have hU2o : ∀ D ∈ Wbase ∪ X, SWIGNode.random D ∈ M.observed := by intro D hD rcases Finset.mem_union.mp hD with hD | hD · exact hWobs D hD · exact hObs D hD have hU2f : ∀ D ∈ Wbase ∪ X, SWIGNode.fixed D ∉ M.fixed := by intro D hD rcases Finset.mem_union.mp hD with hD | hD · exact hWfix D hD · exact hFix D hD have e1 : SCM.Equiv M₁ (M.fixSet (X ∪ Wbase) hU1o hU1f) := by exact SCM.ID.intervention_target_simp M X Wbase hObs hFix hWobsX hWfixX hU1o hU1f hDisjBaseXW have e2 : SCM.Equiv M₂ (M.fixSet (Wbase ∪ X) hU2o hU2f) := by exact SCM.ID.intervention_target_simp M Wbase X hWobs hWfix hXobsW hXfixW hU2o hU2f hDisjBaseXW.symm have eb : SCM.Equiv (M.fixSet (X ∪ Wbase) hU1o hU1f) (M.fixSet (Wbase ∪ X) hU2o hU2f) := by simpa [union_comm] using (SCM.Equiv.refl (M.fixSet (X ∪ Wbase) hU1o hU1f)) have eswap : SCM.Equiv M₁ M₂ := SCM.Equiv.trans e1 (SCM.Equiv.trans eb e2.symm) have hY₁ : Y ⊆ M₁.observed := by simpa [M₁, SCM.fixSet_observed] using hY have hY₂ : Y ⊆ M₂.observed := by simpa [M₂, SCM.fixSet_observed] using hY have hs : HEq s₁ s₃ := by have hFixed : M₁.fixed = M₂.fixed := by dsimp [M₁, M₂] simp [union_comm, Finset.union_left_comm] have hDisjXWf : Disjoint (X.image SWIGNode.fixed) (Wbase.image SWIGNode.fixed) := by rw [Finset.disjoint_left] intro v hvX hvW rcases Finset.mem_image.mp hvX with ⟨x, hx, rfl⟩ rcases Finset.mem_image.mp hvW with ⟨w0, hw0, hEq⟩ cases hEq exact (Finset.disjoint_left.mp hDisjBaseXW) hx hw0 apply Function.hfunext · exact congrArg (fun S : Finset (SWIGNode N) => {i // i ∈ S}) hFixed · rintro ⟨v, hv₁⟩ ⟨v', hv₃⟩ hidx have hv_eq : v = v' := by exact (Subtype.heq_iff_coe_eq (by intro x; rw [hFixed])).mp hidx subst hv_eq apply heq_of_eq have hv₁_full : v ∈ (M.fixed ∪ X.image SWIGNode.fixed) ∪ Wbase.image SWIGNode.fixed := by simpa [M₁, SCM.fixSet_fixed] using hv₁ by_cases hM : v ∈ M.fixed · simp [s₁, s₃, M₁, M₂, SCM.fixSetExtend, SCM.fixSet_fixed, hM] · by_cases hXf : v ∈ X.image SWIGNode.fixed · have hnotWf : v ∉ Wbase.image SWIGNode.fixed := fun hWf => (Finset.disjoint_left.mp hDisjXWf) hXf hWf have hnotMW : v ∉ M.fixed ∪ Wbase.image SWIGNode.fixed := by simp [hM, hnotWf] have hMX : v ∈ M.fixed ∪ X.image SWIGNode.fixed := mem_union_right _ hXf simp [s₁, s₃, M₁, M₂, SCM.fixSetExtend, SCM.fixSet_fixed, hM, hnotMW, hMX] · have hWf : v ∈ Wbase.image SWIGNode.fixed := by rcases Finset.mem_union.mp hv₁_full with hMX | hWf · rcases Finset.mem_union.mp hMX with hM' | hXf' · exact False.elim (hM hM') · exact False.elim (hXf hXf') · exact hWf have hnotMX : v ∉ M.fixed ∪ X.image SWIGNode.fixed := by simp [hM, hXf] have hMW : v ∈ M.fixed ∪ Wbase.image SWIGNode.fixed := mem_union_right _ hWf simp [s₁, s₃, M₁, M₂, SCM.fixSetExtend, SCM.fixSet_fixed, hM, hnotMX, hMW] have hswap := obsKernel_map_proj_eq_of_equiv eswap Y hY₁ hY₂ s₁ s₃ hs have hdrop := SCM.condDistrib_intervention_ancestral_eq (M.fixSet Wbase hWobs hWfix) X hXobsW hXfixW Y (by simpa [SCM.fixSet_observed] using hY) hG2 s₃ have hproj : (M.fixSet Wbase hWobs hWfix).fixSetProj X hXobsW hXfixW s₃ = M.fixSetExtend Wbase hWobs hWfix s0 w := by dsimp [s₃] rw [SCM.fixSetProj_fixSetExtend] rw [show ((((M.fixSet X hObs hFix).fixSet Wbase hWobsX hWfixX).obsKernel ((M.fixSet X hObs hFix).fixSetExtend Wbase hWobsX hWfixX (M.fixSetExtend X hObs hFix s0 t) w)).map (valuesProjection (by simpa [SCM.fixSet_observed] using hY))) = (M₁.obsKernel s₁).map (valuesProjection hY₁) from rfl] rw [hswap] rw [show (M₂.obsKernel s₃).map (valuesProjection hY₂) = (((M.fixSet Wbase hWobs hWfix).fixSet X hXobsW hXfixW).obsKernel s₃).map (valuesProjection ((SCM.fixSet_observed (M.fixSet Wbase hWobs hWfix) X hXobsW hXfixW).symm ▸ (by simpa [SCM.fixSet_observed] using hY))) from rfl] rw [hdrop] rw [hproj] rw [SCM.doKernelY, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection _), ProbabilityTheory.Kernel.comap_apply]
Completeness 2 core · 0 supporting This file assembles the mediator, outcome, and interception identities into the frontdoor functional. ★ frontdoor_completeness_ae_compProd★ frontdoor_adjustment_ae
Frontdoor adjustment equality, a.e. in treatment
This file assembles the mediator, outcome, and interception identities into the
frontdoor functional. It proves both the version-safe compProd equality and
the resulting almost-everywhere equality between frontdoorAdjustment and the
post-intervention outcome marginal.
theorem frontdoor_completeness_ae_compProd reviewed
⚑ flagged
Causalean.SCM
For a finite structural causal model with measurable, standard-Borel, nonempty node-value spaces, treatment nodes whose random copies are observed and whose fixed copies are not already fixed, mediator nodes with the same intervention validity conditions, outcome nodes, observability of outcomes, the frontdoor criterion, an original fixed-node assignment, and the API's three formal support premises, the joint law of the treatment marginal with the post-intervention outcome equals its joint law with the frontdoor-adjustment functional. The first and third premises are empty-coordinate self-domination conditions; only the middle premise expresses substantive treatment–mediator overlap.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Wbase :
Finset N
hWobs :
∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed
hWfix :
∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hFD :
frontdoorCriterion M.toSWIGGraph X hObs hFix Wbase hWobs hWfix Y
s0 :
M.FixedValues
hPositivityA :
M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using (Finset.image_subset_iff.mpr hObs)) s0
hPositivityB :
M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) (Finset.image_subset_iff.mpr hObs) (union_subset (Finset.image_subset_iff.mpr hWobs) (Finset.image_subset_iff.mpr hObs)) s0
hPositivityFD1 :
∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [SCM.fixSet_observed] using (Finset.image_subset_iff.mpr hWobs))) ⊗ₘ const _ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (empty_subset _)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (I := (M.fixSet X hObs hFix).observed) (J := Wbase.image SWIGNode.random ∪ ∅) (Ω := swigΩ Ω) (by simpa [union_empty, SCM.fixSet_observed] using (Finset.image_subset_iff.mpr hWobs))))
conclusion
(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0)
= (M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ (M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY (Finset.image_subset_iff.mpr hWobs) s0)
Proof (Lean source)
theorem frontdoor_completeness_ae_compProd
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Wbase : Finset N)
(hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed)
(hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N))
(hY : Y ⊆ M.observed)
(hFD : frontdoorCriterion M.toSWIGGraph
X hObs hFix Wbase hWobs hWfix Y)
(s0 : M.FixedValues)
(hPositivityA : M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N))
(empty_subset M.observed)
(by simpa using (Finset.image_subset_iff.mpr hObs)) s0)
(hPositivityB : M.BackdoorPositivityAE Wbase (X.image SWIGNode.random)
(Finset.image_subset_iff.mpr hObs)
(union_subset (Finset.image_subset_iff.mpr hWobs)
(Finset.image_subset_iff.mpr hObs)) s0)
(hPositivityFD1 : ∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(by simpa [SCM.fixSet_observed] using
(Finset.image_subset_iff.mpr hWobs))) ⊗ₘ
const _
(((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection (empty_subset _)))).map
(fun p => valuesUnionMk p.1 p.2))
≪ (((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(I := (M.fixSet X hObs hFix).observed)
(J := Wbase.image SWIGNode.random ∪ ∅)
(Ω := swigΩ Ω)
(by simpa [union_empty, SCM.fixSet_observed] using
(Finset.image_subset_iff.mpr hWobs))))) :
(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ
(M.doKernelY X hObs hFix Y hY s0)
= (M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ
(M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY
(Finset.image_subset_iff.mpr hWobs) s0) := by
exact frontdoor_fd1_interception_compProd M X hObs hFix Wbase hWobs hWfix Y hY
hFD s0 hPositivityA hPositivityB hPositivityFD1
theorem frontdoor_adjustment_ae reviewed
⚑ flagged
Causalean.SCM
For a finite structural causal model with measurable, standard-Borel, nonempty node-value spaces, treatment nodes whose random copies are observed and whose fixed copies are not already fixed, mediator nodes with the same intervention validity conditions, outcome nodes, observability of outcomes, the frontdoor criterion, an original fixed-node assignment, and the API's three formal support premises, for almost every treatment value, the post-intervention outcome law equals the frontdoor-adjustment functional. The first and third premises are empty-coordinate self-domination conditions; only the middle premise expresses substantive treatment–mediator overlap.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Wbase :
Finset N
hWobs :
∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed
hWfix :
∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hFD :
frontdoorCriterion M.toSWIGGraph X hObs hFix Wbase hWobs hWfix Y
s0 :
M.FixedValues
hPositivityA :
M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using (Finset.image_subset_iff.mpr hObs)) s0
hPositivityB :
M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) (Finset.image_subset_iff.mpr hObs) (union_subset (Finset.image_subset_iff.mpr hWobs) (Finset.image_subset_iff.mpr hObs)) s0
hPositivityFD1 :
∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [SCM.fixSet_observed] using (Finset.image_subset_iff.mpr hWobs))) ⊗ₘ const _ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (empty_subset _)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (I := (M.fixSet X hObs hFix).observed) (J := Wbase.image SWIGNode.random ∪ ∅) (Ω := swigΩ Ω) (by simpa [union_empty, SCM.fixSet_observed] using (Finset.image_subset_iff.mpr hWobs))))
conclusion
∀ᵐ t ∂(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0), M.doKernelY X hObs hFix Y hY s0 t
= M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY (Finset.image_subset_iff.mpr hWobs) s0 t
Proof (Lean source)
theorem frontdoor_adjustment_ae
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Wbase : Finset N)
(hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed)
(hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N))
(hY : Y ⊆ M.observed)
(hFD : frontdoorCriterion M.toSWIGGraph
X hObs hFix Wbase hWobs hWfix Y)
(s0 : M.FixedValues)
(hPositivityA : M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N))
(empty_subset M.observed)
(by simpa using (Finset.image_subset_iff.mpr hObs)) s0)
(hPositivityB : M.BackdoorPositivityAE Wbase (X.image SWIGNode.random)
(Finset.image_subset_iff.mpr hObs)
(Finset.union_subset (Finset.image_subset_iff.mpr hWobs)
(Finset.image_subset_iff.mpr hObs)) s0)
(hPositivityFD1 : ∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(by simpa [SCM.fixSet_observed] using
(Finset.image_subset_iff.mpr hWobs))) ⊗ₘ
const _
(((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection (empty_subset _)))).map
(fun p => valuesUnionMk p.1 p.2))
≪ (((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(I := (M.fixSet X hObs hFix).observed)
(J := Wbase.image SWIGNode.random ∪ ∅)
(Ω := swigΩ Ω)
(by simpa [union_empty, SCM.fixSet_observed] using
(Finset.image_subset_iff.mpr hWobs))))) :
∀ᵐ t ∂(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0),
M.doKernelY X hObs hFix Y hY s0 t
= M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY
(Finset.image_subset_iff.mpr hWobs) s0 t := by
have hWr : Wbase.image SWIGNode.random ⊆ M.observed :=
Finset.image_subset_iff.mpr hWobs
have hXr : X.image SWIGNode.random ⊆ M.observed :=
Finset.image_subset_iff.mpr hObs
have hXrW : X.image SWIGNode.random ∪ Wbase.image SWIGNode.random ⊆ M.observed :=
Finset.union_subset hXr hWr
haveI : IsFiniteMeasure (M.treatmentMarginal X hXr s0) := by
unfold treatmentMarginal
exact (M.obsKernel s0).isFiniteMeasure_map _
exact ProbabilityTheory.Kernel.ae_eq_of_compProd_eq
(M.frontdoor_completeness_ae_compProd X hObs hFix Wbase hWobs hWfix Y hY
hFD s0 hPositivityA hPositivityB hPositivityFD1)
Interception 1 core · 0 supporting This file proves the compProd identity contributed by the frontdoor interception clause. ★ frontdoor_fd1_interception_compProd
The interception bridge for frontdoor adjustment
This file proves the compProd identity contributed by the frontdoor interception clause. It connects the double-intervention outcome kernel to the single-intervention kernel and is the FD1 bridge consumed by the final frontdoor assembly.
theorem frontdoor_fd1_interception_compProd reviewed
⚑ flagged
Causalean.SCM
For a finite structural causal model with measurable node-value spaces, treatment nodes, observability of their random copies, absence of their fixed copies from the original fixed set, mediator nodes, observability of their random copies, absence of their fixed copies from the original fixed set, outcome nodes, observability of outcomes, the frontdoor criterion, an original fixed-node assignment, and the API's three formal support premises, the treatment-indexed causal outcome law equals the treatment-indexed frontdoor adjustment law. The first and third premises are empty-coordinate self-domination conditions; only the middle premise expresses substantive treatment–mediator overlap.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M :
SCM N Ω
X :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Wbase :
Finset N
hWobs :
∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed
hWfix :
∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed
hY :
Y ⊆ M.observed
hFD :
frontdoorCriterion M.toSWIGGraph X hObs hFix Wbase hWobs hWfix Y
s0 :
M.FixedValues
hPositivityA :
M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N)) (empty_subset M.observed) (by simpa using (Finset.image_subset_iff.mpr hObs)) s0
hPositivityB :
M.BackdoorPositivityAE Wbase (X.image SWIGNode.random) (Finset.image_subset_iff.mpr hObs) (union_subset (Finset.image_subset_iff.mpr hWobs) (Finset.image_subset_iff.mpr hObs)) s0
hPositivityFD1 :
∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (by simpa [SCM.fixSet_observed] using (Finset.image_subset_iff.mpr hWobs))) ⊗ₘ const _ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (empty_subset _)))).map (fun p => valuesUnionMk p.1 p.2)) ≪ (((M.fixSet X hObs hFix).obsKernel s).map (valuesProjection (I := (M.fixSet X hObs hFix).observed) (J := Wbase.image SWIGNode.random ∪ ∅) (Ω := swigΩ Ω) (by simpa [union_empty, SCM.fixSet_observed] using (Finset.image_subset_iff.mpr hWobs))))
conclusion
(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ (M.doKernelY X hObs hFix Y hY s0)
= (M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ (M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY (Finset.image_subset_iff.mpr hWobs) s0)
Proof (Lean source)
theorem frontdoor_fd1_interception_compProd
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Wbase : Finset N)
(hWobs : ∀ D ∈ Wbase, SWIGNode.random D ∈ M.observed)
(hWfix : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ M.fixed)
(Y : Finset (SWIGNode N))
(hY : Y ⊆ M.observed)
(hFD : frontdoorCriterion M.toSWIGGraph
X hObs hFix Wbase hWobs hWfix Y)
(s0 : M.FixedValues)
(hPositivityA : M.BackdoorPositivityAE X (∅ : Finset (SWIGNode N))
(empty_subset M.observed)
(by simpa using (Finset.image_subset_iff.mpr hObs)) s0)
(hPositivityB : M.BackdoorPositivityAE Wbase (X.image SWIGNode.random)
(Finset.image_subset_iff.mpr hObs)
(union_subset (Finset.image_subset_iff.mpr hWobs)
(Finset.image_subset_iff.mpr hObs)) s0)
(hPositivityFD1 : ∀ s : (M.fixSet X hObs hFix).FixedValues,
((((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(by simpa [SCM.fixSet_observed] using
(Finset.image_subset_iff.mpr hWobs))) ⊗ₘ
const _
(((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection (empty_subset _)))).map
(fun p => valuesUnionMk p.1 p.2))
≪ (((M.fixSet X hObs hFix).obsKernel s).map
(valuesProjection
(I := (M.fixSet X hObs hFix).observed)
(J := Wbase.image SWIGNode.random ∪ ∅)
(Ω := swigΩ Ω)
(by simpa [union_empty, SCM.fixSet_observed] using
(Finset.image_subset_iff.mpr hWobs)))))
:
(M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ
(M.doKernelY X hObs hFix Y hY s0)
= (M.treatmentMarginal X (Finset.image_subset_iff.mpr hObs) s0) ⊗ₘ
(M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY
(Finset.image_subset_iff.mpr hWobs) s0) := by
have hWr : Wbase.image SWIGNode.random ⊆ M.observed :=
Finset.image_subset_iff.mpr hWobs
have hXr : X.image SWIGNode.random ⊆ M.observed :=
Finset.image_subset_iff.mpr hObs
have hDisj_WrXr :
Disjoint (Wbase.image SWIGNode.random) (X.image SWIGNode.random) :=
hFD.2.2.2.1
have hDisj_YWr : Disjoint Y (Wbase.image SWIGNode.random) :=
hFD.2.2.2.2.symm
have hXrW : X.image SWIGNode.random ∪ Wbase.image SWIGNode.random ⊆ M.observed :=
union_subset hXr hWr
have hLegA := frontdoor_legA_mediator M X hObs hFix Wbase hWobs hWfix Y
hFD s0 hPositivityA
have hLegB := frontdoor_legB_outcome M X hObs hFix Wbase hWobs hWfix Y hY
hFD s0 hPositivityB
have hG1 :=
frontdoor_fd3_rule2_dSep M X Wbase hObs hFix hWobs hWfix Y hY hFD.2.2.1
hDisj_WrXr
have hG2 :=
frontdoor_fd1_rule3_nonDesc M X Wbase hObs hFix hWobs hWfix Y hFD.1 hDisj_WrXr
haveI : IsFiniteMeasure (M.treatmentMarginal X hXr s0) := by
unfold treatmentMarginal
exact (M.obsKernel s0).isFiniteMeasure_map _
haveI : IsFiniteMeasure (M.treatmentMarginal Wbase hWr s0) := by
unfold treatmentMarginal
exact (M.obsKernel s0).isFiniteMeasure_map _
haveI : IsFiniteKernel
(M.doKernelY X hObs hFix (Wbase.image SWIGNode.random) hWr s0) := by
rw [SCM.doKernelY]; infer_instance
haveI : IsFiniteKernel
(M.doKernelY Wbase hWobs hWfix Y hY s0) := by
rw [SCM.doKernelY]; infer_instance
have hLegA_ae :
(M.doKernelY X hObs hFix (Wbase.image SWIGNode.random) hWr s0)
=ᵐ[M.treatmentMarginal X hXr s0]
(M.adjustmentKernelY X hObs hFix (Wbase.image SWIGNode.random)
(∅ : Finset (SWIGNode N)) hWr (empty_subset M.observed) s0) :=
ProbabilityTheory.Kernel.ae_eq_of_compProd_eq hLegA
have hLegB_ae :
(M.doKernelY Wbase hWobs hWfix Y hY s0)
=ᵐ[M.treatmentMarginal Wbase hWr s0]
(M.adjustmentKernelY Wbase hWobs hWfix Y (X.image SWIGNode.random) hY hXr s0) :=
ProbabilityTheory.Kernel.ae_eq_of_compProd_eq hLegB
-- Package the FD1 transport lemma. The finite-kernel obstruction is handled
-- by `hLegA_ae`/`hLegB_ae` above; the remaining step is to turn `hG1` into
-- the per-treatment Rule-2 conditional equality for
-- `(M.fixSet X).fixSet Wbase` with empty conditioning, then transport that
-- double intervention to the `do(Wbase)` orientation consumed by `hG2`/Rule 3.
-- This uses the FD1 positivity hypothesis; the remaining ingredient is a
-- reusable structural kernel-transport lemma across the two intervention orders.
have hWobsX : ∀ D ∈ Wbase, SWIGNode.random D ∈ (M.fixSet X hObs hFix).observed := by
intro D hD
simpa [SCM.fixSet_observed] using hWobs D hD
have hDisjBaseXW : Disjoint X Wbase :=
(disjoint_base_of_disjoint_random_image X Wbase hDisj_WrXr).symm
have hWfixX : ∀ D ∈ Wbase, SWIGNode.fixed D ∉ (M.fixSet X hObs hFix).fixed :=
Causalean.SCM.fixSet_fixed_not_mem_of_disjoint M Wbase X hObs hFix hWfix hDisjBaseXW
have hWrX : Wbase.image SWIGNode.random ⊆ (M.fixSet X hObs hFix).observed := by
simpa [SCM.fixSet_observed] using hWr
have hWrEmptyX :
Wbase.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N)) ⊆
(M.fixSet X hObs hFix).observed := by
simpa [union_empty] using hWrX
have hYpost : Y ⊆ (M.fixSet X hObs hFix).observed := by
simpa [SCM.fixSet_observed] using hY
have hR2FD1 (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) :
∀ᵐ p ∂(((M.fixSet X hObs hFix).obsKernel
(M.fixSetExtend X hObs hFix s0 t)).map
(valuesProjection hWrX) ⊗ₘ
const _
(((M.fixSet X hObs hFix).obsKernel
(M.fixSetExtend X hObs hFix s0 t)).map
(valuesProjection (empty_subset _)))),
((M.fixSet X hObs hFix).fixSet Wbase hWobsX hWfixX).obsCondKernel Y
(∅ : Finset (SWIGNode N))
((SCM.fixSet_observed (M.fixSet X hObs hFix) Wbase hWobsX hWfixX).symm ▸ hYpost)
((SCM.fixSet_observed (M.fixSet X hObs hFix) Wbase hWobsX hWfixX).symm ▸
(empty_subset (M.fixSet X hObs hFix).observed))
((M.fixSet X hObs hFix).fixSetExtend Wbase hWobsX hWfixX
(M.fixSetExtend X hObs hFix s0 t) p.1, p.2)
=
(M.fixSet X hObs hFix).obsCondKernel Y
(Wbase.image SWIGNode.random ∪ (∅ : Finset (SWIGNode N)))
hYpost hWrEmptyX
(M.fixSetExtend X hObs hFix s0 t, valuesUnionMk p.1 p.2) := by
exact SCM.do_rule2_kernel_of_nondescendant_product_ae
(M.fixSet X hObs hFix) Wbase hWobsX hWfixX
Y (∅ : Finset (SWIGNode N)) hYpost (empty_subset _)
hWrX hWrEmptyX
(by simpa [hWobsX, hWfixX] using hG1)
(by intro z hz v hv; simpa using hv)
(by intro z hz v hv; simpa using hv)
(M.fixSetExtend X hObs hFix s0 t)
(by
simpa [hWrX, hWrEmptyX] using
hPositivityFD1 (M.fixSetExtend X hObs hFix s0 t))
-- Reduce the joint (compProd) equality to a per-treatment a.e. kernel equality.
haveI : IsFiniteKernel
(M.doKernelY X hObs hFix Y hY s0) := by
rw [SCM.doKernelY]; infer_instance
haveI : IsSFiniteKernel
(M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0) := by
rw [SCM.frontdoorKernelY, SCM.frontdoorAdjustment]; infer_instance
set sT := fun t => M.fixSetExtend X hObs hFix s0 t with hsT
set κ := M.doKernelY X hObs hFix (Wbase.image SWIGNode.random) hWr s0 with hκ_def
set condDoX :
Kernel
((M.fixSet X hObs hFix).FixedValues ×
ValuesOn (Wbase.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
(M.fixSet X hObs hFix).obsCondKernel Y (Wbase.image SWIGNode.random) hYpost hWrX
with hcondDoX_def
have hP1 : ∀ t,
M.doKernelY X hObs hFix Y hY s0 t
= condDoX.sectR (sT t) ∘ₘ κ t := by
-- Now a direct application of the treatment-indexed chain rule.
intro t
rw [hsT, hcondDoX_def, hκ_def]
exact SCM.doKernelY_disintegrate M X hObs hFix Y (Wbase.image SWIGNode.random)
hY hWr s0 t
let xDo : (M.fixSet X hObs hFix).FixedValues →
ValuesOn (X.image SWIGNode.random) (swigΩ Ω) :=
fun s => zFixedAsRandom
(valuesProjection (fixSet_image_fixed_subset M X hObs hFix) s)
have hxDo : Measurable xDo :=
measurable_zFixedAsRandom.comp
(measurable_valuesProjection (fixSet_image_fixed_subset M X hObs hFix))
haveI : IsMarkovKernel
(M.obsCondKernel (Wbase.image SWIGNode.random) (X.image SWIGNode.random) hWr hXr) := by
unfold SCM.obsCondKernel
infer_instance
let zCondXdo :
Kernel (M.fixSet X hObs hFix).FixedValues
(ValuesOn (Wbase.image SWIGNode.random) (swigΩ Ω)) :=
(M.obsCondKernel (Wbase.image SWIGNode.random) (X.image SWIGNode.random) hWr hXr).comap
(fun s => (M.fixSetProj X hObs hFix s, xDo s))
(prodMk (M.measurable_fixSetProj X hObs hFix) hxDo)
haveI : IsSFiniteKernel zCondXdo := by
dsimp [zCondXdo]
infer_instance
let xMarginal :
Kernel (M.fixSet X hObs hFix).FixedValues
(ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) :=
(M.obsKernel.map (valuesProjection hXr)).comap
(M.fixSetProj X hObs hFix)
(M.measurable_fixSetProj X hObs hFix)
let yCondXZ :
Kernel
((M.fixSet X hObs hFix).FixedValues ×
ValuesOn (X.image SWIGNode.random) (swigΩ Ω) ×
ValuesOn (Wbase.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
(M.obsCondKernel Y (X.image SWIGNode.random ∪ Wbase.image SWIGNode.random)
hY hXrW).comap
(fun p =>
(M.fixSetProj X hObs hFix p.1,
valuesUnionMk p.2.1 p.2.2))
(prodMk
((M.measurable_fixSetProj X hObs hFix).comp measurable_fst)
(measurable_valuesUnionMk.comp
(prodMk
(measurable_fst.comp measurable_snd)
(measurable_snd.comp measurable_snd))))
let innerY :
Kernel
((M.fixSet X hObs hFix).FixedValues ×
ValuesOn (Wbase.image SWIGNode.random) (swigΩ Ω))
(ValuesOn Y (swigΩ Ω)) :=
((xMarginal.comap fst measurable_fst) ⊗ₖ
(yCondXZ.comap
(fun q : ((M.fixSet X hObs hFix).FixedValues ×
ValuesOn (Wbase.image SWIGNode.random) (swigΩ Ω)) ×
ValuesOn (X.image SWIGNode.random) (swigΩ Ω) =>
(q.1.1, q.2, q.1.2))
(prodMk
(measurable_fst.comp measurable_fst)
(prodMk measurable_snd
(measurable_snd.comp measurable_fst))))).map Prod.snd
have hP2 : ∀ t,
M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0 t
= innerY.sectR (sT t) ∘ₘ zCondXdo (sT t) := by
intro t
have hfd :
M.frontdoorKernelY X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr s0 t
= M.frontdoorAdjustment X hObs hFix Y (Wbase.image SWIGNode.random) hY hWr
(sT t) := by
rw [SCM.frontdoorKernelY, ProbabilityTheory.Kernel.comap_apply, hsT]
rw [hfd]
change (((zCondXdo ⊗ₖ innerY).map Prod.snd) (sT t))
= innerY.sectR (sT t) ∘ₘ zCondXdo (sT t)
rw [compProd_map_snd_apply]
refine MeasureTheory.Measure.compProd_congr ?_
have hZc : ∀ a,
zCondXdo (sT a)
= M.obsCondKernel (Wbase.image SWIGNode.random) (X.image SWIGNode.random)
hWr hXr (s0, a) := by
intro a
rw [hsT]
-- … truncated; follow the source link for the rest …