SCM.Do.Rule2Kernel
Kernel-level proof of do-calculus Rule 2: conditional kernels under intervention, levelset compatibility, and the rectangle-identity bridge.
Structural 3 core · 6 supporting · 2 submodules Structural helpers for Rule 2 kernels: cross-SCM compatibility and pointwise structural identities behind the kernel-level argument. WitnessBridge 5 core · 5 supporting · 3 submodules The analytic core of Rule 2 of the do-calculus for treatments with arbitrary (possibly continuous) values.
Helpers 6 core · 7 supporting This file builds the value-space maps that insert intervention values into a conditioning assignment. ★ fixSetProj_fixSetExtend★ fillZrW_fixSetExtend
Value-Space Helpers for Rule 2
This file builds the value-space maps that insert intervention values into a conditioning assignment. These maps provide the bookkeeping needed to compare conditioning on an observed random copy with conditioning on the corresponding intervention value in Rule 2.
def zFixedAsRandom reviewed
⚑ flagged
Causalean.SCM
For a set of treatment-variable names and an assignment to their intervention copies, the intervention-to-random value map is the assignment to the corresponding random copies that for a random copy returns the value of its matching intervention copy and has no possible fixed-copy case](step:2).
Definition (Lean source)
parameters
given by
fun ⟨v, hv⟩
=> match v, hv with | SWIGNode.random D, hv => have hD : D ∈ Z := by rcases Finset.mem_image.mp hv with ⟨D', hD', heq⟩ cases heq; exact hD' z ⟨SWIGNode.fixed D, Finset.mem_image.mpr ⟨D, hD, rfl⟩⟩ | SWIGNode.fixed _, hv => by exfalso rcases Finset.mem_image.mp hv with ⟨_, _, heq⟩ cases heq
def fillZrW reviewed
⚑ flagged
Causalean.SCM
For a structural causal model, a set of treatment-variable names, the condition that each corresponding random copy is observed, the condition that none of their fixed copies is already fixed, a set of conditioning nodes, and a fixed-value assignment for the model after fixing those treatments, the Rule 2 filler maps each conditioning assignment to an assignment on the union of the treatment random copies and conditioning nodes, inserting the treatment values from the fixed-value assignment; on any overlap, the treatment values take priority.
Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
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
def
given by
fun w
=> valuesUnionMk (zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s')) w
def xRandomAsFixed reviewed
⚑ flagged
Causalean.SCM
For a set of treatment-variable names and an assignment to their random copies, the random-to-intervention value map is the assignment to the corresponding intervention copies that for an intervention copy returns the value of its matching random copy and has no possible random-copy case](step:2).
Definition (Lean source)
parameters
given by
fun ⟨v, hv⟩
=> match v, hv with | SWIGNode.fixed D, hv => have hD : D ∈ X := by rcases Finset.mem_image.mp hv with ⟨D', hD', heq⟩; cases heq; exact hD' t ⟨SWIGNode.random D, Finset.mem_image.mpr ⟨D, hD, rfl⟩⟩ | SWIGNode.random _, hv => by exfalso; rcases Finset.mem_image.mp hv with ⟨_, _, heq⟩; cases heq
def fixSetExtend reviewed
⚑ flagged
Causalean.SCM
For a structural causal model, a set of treatment-variable names, the condition that each corresponding random copy is observed, the condition that none of their fixed copies is already fixed, an assignment on the model's original fixed nodes, and an assignment to the treatment random copies, the extended fixed-value assignment is the fixed-value assignment for the model after those treatments are fixed, retaining original fixed values and using the matching treatment values for newly fixed copies.
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
s0 :
M.FixedValues
def
given by
fun ⟨v, hv⟩
=> if hM : v ∈ M.fixed then s0 ⟨v, hM⟩ else have hXf : v ∈ X.image SWIGNode.fixed := (Finset.mem_union.mp (by simpa using hv)).resolve_left hM xRandomAsFixed t ⟨v, hXf⟩
lemma fixSetProj_fixSetExtend reviewed
⚑ flagged
Causalean.SCM
For the intervention names X, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, projecting the extended post-intervention fixed assignment — built from the base assignment s0 and treatment value t — back onto the original fixed coordinates recovers s0.
Formal statement
Proof (Lean source)
lemma fixSetProj_fixSetExtend (M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) :
M.fixSetProj X hObs hFix (M.fixSetExtend X hObs hFix s0 t) = s0 := by
funext ⟨v, hv⟩
simp only [fixSetProj, valuesProjection, fixSetExtend, dif_pos hv]
lemma fillZrW_fixSetExtend reviewed
⚑ flagged
Causalean.SCM
For the intervention names X, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, filling the conditioning assignment z against the extended post-intervention fixed assignment built from the base assignment s0 and treatment value t equals directly combining t and z into one assignment on their union.
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
s0 :
M.FixedValues
conclusion
M.fillZrW X hObs hFix Z (M.fixSetExtend X hObs hFix s0 t) z = valuesUnionMk t z
Proof (Lean source)
lemma fillZrW_fixSetExtend
(M : SCM N Ω) (X : Finset N)
(hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed)
(hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed)
(Z : Finset (SWIGNode N))
(s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω))
(z : ValuesOn Z (swigΩ Ω)) :
M.fillZrW X hObs hFix Z (M.fixSetExtend X hObs hFix s0 t) z
= valuesUnionMk t z := by
rw [SCM.fillZrW, SCM.zFixedAsRandom_proj_fixSetExtend]
7 supporting declarations (lemmas, instances)
-
measurable_zFixedAsRandomlemma — Reading intervention values as random-copy values is a measurable operation.Proof (Lean source)
@[fun_prop] lemma measurable_zFixedAsRandom {Z : Finset N} : Measurable (zFixedAsRandom (Ω := Ω) (Z := Z)) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ obtain ⟨D, hD, rfl⟩ := Finset.mem_image.mp hv -- v = SWIGNode.random D; output is `z ⟨.fixed D, _⟩` exact measurable_pi_apply _ -
measurable_fillZrWtheorem — The Rule 2 filler is measurable as a function of the free conditioning assignment.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixeds' :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesconclusionMeasurable (M'.fillZrW Z hZ_obs hZ_fixed W s')Proof (Lean source)
@[fun_prop] theorem measurable_fillZrW (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (W : Finset (SWIGNode N)) (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) : Measurable (M'.fillZrW Z hZ_obs hZ_fixed W s') := by unfold fillZrW exact measurable_valuesUnionMk_right _ -
measurable_fillZrW_prodtheorem — The Rule 2 filler is jointly measurable in the post-intervention fixed slice and the free conditioning coordinates.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedconclusionMeasurable (fun p : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues × ValuesOn W (swigΩ Ω) => M'.fillZrW Z hZ_obs hZ_fixed W p.1 p.2)Proof (Lean source)
@[fun_prop] theorem measurable_fillZrW_prod (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (W : Finset (SWIGNode N)) : Measurable (fun p : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues × ValuesOn W (swigΩ Ω) => M'.fillZrW Z hZ_obs hZ_fixed W p.1 p.2) := by unfold fillZrW change Measurable ((fun q : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) × ValuesOn W (swigΩ Ω) => valuesUnionMk q.1 q.2) ∘ (fun p : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues × ValuesOn W (swigΩ Ω) => (zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) p.1), p.2))) refine (measurable_valuesUnionMk (Ω := swigΩ Ω) (A := Z.image SWIGNode.random) (B := W)).comp ?_ refine prodMk ?_ measurable_snd exact measurable_zFixedAsRandom.comp ((measurable_valuesProjection _).comp measurable_fst) -
measurable_xRandomAsFixedlemma — Reading observed treatment values as intervention-coordinate values is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_xRandomAsFixed {X : Finset N} : Measurable (xRandomAsFixed (Ω := Ω) (X := X)) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ obtain ⟨D, hD, rfl⟩ := Finset.mem_image.mp hv exact measurable_pi_apply _ -
fixSetExtend_apply_new_fixedlemma — A newly fixed coordinate in fixSetExtend reads the matching observed intervention coordinate.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.fixeds0 :M.FixedValuesD :NhD :D ∈ XconclusionM.fixSetExtend X hObs hFix s0 t ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M X hObs hFix hD⟩= t ⟨SWIGNode.random D, Finset.mem_image.mpr ⟨D, hD, rfl⟩⟩Proof (Lean source)
@[simp] lemma fixSetExtend_apply_new_fixed (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) {D : N} (hD : D ∈ X) : M.fixSetExtend X hObs hFix s0 t ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M X hObs hFix hD⟩ = t ⟨SWIGNode.random D, Finset.mem_image.mpr ⟨D, hD, rfl⟩⟩ := by simp [fixSetExtend, hFix D hD, xRandomAsFixed] -
measurable_fixSetExtendlemma — Extending a base fixed-value assignment is measurable in the treatment value when the base assignment is held fixed.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.fixeds0 :M.FixedValuesconclusionMeasurable (M.fixSetExtend X hObs hFix s0)Proof (Lean source)
@[fun_prop] lemma measurable_fixSetExtend (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (s0 : M.FixedValues) : Measurable (M.fixSetExtend X hObs hFix s0) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ by_cases hM : v ∈ M.fixed · simp only [fixSetExtend, dif_pos hM]; exact measurable_const · have hXf : v ∈ X.image SWIGNode.fixed := (Finset.mem_union.mp (by simpa using hv)).resolve_left hM have : (fun t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω) => M.fixSetExtend X hObs hFix s0 t ⟨v, hv⟩) = fun t => xRandomAsFixed t ⟨v, hXf⟩ := by funext t; simp only [fixSetExtend, dif_neg hM] rw [this] exact (measurable_xRandomAsFixed).eval -
zFixedAsRandom_proj_fixSetExtendlemma — Relabeling the treatment part of the extended fixed assignment back to observed coordinates recovers the treatment assignment.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.fixeds0 :M.FixedValuesconclusionSCM.zFixedAsRandom (valuesProjection (SCM.fixSet_image_fixed_subset M X hObs hFix) (M.fixSetExtend X hObs hFix s0 t))= tProof (Lean source)
lemma zFixedAsRandom_proj_fixSetExtend (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (s0 : M.FixedValues) (t : ValuesOn (X.image SWIGNode.random) (swigΩ Ω)) : SCM.zFixedAsRandom (valuesProjection (SCM.fixSet_image_fixed_subset M X hObs hFix) (M.fixSetExtend X hObs hFix s0 t)) = t := by funext ⟨v, hv⟩ obtain ⟨D, hD, rfl⟩ := Finset.mem_image.mp hv -- LHS unfolds: zFixedAsRandom at .random D reads the .fixed D coordinate. simp only [SCM.zFixedAsRandom, valuesProjection] -- The .fixed D coordinate of fixSetExtend: .fixed D ∉ M.fixed, so it is -- xRandomAsFixed t ⟨.fixed D, _⟩ = t ⟨.random D, _⟩. have hMf : SWIGNode.fixed D ∉ M.fixed := hFix D hD simp only [SCM.fixSetExtend, dif_neg hMf, SCM.xRandomAsFixed]
DiscreteZHelpers 1 core · 2 supporting This file provides the discrete-treatment measure-theoretic helpers used to state Pearl's action-observation exchange without requiring the post-intervention treatment coordinate to be almost surely pinned. ★ obsKernel_fixSet_W_marginal_eq_M1_marginal
Discrete Treatment Helpers for Rule 2
This file provides the discrete-treatment measure-theoretic helpers used to state
Pearl's action-observation exchange without requiring the post-intervention
treatment coordinate to be almost surely pinned. It proves the W-marginal
equality obsKernel_fixSet_W_marginal_eq_M1_marginal, the filled-assignment
pullback equality mu_C_comap_F_eq_nu_C_comap_F, and the discrete conditional
kernel bridge obsCondKernel_cross_eq_ae_of_discrete. Together these connect
post-intervention adjustment marginals to pre-intervention joint marginals using
overlap, positivity, and the non-descendance condition needed for the Rule 3*
marginal step.
theorem obsKernel_fixSet_W_marginal_eq_M1_marginal reviewed
⚑ flagged
Causalean.SCM
**Rule 3* W-marginal equality for Rule 2.** For the intervention on names Z, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, and a conditioning set W contained in the observed variables, if no fixed copy of a name in Z is an ancestor, in the post-intervention DAG, of any node in W, then the W-marginal of the intervened model's observational kernel at a fixed assignment s equals the W-marginal of the base model's observational kernel at the corresponding projected assignment.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
hW :
W ⊆ M'.observed
hWNonDesc :
∀ z ∈ Z, ∀ v ∈ W, ¬ (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 ▸ hW))
= (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map (valuesProjection hW)
Proof (Lean source)
theorem obsKernel_fixSet_W_marginal_eq_M1_marginal
(M' : SCM N Ω) (Z : Finset N)
(hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed)
(hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed)
(W : Finset (SWIGNode N)) (hW : W ⊆ M'.observed)
(hWNonDesc : ∀ z ∈ Z, ∀ v ∈ W,
¬ (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 ▸ hW))
= (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map
(valuesProjection hW) := by
-- Rule 3* specialised to `T := W`: the W-marginal of the intervention
-- kernel equals the W-marginal of the original kernel, because no z ∈ Z
-- has `.fixed z` as ancestor of any v ∈ W in the post-intervention DAG.
exact condDistrib_intervention_ancestral_eq M' Z hZ_obs hZ_fixed W hW
(fun z hz v hv => hWNonDesc z hz v hv) s
2 supporting declarations (lemmas, instances)
-
mu_C_comap_F_eq_nu_C_comap_Flemma — Cross-SCM pullback equality along the filled assignment.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhZrW :Z.image SWIGNode.random ∪ W ⊆ M'.observedhDisj_ZrW :Disjoint (Z.image SWIGNode.random) Ws :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesconclusion((M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map (valuesProjection (Ω := swigΩ Ω) hZrW)).comap (M'.fillZrW Z hZ_obs hZ_fixed W s)= (((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s).map (valuesProjection (Ω := swigΩ Ω) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))).comap (M'.fillZrW Z hZ_obs hZ_fixed W s)Proof (Lean source)
lemma mu_C_comap_F_eq_nu_C_comap_F (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (W : Finset (SWIGNode N)) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) (hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W) [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) : ((M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map (valuesProjection (Ω := swigΩ Ω) hZrW)).comap (M'.fillZrW Z hZ_obs hZ_fixed W s) = (((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s).map (valuesProjection (Ω := swigΩ Ω) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))).comap (M'.fillZrW Z hZ_obs hZ_fixed W s) := by classical let M2 := M'.fixSet Z hZ_obs hZ_fixed let sM1 : M'.FixedValues := M'.fixSetProj Z hZ_obs hZ_fixed s let F := M'.fillZrW Z hZ_obs hZ_fixed W s have hZrW_M2 : Z.image SWIGNode.random ∪ W ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW have hF_emb : MeasurableEmbedding F := measurableEmbedding_fillZrW M' Z hZ_obs hZ_fixed W hDisj_ZrW s have hπC_M1 : Measurable (valuesProjection (Ω := swigΩ Ω) hZrW : M'.ObservedValues → _) := measurable_valuesProjection _ have hπC_M2 : Measurable (valuesProjection (Ω := swigΩ Ω) hZrW_M2 : M2.ObservedValues → _) := measurable_valuesProjection _ refine MeasureTheory.Measure.ext (fun A_W hA_W => ?_) rw [hF_emb.comap_apply, hF_emb.comap_apply] have hImg_meas : MeasurableSet (F '' A_W) := hF_emb.measurableSet_image' hA_W rw [MeasureTheory.Measure.map_apply hπC_M1 hImg_meas, MeasureTheory.Measure.map_apply hπC_M2 hImg_meas] have hBridge : M2.obsKernel s (univ ∩ (valuesProjection hZrW_M2)⁻¹' (F '' A_W)) = M'.obsKernel sM1 (univ ∩ (valuesProjection hZrW)⁻¹' (F '' A_W)) := obsKernel_inter_Wset_Zrand_levelset_eq M' Z hZ_obs hZ_fixed W hZrW hDisj_ZrW s MeasurableSet.univ hA_W rw [Set.univ_inter, Set.univ_inter] at hBridge exact hBridge.symm -
obsCondKernel_cross_eq_ae_of_discretelemma — Discrete-treatment cross-SCM conditional-kernel equality. For an intervention target whose random copies are observed and fixed copies are not already fixed, observed outcome and conditioning blocks, and an observed union of the target's random copies with the conditioning block, assume the post-intervention d-separation premise and non-descendancy of the conditioning block. At a post-intervention fixed assignment, if the base conditioning marginal is absolutely continuous with respect to the pullback of the base joint marginal and the outcome event is measurable, then the base and post-intervention conditional kernels agree almost everywhere under the post-intervention conditioning marginal.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhY :Y ⊆ M'.observedhW :W ⊆ M'.observedhZrW :Z.image SWIGNode.random ∪ W ⊆ M'.observed∀ n, StandardBorelSpace (swigΩ Ω n)∀ n, Nonempty (swigΩ Ω n)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) vStandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).RandomValuesStandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).ObservedValues∀ s : M'.FixedValues, IsFiniteMeasure (M'.obsKernel s)∀ s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues,IsFiniteMeasure ((M'.fixSet Z hZ_obs hZ_fixed).jointKernel s)∀ s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues,IsFiniteMeasure ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s)CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))s :(M'.fixSet Z hZ_obs hZ_fixed).FixedValueshPositivity :((M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map (valuesProjection (Ω := swigΩ Ω) hW)) ≪ (((M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map (valuesProjection (Ω := swigΩ Ω) hZrW)).comap (M'.fillZrW Z hZ_obs hZ_fixed W s))hB :conclusion∀ᵐ w ∂(((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s).map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW))), (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (M'.fixSetProj Z hZ_obs hZ_fixed s, M'.fillZrW Z hZ_obs hZ_fixed W s w)) B= ((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)) BProof (Lean source)
lemma obsCondKernel_cross_eq_ae_of_discrete (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) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] (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) [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).RandomValues] [StandardBorelSpace (M'.fixSet Z hZ_obs hZ_fixed).ObservedValues] [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [StandardBorelSpace (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [Nonempty (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))] [∀ s : M'.FixedValues, IsFiniteMeasure (M'.obsKernel s)] [∀ s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues, IsFiniteMeasure ((M'.fixSet Z hZ_obs hZ_fixed).jointKernel s)] [∀ s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues, IsFiniteMeasure ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s)] [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Ω Ω))] (s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) (hPositivity : ((M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map (valuesProjection (Ω := swigΩ Ω) hW)) ≪ (((M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s)).map (valuesProjection (Ω := swigΩ Ω) hZrW)).comap (M'.fillZrW Z hZ_obs hZ_fixed W s))) {B : Set (ValuesOn Y (swigΩ Ω))} (hB : MeasurableSet B) : ∀ᵐ w ∂(((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s).map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW))), (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (M'.fixSetProj Z hZ_obs hZ_fixed s, M'.fillZrW Z hZ_obs hZ_fixed W s w)) B = ((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)) B := by classical -- Abbreviations. let M2 := M'.fixSet Z hZ_obs hZ_fixed let sM1 : M'.FixedValues := M'.fixSetProj Z hZ_obs hZ_fixed s let F := M'.fillZrW Z hZ_obs hZ_fixed W s have hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W := Disjoint.mono_right Finset.subset_union_left hdSep.2.2.1 have hY_M2 : Y ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY have hW_M2 : W ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW have hZrW_M2 : Z.image SWIGNode.random ∪ W ⊆ M2.observed := (fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW have hF_emb : MeasurableEmbedding F := measurableEmbedding_fillZrW M' Z hZ_obs hZ_fixed W hDisj_ZrW s -- Marginal measures. let μ_C : Measure (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω)) := (M'.obsKernel sM1).map (valuesProjection hZrW) let ν_C : Measure (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω)) := (M2.obsKernel s).map (valuesProjection hZrW_M2) let μ_W : Measure (ValuesOn W (swigΩ Ω)) := (M'.obsKernel sM1).map (valuesProjection (Ω := swigΩ Ω) hW) let ν_W : Measure (ValuesOn W (swigΩ Ω)) := (M2.obsKernel s).map (valuesProjection (Ω := swigΩ Ω) hW_M2) have hμC_def : μ_C = (M'.obsKernel sM1).map (valuesProjection (Ω := swigΩ Ω) hZrW) := rfl have hνC_def : ν_C = (M2.obsKernel s).map (valuesProjection (Ω := swigΩ Ω) hZrW_M2) := rfl -- (1) Cross-SCM bridge: μ_C.comap F-a.e. w, M1.obsCondKernel(C)(sM1, F w) B -- = M2.obsCondKernel(C)(s, F w) B. have h_L2 := obsCondKernel_cross_SCM_ae_eq_on_fillZrW M' Z hZ_obs hZ_fixed Y W hY hZrW hDisj_ZrW s hB -- (2) D-sep collapse: ν_C-a.e. c, M2.obsCondKernel(C)(s, c) B -- = M2.obsCondKernel(W)(s, π_W^C c) B. have h_L1 := obsCondKernel_dSep_collapse_ae M' Z hZ_obs hZ_fixed Y W hY hW hdSep s (B := B) -- (3) Pullback equality: μ_C.comap F = ν_C.comap F. have hPartA : μ_C.comap F = ν_C.comap F := mu_C_comap_F_eq_nu_C_comap_F M' Z hZ_obs hZ_fixed W hZrW hDisj_ZrW s -- (4) Rule 3* marginal equality: ν_W = μ_W as measures. have hν_W_eq_μ_W : ν_W = μ_W := by change (M2.obsKernel s).map (valuesProjection hW_M2) = (M'.obsKernel sM1).map (valuesProjection hW) exact obsKernel_fixSet_W_marginal_eq_M1_marginal M' Z hZ_obs hZ_fixed W hW hWNonDesc s -- (5) Transport h_L1 from ν_C-a.e. (in `c`) to ν_C.comap F-a.e. (in `w`, -- with `c := F w`). Step (5a): ν_C-a.e. → ν_C.restrict (range F)-a.e. have h_L1_restrict : ∀ᵐ c ∂(ν_C.restrict (range F)), (M2.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY_M2 hZrW_M2 (s, c)) B = (M2.obsCondKernel Y W hY_M2 hW_M2 (s, valuesProjection (Finset.subset_union_right (s₁ := Z.image SWIGNode.random) (s₂ := W)) c)) B := MeasureTheory.ae_restrict_of_ae h_L1 -- (5b): ν_C.restrict (range F) = (ν_C.comap F).map F (`hF_emb.map_comap`). have h_map_comap_ν : (ν_C.comap F).map F = ν_C.restrict (range F) := hF_emb.map_comap ν_C rw [← h_map_comap_ν] at h_L1_restrict -- (5c): Pull back through F via MeasurableEmbedding.ae_map_iff. have h_L1_pulled : ∀ᵐ w ∂(ν_C.comap F), (M2.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY_M2 hZrW_M2 (s, F w)) B = (M2.obsCondKernel Y W hY_M2 hW_M2 (s, valuesProjection (Finset.subset_union_right (s₁ := Z.image SWIGNode.random) (s₂ := W)) (F w))) B := (hF_emb.ae_map_iff (μ := ν_C.comap F) (p := fun c => (M2.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY_M2 hZrW_M2 (s, c)) B = (M2.obsCondKernel Y W hY_M2 hW_M2 (s, valuesProjection (Finset.subset_union_right (s₁ := Z.image SWIGNode.random) (s₂ := W)) c)) B)).mp h_L1_restrict -- (6) `π_W^C (F w) = w`, by construction of F. have h_proj_F : ∀ w : ValuesOn W (swigΩ Ω), valuesProjection (Finset.subset_union_right (s₁ := Z.image SWIGNode.random) (s₂ := W)) (F w) = w := by intro w funext ⟨v, hvW⟩ have hv_in : v ∈ Z.image SWIGNode.random ∪ W := Finset.subset_union_right hvW have hvNotZr : v ∉ Z.image SWIGNode.random := fun hvZr => Finset.disjoint_left.mp hDisj_ZrW hvZr hvW simp only [valuesProjection, F, fillZrW] rw [valuesUnionMk_apply_right _ _ hv_in hvNotZr] -- (7) Simplify h_L1_pulled using h_proj_F. have h_L1_simpl : ∀ᵐ w ∂(ν_C.comap F), (M2.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY_M2 hZrW_M2 (s, F w)) B = (M2.obsCondKernel Y W hY_M2 hW_M2 (s, w)) B := by refine Filter.Eventually.mono h_L1_pulled (fun w hw => ?_) rw [h_proj_F] at hw exact hw -- (8) Combine h_L2 (μ_C.comap F-a.e.) with h_L1_simpl (ν_C.comap F-a.e.), -- using the pullback equality to identify the two measures. have h_L1_simpl_μ : ∀ᵐ w ∂(μ_C.comap F), (M2.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY_M2 hZrW_M2 (s, F w)) B = (M2.obsCondKernel Y W hY_M2 hW_M2 (s, w)) B := by rw [hPartA]; exact h_L1_simpl have h_chain_μ : ∀ᵐ w ∂(μ_C.comap F), (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (sM1, F w)) B = (M2.obsCondKernel Y W hY_M2 hW_M2 (s, w)) B := by filter_upwards [h_L2, h_L1_simpl_μ] with w hL2 hL1 exact hL2.trans hL1 -- (9) Transport from μ_C.comap F-a.e. to μ_W-a.e. via hPositivity. have h_chain_μW : ∀ᵐ w ∂μ_W, (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (sM1, F w)) B = (M2.obsCondKernel Y W hY_M2 hW_M2 (s, w)) B := hPositivity.ae_eq h_chain_μ -- (10) Rewrite the goal's measure ν_W to μ_W via the Rule 3* marginal equality. change ∀ᵐ w ∂ν_W, _ rw [hν_W_eq_μ_W] exact h_chain_μW
InterSingleton 1 core · 2 supporting This file proves that, on the event where the treatment and adjustment coordinates take the fixed value inserted by the intervention, the post-intervention observational kernel and the original observational kernel assig ★ obsKernel_inter_Wset_Zrand_levelset_eq
Level-Set Agreement for Rule 2
This file proves that, on the event where the treatment and adjustment coordinates take the fixed value inserted by the intervention, the post-intervention observational kernel and the original observational kernel assign the same mass to every additional measurable observed event. This level-set identity is the cross-model cylinder equality used in the disintegration argument for Rule 2.
theorem obsKernel_inter_Wset_Zrand_levelset_eq reviewed
⚑ flagged
Causalean.SCM
For the intervention on names Z, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, with the union of the random copies of Z and a conditioning set W contained in the observed variables and the random copies of Z disjoint from W, fix an intervened fixed assignment s'; for measurable subsets S of the observed-value space and measurable subsets A of the values on W, the intervened model's observational kernel at s', evaluated on S intersected with the preimage under the Z.random ∪ W-projection of the image of A under the filled-assignment map, equals the base model's observational kernel at the projected fixed assignment, evaluated on the analogous set.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
hZrW :
Z.image SWIGNode.random ∪ W ⊆ M'.observed
hDisj_ZrW :
Disjoint (Z.image SWIGNode.random) W
s' :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
S :
Set M'.ObservedValues
hS :
hA :
conclusion
(M'.fixSet Z hZ_obs hZ_fixed).obsKernel s' (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' ((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))
= M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s') (S ∩ (valuesProjection hZrW)⁻¹' ((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))
Proof (Lean source)
theorem obsKernel_inter_Wset_Zrand_levelset_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)
(W : Finset (SWIGNode N))
(hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed)
(hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W)
[MeasurableSingletonClass
(ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))]
(s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues)
{S : Set M'.ObservedValues} {A : Set (ValuesOn W (swigΩ Ω))}
(hS : MeasurableSet S) (hA : MeasurableSet A) :
(M'.fixSet Z hZ_obs hZ_fixed).obsKernel s'
(S ∩ (valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))
= M'.obsKernel
(M'.fixSetProj Z hZ_obs hZ_fixed s')
(S ∩ (valuesProjection hZrW)⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A)) := by
classical
-- Abbreviations.
let M1 := M'
let M2 := M1.fixSet Z hZ_obs hZ_fixed
have hZrW_M2 : Z.image SWIGNode.random ∪ W ⊆ M2.observed :=
(fixSet_observed M1 Z hZ_obs hZ_fixed).symm ▸ hZrW
let s_M1 : M1.FixedValues := M1.fixSetProj Z hZ_obs hZ_fixed s'
let F := M'.fillZrW Z hZ_obs hZ_fixed W s'
-- Measurability bookkeeping for the image preimage.
have hF_meas : Measurable F := by fun_prop
-- The image `F '' A` has the explicit form
-- `{c | π_W^C c ∈ A ∧ π_Zr^C c = ζ_s}`
-- which is measurable. Use this to deduce the cylinder
-- `π_C⁻¹ (F '' A)` is measurable.
have hπ_M1 : Measurable (valuesProjection hZrW : M1.ObservedValues → _) := by fun_prop
have hπ_M2 : Measurable (valuesProjection hZrW_M2 : M2.ObservedValues → _) := by fun_prop
-- Helper: the Zr-singleton `{ζ_s}` is measurable in
-- `ValuesOn (Z.image .random) (swigΩ Ω)` provided we have a witness
-- `w₀ : ValuesOn W (swigΩ Ω)`. We isolate this as a parameterized lemma.
-- The proof: pull back the measurable singleton
-- `{valuesUnionMk ζ_s w₀} ⊆ ValuesOn (Zr ∪ W) (swigΩ Ω)` (which is
-- measurable by the MSC hypothesis) under the measurable embedding
-- `ζ ↦ valuesUnionMk ζ w₀`.
let ζ_s : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) :=
zFixedAsRandom
(valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s')
have hSingZr : ∀ (w₀ : ValuesOn W (swigΩ Ω)),
MeasurableSet ({ζ_s} : Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))) := by
intro w₀
have hmeas : Measurable
(fun ζ : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) =>
valuesUnionMk ζ w₀) := by fun_prop
have h_pre : ({ζ_s} : Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))) =
(fun ζ => valuesUnionMk ζ w₀)⁻¹' ({valuesUnionMk ζ_s w₀} :
Set (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))) := by
ext ζ
simp only [Set.mem_singleton_iff, Set.mem_preimage]
refine ⟨fun h => by rw [h], fun h => ?_⟩
funext ⟨v, hv⟩
have hv_union : v ∈ Z.image SWIGNode.random ∪ W :=
subset_union_left hv
have h_coord := congrFun h ⟨v, hv_union⟩
rw [valuesUnionMk_apply_left _ _ hv,
valuesUnionMk_apply_left _ _ hv] at h_coord
exact h_coord
rw [h_pre]
exact hmeas (measurableSet_singleton _)
-- Helper: prove `MeasurableSet ((valuesProjection h)⁻¹' (F '' A))` via the
-- `hImg` decomposition. The proof is identical for `h = hZrW` (M1 side)
-- and `h = hZrW_M2` (M2 side); we factor it.
have hPreImage_meas_gen :
∀ {O : Finset (SWIGNode N)} (h : Z.image SWIGNode.random ∪ W ⊆ O)
(hπ : Measurable
(valuesProjection h : ValuesOn O (swigΩ Ω) → _)),
MeasurableSet ((valuesProjection h)⁻¹' (F '' A)) := by
intro O h hπ
by_cases hW : Nonempty (ValuesOn W (swigΩ Ω))
· obtain ⟨w₀⟩ := hW
have hImg : (F '' A : Set _) =
(fun c : ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) =>
valuesProjection
(Finset.subset_union_right (s₁ := Z.image SWIGNode.random)) c)⁻¹' A ∩
(fun c => valuesProjection
(subset_union_left (s₂ := W)) c)⁻¹'
({ζ_s} :
Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))) := by
ext c
constructor
· rintro ⟨w, hwA, rfl⟩
refine ⟨?_, ?_⟩
· simp only [Set.mem_preimage]
show valuesProjection (Finset.subset_union_right) (F w) ∈ A
have : valuesProjection (Finset.subset_union_right : W ⊆ _) (F w) = w := by
funext ⟨v, hv⟩
simp only [valuesProjection, F, fillZrW]
by_cases hvA : v ∈ Z.image SWIGNode.random
· exfalso
exact Finset.disjoint_left.mp hDisj_ZrW hvA hv
· rw [valuesUnionMk_apply_right _ _ _ hvA]
rw [this]
exact hwA
· simp only [Set.mem_preimage, Set.mem_singleton_iff]
show valuesProjection (subset_union_left) (F w) = ζ_s
funext ⟨v, hv⟩
simp only [valuesProjection, F, fillZrW]
rw [valuesUnionMk_apply_left _ _ hv]
· rintro ⟨hW_mem, hZr_mem⟩
simp only [Set.mem_preimage] at hW_mem
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hZr_mem
refine ⟨valuesProjection (Finset.subset_union_right : W ⊆ _) c, hW_mem, ?_⟩
funext ⟨v, hv⟩
simp only [F, fillZrW]
rcases Finset.mem_union.mp hv with hZrV | hWV
· rw [valuesUnionMk_apply_left _ _ hZrV]
have := congrFun hZr_mem ⟨v, hZrV⟩
simp only [valuesProjection] at this
exact this.symm
· by_cases hZrV' : v ∈ Z.image SWIGNode.random
· rw [valuesUnionMk_apply_left _ _ hZrV']
have := congrFun hZr_mem ⟨v, hZrV'⟩
simp only [valuesProjection] at this
exact this.symm
· rw [valuesUnionMk_apply_right _ _ _ hZrV']
simp only [valuesProjection]
rw [hImg, Set.preimage_inter]
refine (hπ ((measurable_valuesProjection _) hA)).inter ?_
exact hπ ((measurable_valuesProjection _) (hSingZr w₀))
· -- `ValuesOn W` is empty. Then `A : Set (ValuesOn W)` must be `∅`,
-- hence `F '' A = ∅` and the preimage is empty (measurable).
have hA_empty : A = ∅ := by
ext w
exact ⟨fun _ => (hW ⟨w⟩).elim, fun h => h.elim⟩
rw [hA_empty, Set.image_empty, Set.preimage_empty]
exact MeasurableSet.empty
have hPreImage_meas_M1 : MeasurableSet ((valuesProjection hZrW)⁻¹' (F '' A)) :=
hPreImage_meas_gen hZrW hπ_M1
have hPreImage_meas_M2 : MeasurableSet ((valuesProjection hZrW_M2)⁻¹' (F '' A)) :=
hPreImage_meas_gen hZrW_M2 hπ_M2
-- LHS: unfold obsKernel → jointKernel → latentProduct.map evalMap.
unfold obsKernel
have hI_M2_exp : MeasurableSet
(S ∩ (valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A)) :=
hS.inter hPreImage_meas_M2
have hI_M1_exp : MeasurableSet
(S ∩ (valuesProjection hZrW)⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A)) :=
hS.inter hPreImage_meas_M1
rw [ProbabilityTheory.Kernel.map_apply _
((M'.fixSet Z hZ_obs hZ_fixed).measurable_randomToObserved),
ProbabilityTheory.Kernel.map_apply _ M'.measurable_randomToObserved]
have hmap_M2 :
(map (M'.fixSet Z hZ_obs hZ_fixed).randomToObserved
((M'.fixSet Z hZ_obs hZ_fixed).jointKernel s'))
(S ∩ (valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))
= ((M'.fixSet Z hZ_obs hZ_fixed).jointKernel s')
((M'.fixSet Z hZ_obs hZ_fixed).randomToObserved ⁻¹'
(S ∩ (valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))) :=
MeasureTheory.Measure.map_apply
((M'.fixSet Z hZ_obs hZ_fixed).measurable_randomToObserved) hI_M2_exp
have hmap_M1 :
(map M'.randomToObserved
(M'.jointKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')))
(S ∩ (valuesProjection hZrW)⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))
= (M'.jointKernel (M'.fixSetProj Z hZ_obs hZ_fixed s'))
(M'.randomToObserved ⁻¹'
(S ∩ (valuesProjection hZrW)⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))) :=
MeasureTheory.Measure.map_apply M'.measurable_randomToObserved hI_M1_exp
rw [hmap_M2, hmap_M1,
jointKernel_apply_eq (M'.fixSet Z hZ_obs hZ_fixed) s',
jointKernel_apply_eq M' (M'.fixSetProj Z hZ_obs hZ_fixed s')]
have hf_M2_exp : Measurable
(fun ℓ : (M'.fixSet Z hZ_obs hZ_fixed).LatentValues =>
(M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ) := by fun_prop
have hf_M1_exp : Measurable
(fun ℓ : M'.LatentValues =>
M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') ℓ) := by fun_prop
have hRTO_2 : Measurable (M'.fixSet Z hZ_obs hZ_fixed).randomToObserved := by fun_prop
have hRTO_1 : Measurable M'.randomToObserved := by fun_prop
have hpre_M2 : MeasurableSet
((M'.fixSet Z hZ_obs hZ_fixed).randomToObserved ⁻¹'
(S ∩ (valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))) :=
hRTO_2 hI_M2_exp
have hpre_M1 : MeasurableSet
(M'.randomToObserved ⁻¹'
(S ∩ (valuesProjection hZrW)⁻¹'
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A))) :=
hRTO_1 hI_M1_exp
rw [MeasureTheory.Measure.map_apply hf_M2_exp hpre_M2,
MeasureTheory.Measure.map_apply hf_M1_exp hpre_M1,
← fixSet_latentProduct_compat M' Z hZ_obs hZ_fixed,
MeasureTheory.Measure.map_apply (measurable_valuesProjection _)
(hf_M1_exp hpre_M1)]
-- Reduce to set equality on the same M2.latentProduct (now post-cast on RHS).
congr 1
apply Set.eq_of_subset_of_subset
all_goals
intro ℓ hℓ
simp only [Set.mem_preimage, Set.mem_inter_iff] at hℓ ⊢
· -- ⊆: LHS (M2-side) ⊆ RHS (M1-side via cast).
rcases hℓ with ⟨hS_mem, hπ_mem⟩
rcases hπ_mem with ⟨w₀, hw₀A, hF_eq⟩
-- Extract LS_M2 from the cylinder constraint hF_eq: the M2-side
-- projection at each `.random D` equals the Z-slice of `s'`.
have hLS_M2 : ∀ D (hD : D ∈ Z),
(M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ
-- … truncated; follow the source link for the rest …
2 supporting declarations (lemmas, instances)
-
obsKernel_inter_singleton_Zrand_eqtheorem — Joint kernel agreement on the Z.random-level-set event. For an intervention whose target random copies are observed and fixed copies are not already fixed, an observed union of the target random copies and conditioning block, a post-intervention fixed assignment, a conditioning-block value, and a measurable observed event, the post-intervention and base observational kernels assign equal mass to the intersection of that event with the corresponding filled target-and-conditioning level set.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhZrW :Z.image SWIGNode.random ∪ W ⊆ M'.observeds' :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesS :Set M'.ObservedValueshS :conclusion(M'.fixSet Z hZ_obs hZ_fixed).obsKernel s' (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})= M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s') (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})Proof (Lean source)
theorem obsKernel_inter_singleton_Zrand_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) (W : Finset (SWIGNode N)) (hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed) [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) (w : ValuesOn W (swigΩ Ω)) {S : Set M'.ObservedValues} (hS : MeasurableSet S) : (M'.fixSet Z hZ_obs hZ_fixed).obsKernel s' (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}) = M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s') (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}) := by classical -- Abbreviations (via `let`; avoid `set` to prevent elaboration surprises). let M1 := M' let M2 := M1.fixSet Z hZ_obs hZ_fixed -- Use the explicit `.symm ▸` cast so the form matches the goal. have hZrW_M2 : Z.image SWIGNode.random ∪ W ⊆ M2.observed := (fixSet_observed M1 Z hZ_obs hZ_fixed).symm ▸ hZrW let s_M1 : M1.FixedValues := M1.fixSetProj Z hZ_obs hZ_fixed s' let c := M'.fillZrW Z hZ_obs hZ_fixed W s' w -- Measurability bookkeeping. have h_sing : MeasurableSet ({c} : Set _) := measurableSet_singleton _ have hπ_M1 : Measurable (valuesProjection hZrW : M1.ObservedValues → _) := by fun_prop have hπ_M2 : Measurable (valuesProjection hZrW_M2 : M2.ObservedValues → _) := by fun_prop have h_pre_M1 : MeasurableSet ((valuesProjection hZrW)⁻¹' {c}) := hπ_M1 h_sing have h_pre_M2 : MeasurableSet ((valuesProjection hZrW_M2)⁻¹' {c}) := hπ_M2 h_sing have hI_M1 : MeasurableSet (S ∩ (valuesProjection hZrW)⁻¹' {c}) := hS.inter h_pre_M1 have hI_M2 : MeasurableSet (S ∩ (valuesProjection hZrW_M2)⁻¹' {c}) := hS.inter h_pre_M2 have hRTO_M2 : Measurable M2.randomToObserved := by fun_prop have hRTO_M1 : Measurable M1.randomToObserved := by fun_prop have hf_M1 : Measurable (fun ℓ : M1.LatentValues => M1.evalMap s_M1 ℓ) := by fun_prop have hf_M2 : Measurable (fun ℓ : M2.LatentValues => M2.evalMap s' ℓ) := by fun_prop have hcast : Measurable (valuesProjection (le_of_eq (fixSet_unobserved M1 Z hZ_obs hZ_fixed).symm) : M2.LatentValues → M1.LatentValues) := by fun_prop -- LHS: unfold obsKernel → jointKernel → latentProduct.map evalMap. unfold obsKernel rw [ProbabilityTheory.Kernel.map_apply _ ((M'.fixSet Z hZ_obs hZ_fixed).measurable_randomToObserved), ProbabilityTheory.Kernel.map_apply _ M'.measurable_randomToObserved] have hI_M2_exp : MeasurableSet (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}) := by exact hS.inter ((measurable_valuesProjection _) (measurableSet_singleton _)) have hI_M1_exp : MeasurableSet (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}) := by exact hS.inter ((measurable_valuesProjection _) (measurableSet_singleton _)) have hmap_M2 : (map (M'.fixSet Z hZ_obs hZ_fixed).randomToObserved ((M'.fixSet Z hZ_obs hZ_fixed).jointKernel s')) (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}) = ((M'.fixSet Z hZ_obs hZ_fixed).jointKernel s') ((M'.fixSet Z hZ_obs hZ_fixed).randomToObserved ⁻¹' (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})) := by exact MeasureTheory.Measure.map_apply ((M'.fixSet Z hZ_obs hZ_fixed).measurable_randomToObserved) hI_M2_exp have hmap_M1 : (map M'.randomToObserved (M'.jointKernel (M'.fixSetProj Z hZ_obs hZ_fixed s'))) (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}) = (M'.jointKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')) (M'.randomToObserved ⁻¹' (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})) := by exact MeasureTheory.Measure.map_apply M'.measurable_randomToObserved hI_M1_exp rw [hmap_M2, hmap_M1, jointKernel_apply_eq (M'.fixSet Z hZ_obs hZ_fixed) s', jointKernel_apply_eq M' (M'.fixSetProj Z hZ_obs hZ_fixed s')] have hf_M2_exp : Measurable (fun ℓ : (M'.fixSet Z hZ_obs hZ_fixed).LatentValues => (M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ) := by fun_prop have hf_M1_exp : Measurable (fun ℓ : M'.LatentValues => M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') ℓ) := by fun_prop have hpre_M2 : MeasurableSet ((M'.fixSet Z hZ_obs hZ_fixed).randomToObserved ⁻¹' (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})) := (M'.fixSet Z hZ_obs hZ_fixed).measurable_randomToObserved hI_M2_exp have hpre_M1 : MeasurableSet (M'.randomToObserved ⁻¹' (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})) := M'.measurable_randomToObserved hI_M1_exp have heval_M2 : (map (fun ℓ : (M'.fixSet Z hZ_obs hZ_fixed).LatentValues => (M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ) (M'.fixSet Z hZ_obs hZ_fixed).latentProduct) ((M'.fixSet Z hZ_obs hZ_fixed).randomToObserved ⁻¹' (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})) = (M'.fixSet Z hZ_obs hZ_fixed).latentProduct ((fun ℓ : (M'.fixSet Z hZ_obs hZ_fixed).LatentValues => (M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ) ⁻¹' ((M'.fixSet Z hZ_obs hZ_fixed).randomToObserved ⁻¹' (S ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}))) := by exact MeasureTheory.Measure.map_apply hf_M2_exp hpre_M2 have heval_M1 : (map (fun ℓ : M'.LatentValues => M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') ℓ) M'.latentProduct) (M'.randomToObserved ⁻¹' (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w})) = M'.latentProduct ((fun ℓ : M'.LatentValues => M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') ℓ) ⁻¹' (M'.randomToObserved ⁻¹' (S ∩ (valuesProjection hZrW)⁻¹' {M'.fillZrW Z hZ_obs hZ_fixed W s' w}))) := by exact MeasureTheory.Measure.map_apply hf_M1_exp hpre_M1 rw [heval_M2, heval_M1, ← fixSet_latentProduct_compat M' Z hZ_obs hZ_fixed, MeasureTheory.Measure.map_apply (measurable_valuesProjection _) (hf_M1_exp hpre_M1)] -- Goal: M2.latentProduct {ℓ : rando(M2.evalMap s' ℓ) ∈ I} = M2.latentProduct {ℓ : ...}. -- Reduce to set equality on the same M2.latentProduct. congr 1 -- Two preimage sets (in M2.LatentValues): -- L2 := {ℓ : rando(M2.evalMap s' ℓ) ∈ S ∩ π_C⁻¹{c}} -- L1 := {ℓ : cast ℓ ∈ {ℓ_M1 : rando(M1.evalMap s_M1 ℓ_M1) ∈ S ∩ π_C⁻¹{c}}} -- = {ℓ : rando(M1.evalMap s_M1 (cast ℓ)) ∈ S ∩ π_C⁻¹{c}} apply Set.eq_of_subset_of_subset all_goals intro ℓ hℓ simp only [Set.mem_preimage, Set.mem_inter_iff] at hℓ ⊢ -- Both directions use the same core mechanism: on the preimage, one side's -- evalMap is on the Z-level set; bridge via Claim A/B to get pointwise -- agreement of rando(evalMap) at every observed, hence the other side -- inherits membership. · -- ⊆: LHS (M2-side) ⊆ RHS (M1-side via cast). rcases hℓ with ⟨hS_mem, hπ_mem⟩ -- Extract LS_M2 from π_C = c. have hLS_M2 : ∀ D (hD : D ∈ Z), M2.evalMap s' ℓ ⟨SWIGNode.random D, mem_union_left _ (hZ_obs D hD)⟩ = s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hD⟩ := by intro D hD -- π_C(rando(M2.evalMap s' ℓ)) = c at ⟨.random D, _⟩. have hD_in : SWIGNode.random D ∈ Z.image SWIGNode.random ∪ W := mem_union_left _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩) have hcoord := congrFun hπ_mem ⟨SWIGNode.random D, hD_in⟩ have hc_at : c ⟨SWIGNode.random D, hD_in⟩ = s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hD⟩ := by show (valuesUnionMk (zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s')) w) ⟨SWIGNode.random D, hD_in⟩ = s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hD⟩ rw [valuesUnionMk_apply_left _ _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)] rfl exact hcoord.trans hc_at -- Apply the M2-direction level-set bridge at each observed v. refine ⟨?_, ?_⟩ · -- S membership: rando(M1.evalMap s_M1 (cast ℓ)) ∈ S. have heq : M1.randomToObserved (M1.evalMap s_M1 (valuesProjection (le_of_eq (fixSet_unobserved M1 Z hZ_obs hZ_fixed).symm) ℓ)) = M2.randomToObserved (M2.evalMap s' ℓ) := by funext v simp only [randomToObserved] exact (fixSet_evalMap_levelset_compat_M2 M' Z hZ_obs hZ_fixed s' ℓ hLS_M2 v.property).symm rw [heq] exact hS_mem · -- π_C membership: preserved under the same pointwise equality. have heq : M1.randomToObserved (M1.evalMap s_M1 (valuesProjection (le_of_eq (fixSet_unobserved M1 Z hZ_obs hZ_fixed).symm) ℓ)) = M2.randomToObserved (M2.evalMap s' ℓ) := by funext v simp only [randomToObserved] exact (fixSet_evalMap_levelset_compat_M2 M' Z hZ_obs hZ_fixed s' ℓ hLS_M2 v.property).symm rw [heq] exact hπ_mem · -- ⊇: RHS (M1-side via cast) ⊆ LHS (M2-side). rcases hℓ with ⟨hS_mem, hπ_mem⟩ -- Extract LS_M1(cast ℓ) from π_C = c. have hLS_M1 : ∀ D (hD : D ∈ Z), M1.evalMap s_M1 (valuesProjection (le_of_eq (fixSet_unobserved M1 Z hZ_obs hZ_fixed).symm) ℓ) ⟨SWIGNode.random D, mem_union_left _ (hZ_obs D hD)⟩ = s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hD⟩ := by intro D hD have hD_in : SWIGNode.random D ∈ Z.image SWIGNode.random ∪ W := mem_union_left _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩) have hcoord := congrFun hπ_mem ⟨SWIGNode.random D, hD_in⟩ have hc_at : c ⟨SWIGNode.random D, hD_in⟩ = s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hD⟩ := by show (valuesUnionMk (zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s')) w) ⟨SWIGNode.random D, hD_in⟩ = s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hD⟩ rw [valuesUnionMk_apply_left _ _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)] rfl exact hcoord.trans hc_at -- … truncated; follow the source link for the rest … -
obsKernel_disintegrate_recttheorem — Base-model disintegration over condition coordinates.hypothesesN :sharedType u_1N → Type u_2M :SCM N ΩhY :Y ⊆ M.observedhCC :CC ⊆ M.observeds :M.FixedValueshD :hB :conclusionM.obsKernel s ((valuesProjection hCC)⁻¹' D ∩ (valuesProjection hY)⁻¹' B)= ∫⁻ c in D, M.obsCondKernel Y CC hY hCC (s, c) B ∂((M.obsKernel s).map (valuesProjection hCC))Proof (Lean source)
theorem obsKernel_disintegrate_rect (M : SCM N Ω) (Y CC : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hCC : CC ⊆ M.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [CountableOrCountablyGenerated M.FixedValues (ValuesOn CC (swigΩ Ω))] (s : M.FixedValues) {D : Set (ValuesOn CC (swigΩ Ω))} {B : Set (ValuesOn Y (swigΩ Ω))} (hD : MeasurableSet D) (hB : MeasurableSet B) : M.obsKernel s ((valuesProjection hCC)⁻¹' D ∩ (valuesProjection hY)⁻¹' B) = ∫⁻ c in D, M.obsCondKernel Y CC hY hCC (s, c) B ∂((M.obsKernel s).map (valuesProjection hCC)) := by classical have hπCC : Measurable (valuesProjection (Ω := swigΩ Ω) hCC) := by fun_prop have hπY : Measurable (valuesProjection (Ω := swigΩ Ω) hY) := by fun_prop -- κ := obsCondPairKernel. set κ : Kernel M.FixedValues (ValuesOn CC (swigΩ Ω) × ValuesOn Y (swigΩ Ω)) := M.obsCondPairKernel Y CC hY hCC with hκ_def haveI hMarkov_κ : IsMarkovKernel κ := by rw [hκ_def] unfold obsCondPairKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (hπCC.prodMk hπY) haveI : IsFiniteKernel κ := inferInstance -- Step 1: κ s (D ×ˢ B) = obsKernel cylinder. have h_pre : (valuesProjection hCC)⁻¹' D ∩ (valuesProjection hY)⁻¹' B = (fun ω => (valuesProjection hCC ω, valuesProjection hY ω))⁻¹' (D ×ˢ B) := by ext ω; simp [Set.mem_inter_iff, Set.mem_preimage, Set.mem_prod] have hKpair : κ s (D ×ˢ B) = M.obsKernel s ((valuesProjection hCC)⁻¹' D ∩ (valuesProjection hY)⁻¹' B) := by rw [hκ_def]; unfold obsCondPairKernel rw [ProbabilityTheory.Kernel.map_apply' _ (hπCC.prodMk hπY) _ (hD.prod hB)] rw [h_pre] -- Step 2: Kernel.fst κ s = (M.obsKernel s).map (valuesProjection hCC). have hfst : ProbabilityTheory.Kernel.fst κ s = (M.obsKernel s).map (valuesProjection hCC) := by rw [hκ_def] unfold obsCondPairKernel rw [ProbabilityTheory.Kernel.fst_map_prod _ hπY, ProbabilityTheory.Kernel.map_apply _ hπCC] -- Step 3: Mathlib disintegration for κ. have hKey : ∫⁻ c in D, ProbabilityTheory.Kernel.condKernel κ (s, c) B ∂(ProbabilityTheory.Kernel.fst κ s) = κ s (D ×ˢ B) := ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod (κ := κ) s hD hB -- Step 4: obsCondKernel = condKernel of κ (definitional, up to instance). -- Assemble (sidestep instance rewriting by going through ENNReal eq). rw [← hKpair, ← hKey, hfst] -- Goal: ∫⁻ c in D, condKernel κ (s,c) B d(map π_CC obsKernel s) -- = ∫⁻ c in D, obsCondKernel Y CC … (s,c) B d(map π_CC obsKernel s) refine MeasureTheory.lintegral_congr_ae ?_ refine Filter.Eventually.of_forall ?_ intro c -- obsCondKernel is defined as condKernel of obsCondPairKernel. change ProbabilityTheory.Kernel.condKernel κ (s, c) B = M.obsCondKernel Y CC hY hCC (s, c) B rfl
LevelsetCompat 2 core · 0 supporting This file proves that the evaluation maps of the single-intervention and double-intervention models agree on the latent level set where the single intervention already realizes the additional treatment values. ★ fixSet_evalMap_levelset_compat★ fixSet_evalMap_levelset_compat_M2
Rule 2 Level-Set Compatibility
This file proves that the evaluation maps of the single-intervention and double-intervention models agree on the latent level set where the single intervention already realizes the additional treatment values. This is the evaluation-map bridge used in the kernel proof of Rule 2 of do-calculus.
theorem fixSet_evalMap_levelset_compat reviewed
⚑ flagged
Causalean.SCM
Cross-SCM evalMap level-set bridge for Rule 2. For the intervention on names Z, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, fix an intervened fixed assignment s' and a latent draw ℓ. Suppose on the "level set" picked out by ℓ, the base model's evaluation map at the projected fixed assignment already reproduces, at every random copy of a name in Z, the intervention value recorded in s'; then at any observed node v in the intervened model, the intervened model's evaluation map at (s', ℓ) agrees with the base model's evaluation map at the projected fixed assignment and the correspondingly reindexed latent draw.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
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
hLevelSet :
∀ D (hD : D ∈ Z),
M'.evalMap (M'.fixSetProj Z hZ_obs hZ_fixed s') (valuesProjection (le_of_eq (fixSet_unobserved M' Z hZ_obs hZ_fixed).symm) ℓ) ⟨SWIGNode.random D, mem_union_left _ (hZ_obs D hD)⟩
= s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩
v :
SWIGNode N
hv :
v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed
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_levelset_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)
(hLevelSet : ∀ D (hD : D ∈ Z),
M'.evalMap
(M'.fixSetProj Z hZ_obs hZ_fixed s')
(valuesProjection
(le_of_eq
(fixSet_unobserved M' Z hZ_obs hZ_fixed).symm)
ℓ)
⟨SWIGNode.random D, mem_union_left _ (hZ_obs D hD)⟩
= s' ⟨SWIGNode.fixed D,
SCM.fixed_mem_fixSet M'
Z hZ_obs hZ_fixed hD⟩)
{v : SWIGNode N}
(hv : v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed) :
(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
let M1 := M'
let M2 := M1.fixSet Z hZ_obs hZ_fixed
have h_obs_eq : M2.observed = M1.observed := rfl
have h_unobs : M2.unobserved = M1.unobserved := rfl
let s_M1 : M1.FixedValues := M1.fixSetProj Z hZ_obs hZ_fixed s'
let ℓ_M1 : M1.LatentValues := valuesProjection (le_of_eq h_unobs.symm) ℓ
-- Strong recursion on `M2.observedIndex ⟨v, hv⟩`.
suffices h_obs : ∀ (n : ℕ) (w : SWIGNode N) (hw : w ∈ M2.observed),
(M2.observedIndex ⟨w, hw⟩).val = n →
M2.evalMap s' ℓ ⟨w, mem_union_left _ hw⟩ =
M1.evalMap s_M1 ℓ_M1 ⟨w, mem_union_left _ hw⟩ by
exact h_obs _ v hv rfl
intro n
induction n using Nat.strongRecOn with
| _ n ih =>
intro v hv hidx
have hv_M1 : v ∈ M1.observed := hv
rw [SCM.evalMap_observed_unfold M2 s' ℓ ⟨v, hv⟩,
SCM.evalMap_observed_unfold M1 s_M1 ℓ_M1 ⟨v, hv_M1⟩]
-- Unfold `M2.structFun ⟨v, _⟩` to `M1.structFun ⟨v, _⟩ ∘ fixMonoParentMap`.
change M1.structFun ⟨v, hv_M1⟩
(fixMonoParentMap M1.toSWIGGraph Z hZ_obs hZ_fixed v
(fun w : {w // w ∈ (M1.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⟩))
= M1.structFun ⟨v, hv_M1⟩ (fun w : {w // w ∈ M1.dag.parents v} =>
if huo : w.val ∈ M1.unobserved then ℓ_M1 ⟨w.val, huo⟩
else if hfix : w.val ∈ M1.fixed then s_M1 ⟨w.val, hfix⟩
else
have hedge : M1.dag.edge w.val v := M1.dag.mem_parents.mp w.property
have hobs : w.val ∈ M1.observed := by
rcases Finset.mem_union.mp (M1.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
M1.evalMap s_M1 ℓ_M1 ⟨w.val, mem_union_left _ hobs⟩)
congr 1
funext w
rcases w with ⟨wVal, hwVal_M1⟩
cases wVal with
| random u =>
by_cases hu_Z : u ∈ Z
· -- **New case for Rule 2**: u ∈ Z. LHS reads M2-tuple at `.fixed u`
-- (via `fixMonoParentMap_apply_random` since Z is the split target).
rw [fixMonoParentMap_apply_random M1.toSWIGGraph Z hZ_obs hZ_fixed v u hu_Z _
hwVal_M1]
-- LHS evaluation at `.fixed u`: not unobserved (.fixed nodes are fixed),
-- is in M2.fixed via Z.image .fixed.
have huo_M2 : (SWIGNode.fixed u : SWIGNode N) ∉ M2.unobserved := by
intro h
rcases M2.unobserved_is_random _ h with ⟨_, hEq⟩; cases hEq
have hfix_M2 : (SWIGNode.fixed u : SWIGNode N) ∈ M2.fixed :=
SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hu_Z
simp only [dif_neg huo_M2, dif_pos hfix_M2]
-- RHS evaluation at `.random u`: observed, so falls through to
-- a recursive M1.evalMap call. Use the level-set hypothesis.
have hobs_M1 : (SWIGNode.random u : SWIGNode N) ∈ M1.observed :=
hZ_obs u hu_Z
have huo_M1 : (SWIGNode.random u : SWIGNode N) ∉ M1.unobserved :=
Finset.disjoint_left.mp M1.obs_unobs_disjoint hobs_M1
have hfix_M1 : (SWIGNode.random u : SWIGNode N) ∉ M1.fixed := by
intro h
rcases M1.fixed_is_fixed _ h with ⟨_, hEq⟩; cases hEq
simp only [dif_neg huo_M1, dif_neg hfix_M1]
-- RHS = M1.evalMap s_M1 ℓ_M1 ⟨.random u, _⟩ = s' ⟨.fixed u, _⟩
-- by the level-set hypothesis.
exact (hLevelSet u hu_Z).symm
· -- **Old case (Rule 3 mirror)**: u ∉ Z. fixMonoParentMap acts
-- identity-like at `.random u`.
rw [fixMonoParentMap_apply_random_notMem M1.toSWIGGraph Z hZ_obs hZ_fixed v _ u
hu_Z hwVal_M1]
by_cases huo : (SWIGNode.random u : SWIGNode N) ∈ M1.unobserved
· have huo_M2 : SWIGNode.random u ∈ M2.unobserved := huo
simp only [dif_pos huo, dif_pos huo_M2]
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) ∈ M1.fixed
· exfalso
rcases M1.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) ∈
M1.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.
have hobs_M1 : (SWIGNode.random u : SWIGNode N) ∈ M1.observed := by
have hedge_M1 : M1.dag.edge (SWIGNode.random u) v :=
M1.dag.mem_parents.mp hwVal_M1
rcases Finset.mem_union.mp (M1.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
-- Need: .random u ∈ M2.dag.parents v to apply the index-decrease lemma.
-- Since u ∉ Z and .random u ∈ M1.dag.parents v, the splitMono_parents_char
-- keeps .random u as a parent in M2.
have hwVal_M2 : SWIGNode.random u ∈ M2.dag.parents v :=
(SWIGGraph.splitMono_parents_char M1.toSWIGGraph Z hZ_obs hZ_fixed
v (SWIGNode.random u)).2
(inl ⟨hwVal_M1,
fun D hD heq => hu_Z (SWIGNode.random.inj heq ▸ hD)⟩)
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 rfl
| fixed d =>
-- `.fixed d` parent: copies through.
rw [fixMonoParentMap_apply_fixed M1.toSWIGGraph Z hZ_obs hZ_fixed v _ d hwVal_M1]
have huo : (SWIGNode.fixed d : SWIGNode N) ∉ M1.unobserved := by
intro h
rcases M1.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]
by_cases hfix_M1 : (SWIGNode.fixed d : SWIGNode N) ∈ M1.fixed
· have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∈ M2.fixed := by
change _ ∈ M1.fixed ∪ Z.image SWIGNode.fixed
exact mem_union_left _ hfix_M1
simp only [dif_pos hfix_M1, dif_pos hfix_M2]
rfl
· by_cases hd_Z : d ∈ Z
· exfalso
have := M1.fixed_outside_fixed_isolated d hfix_M1
have hCh : v ∈ M1.dag.children (SWIGNode.fixed d) :=
M1.dag.mem_children.mpr (M1.dag.mem_parents.mp hwVal_M1)
simpa [this.2] using hCh
· have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∉ M2.fixed := by
intro h
rcases Finset.mem_union.mp
(show _ ∈ M1.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]
exfalso
have hobs : (SWIGNode.fixed d : SWIGNode N) ∈ M1.observed := by
have hedge_M1 : M1.dag.edge (SWIGNode.fixed d) v :=
M1.dag.mem_parents.mp hwVal_M1
rcases Finset.mem_union.mp (M1.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 M1.observed_is_random _ hobs with ⟨_, hEq⟩; cases hEq
theorem fixSet_evalMap_levelset_compat_M2 reviewed
⚑ flagged
Causalean.SCM
M2-direction level-set evalMap bridge for Rule 2. For the intervention on names Z, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, fix an intervened fixed assignment s' and a latent draw ℓ. Suppose the intervened model's own evaluation map at (s', ℓ) already reproduces, at every random copy of a name in Z, the intervention value recorded in s'; then at any observed node v in the intervened model, the intervened model's evaluation map at (s', ℓ) agrees with the base model's evaluation map at the projected fixed assignment and the correspondingly reindexed latent draw.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
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
hLS_M2 :
∀ D (hD : D ∈ Z),
(M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ ⟨SWIGNode.random D, mem_union_left _ (hZ_obs D hD)⟩
= s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩
v :
SWIGNode N
hv :
v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed
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_levelset_compat_M2
(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)
(hLS_M2 : ∀ D (hD : D ∈ Z),
(M'.fixSet Z hZ_obs hZ_fixed).evalMap s' ℓ
⟨SWIGNode.random D, mem_union_left _ (hZ_obs D hD)⟩
= s' ⟨SWIGNode.fixed D,
SCM.fixed_mem_fixSet M'
Z hZ_obs hZ_fixed hD⟩)
{v : SWIGNode N}
(hv : v ∈ (M'.fixSet Z hZ_obs hZ_fixed).observed) :
(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
let M1 := M'
let M2 := M1.fixSet Z hZ_obs hZ_fixed
have h_obs_eq : M2.observed = M1.observed := rfl
have h_unobs : M2.unobserved = M1.unobserved := rfl
let s_M1 : M1.FixedValues := M1.fixSetProj Z hZ_obs hZ_fixed s'
let ℓ_M1 : M1.LatentValues := valuesProjection (le_of_eq h_unobs.symm) ℓ
-- Strong recursion on `M1.observedIndex ⟨v, hv⟩`.
suffices h_obs : ∀ (n : ℕ) (w : SWIGNode N) (hw : w ∈ M2.observed),
(M1.observedIndex ⟨w, hw⟩).val = n →
M2.evalMap s' ℓ ⟨w, mem_union_left _ hw⟩ =
M1.evalMap s_M1 ℓ_M1 ⟨w, mem_union_left _ hw⟩ by
exact h_obs _ v hv rfl
intro n
induction n using Nat.strongRecOn with
| _ n ih =>
intro v hv hidx
have hv_M1 : v ∈ M1.observed := hv
rw [SCM.evalMap_observed_unfold M2 s' ℓ ⟨v, hv⟩,
SCM.evalMap_observed_unfold M1 s_M1 ℓ_M1 ⟨v, hv_M1⟩]
change M1.structFun ⟨v, hv_M1⟩
(fixMonoParentMap M1.toSWIGGraph Z hZ_obs hZ_fixed v
(fun w : {w // w ∈ (M1.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⟩))
= M1.structFun ⟨v, hv_M1⟩ (fun w : {w // w ∈ M1.dag.parents v} =>
if huo : w.val ∈ M1.unobserved then ℓ_M1 ⟨w.val, huo⟩
else if hfix : w.val ∈ M1.fixed then s_M1 ⟨w.val, hfix⟩
else
have hedge : M1.dag.edge w.val v := M1.dag.mem_parents.mp w.property
have hobs : w.val ∈ M1.observed := by
rcases Finset.mem_union.mp (M1.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
M1.evalMap s_M1 ℓ_M1 ⟨w.val, mem_union_left _ hobs⟩)
congr 1
funext w
rcases w with ⟨wVal, hwVal_M1⟩
cases wVal with
| random u =>
by_cases hu_Z : u ∈ Z
· -- u ∈ Z: IH + hLS_M2 replaces the direct `hLevelSet` appeal.
rw [fixMonoParentMap_apply_random M1.toSWIGGraph Z hZ_obs hZ_fixed v u hu_Z _
hwVal_M1]
have huo_M2 : (SWIGNode.fixed u : SWIGNode N) ∉ M2.unobserved := by
intro h
rcases M2.unobserved_is_random _ h with ⟨_, hEq⟩; cases hEq
have hfix_M2 : (SWIGNode.fixed u : SWIGNode N) ∈ M2.fixed :=
SCM.fixed_mem_fixSet M1 Z hZ_obs hZ_fixed hu_Z
simp only [dif_neg huo_M2, dif_pos hfix_M2]
have hobs_M1_u : (SWIGNode.random u : SWIGNode N) ∈ M1.observed :=
hZ_obs u hu_Z
have huo_M1 : (SWIGNode.random u : SWIGNode N) ∉ M1.unobserved :=
Finset.disjoint_left.mp M1.obs_unobs_disjoint hobs_M1_u
have hfix_M1 : (SWIGNode.random u : SWIGNode N) ∉ M1.fixed := by
intro h
rcases M1.fixed_is_fixed _ h with ⟨_, hEq⟩; cases hEq
simp only [dif_neg huo_M1, dif_neg hfix_M1]
-- IH at `.random u` via M1.observed_parent_index_lt (edge in M1.dag).
have hobs_M2_u : (SWIGNode.random u : SWIGNode N) ∈ M2.observed := hobs_M1_u
have hidx_u : (M1.observedIndex ⟨SWIGNode.random u, hobs_M1_u⟩).val
< (M1.observedIndex ⟨v, hv_M1⟩).val := by
have hedge_M1 : M1.dag.edge (SWIGNode.random u) v :=
M1.dag.mem_parents.mp hwVal_M1
have hv_eq : (M1.observedAt
⟨(M1.observedIndex ⟨v, hv_M1⟩).val,
(M1.observedIndex ⟨v, hv_M1⟩).isLt⟩).val = v := by
have := M1.observedAt_observedIndex ⟨v, hv_M1⟩
convert this
have hedge_M1' : M1.dag.edge (SWIGNode.random u)
(M1.observedAt
⟨(M1.observedIndex ⟨v, hv_M1⟩).val,
(M1.observedIndex ⟨v, hv_M1⟩).isLt⟩).val := by
rw [hv_eq]; exact hedge_M1
exact M1.observed_parent_index_lt
(M1.observedIndex ⟨v, hv_M1⟩).isLt hedge_M1' hobs_M1_u
rw [hidx] at hidx_u
have h_ih := ih _ hidx_u (SWIGNode.random u) hobs_M2_u rfl
-- h_ih: M2 at .random u = M1 at .random u. Combined with hLS_M2: M1 at .random u = z_u.
rw [← h_ih]
exact (hLS_M2 u hu_Z).symm
· -- u ∉ Z: structurally identical to levelset_compat's u ∉ Z branch,
-- but IH indexes on M1.observedIndex (natural since the edge is in M1.dag).
rw [fixMonoParentMap_apply_random_notMem M1.toSWIGGraph Z hZ_obs hZ_fixed v _ u
hu_Z hwVal_M1]
by_cases huo : (SWIGNode.random u : SWIGNode N) ∈ M1.unobserved
· have huo_M2 : SWIGNode.random u ∈ M2.unobserved := huo
simp only [dif_pos huo, dif_pos huo_M2]
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) ∈ M1.fixed
· exfalso
rcases M1.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) ∈
M1.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]
have hobs_M1 : (SWIGNode.random u : SWIGNode N) ∈ M1.observed := by
have hedge_M1 : M1.dag.edge (SWIGNode.random u) v :=
M1.dag.mem_parents.mp hwVal_M1
rcases Finset.mem_union.mp (M1.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
have hidx_w : (M1.observedIndex ⟨SWIGNode.random u, hobs_M1⟩).val
< (M1.observedIndex ⟨v, hv_M1⟩).val := by
have hedge_M1 : M1.dag.edge (SWIGNode.random u) v :=
M1.dag.mem_parents.mp hwVal_M1
have hv_eq : (M1.observedAt
⟨(M1.observedIndex ⟨v, hv_M1⟩).val,
(M1.observedIndex ⟨v, hv_M1⟩).isLt⟩).val = v := by
have := M1.observedAt_observedIndex ⟨v, hv_M1⟩
convert this
have hedge_M1' : M1.dag.edge (SWIGNode.random u)
(M1.observedAt
⟨(M1.observedIndex ⟨v, hv_M1⟩).val,
(M1.observedIndex ⟨v, hv_M1⟩).isLt⟩).val := by
rw [hv_eq]; exact hedge_M1
exact M1.observed_parent_index_lt
(M1.observedIndex ⟨v, hv_M1⟩).isLt hedge_M1' hobs_M1
rw [hidx] at hidx_w
exact ih _ hidx_w (SWIGNode.random u) hobs_M2 rfl
| fixed d =>
-- Unchanged from levelset_compat.
rw [fixMonoParentMap_apply_fixed M1.toSWIGGraph Z hZ_obs hZ_fixed v _ d hwVal_M1]
have huo : (SWIGNode.fixed d : SWIGNode N) ∉ M1.unobserved := by
intro h
rcases M1.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]
by_cases hfix_M1 : (SWIGNode.fixed d : SWIGNode N) ∈ M1.fixed
· have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∈ M2.fixed := by
change _ ∈ M1.fixed ∪ Z.image SWIGNode.fixed
exact mem_union_left _ hfix_M1
simp only [dif_pos hfix_M1, dif_pos hfix_M2]
rfl
· by_cases hd_Z : d ∈ Z
· exfalso
have := M1.fixed_outside_fixed_isolated d hfix_M1
have hCh : v ∈ M1.dag.children (SWIGNode.fixed d) :=
M1.dag.mem_children.mpr (M1.dag.mem_parents.mp hwVal_M1)
simpa [this.2] using hCh
· have hfix_M2 : (SWIGNode.fixed d : SWIGNode N) ∉ M2.fixed := by
intro h
rcases Finset.mem_union.mp
(show _ ∈ M1.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]
exfalso
have hobs : (SWIGNode.fixed d : SWIGNode N) ∈ M1.observed := by
have hedge_M1 : M1.dag.edge (SWIGNode.fixed d) v :=
M1.dag.mem_parents.mp hwVal_M1
rcases Finset.mem_union.mp (M1.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 M1.observed_is_random _ hobs with ⟨_, hEq⟩; cases hEq
RectIdentity 2 core · 0 supporting This file provides two almost-everywhere equalities of conditional kernels — a d-separation collapse and a cross-model image comparison — consumed by the discrete-treatment backdoor Rule-2 derivation. ★ obsCondKernel_dSep_collapse_ae★ obsCondKernel_cross_SCM_ae_eq_on_fillZrW
Rule 2 conditional-kernel a.e. helpers
This file provides two almost-everywhere equalities of conditional kernels — a d-separation collapse and a cross-model image comparison — consumed by the discrete-treatment backdoor Rule-2 derivation.
lemma obsCondKernel_dSep_collapse_ae reviewed
⚑ flagged
Causalean.SCM
D-separation collapse for the post-intervention conditional kernel. For the intervention on names Z, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, with outcome set Y and conditioning set W contained in the observed variables, suppose 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. Then, fixing an intervened fixed assignment s and an outcome set B, for almost every conditioning value on Z.random ∪ W, the intervened model's conditional distribution of Y given Z.random ∪ W assigns B the same probability as its conditional distribution of Y given W alone, evaluated at the W-projection of that conditioning value.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
hY :
Y ⊆ M'.observed
hW :
W ⊆ M'.observed
∀ n, StandardBorelSpace (swigΩ Ω n)
∀ n, Nonempty (swigΩ Ω n)
hdSep :
(M'.fixSet Z hZ_obs hZ_fixed).dag.dSep Y (Z.image SWIGNode.random) (W ∪ (M'.fixSet Z hZ_obs hZ_fixed).fixed)
CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
s :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
conclusion
hZr :
by intro v hv rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩ exact hZ_obs D hD (: Z.image SWIGNode.random ⊆ M'.observed)
hZrW :
union_subset hZr hW (: Z.image SWIGNode.random ∪ W ⊆ M'.observed)
∀ᵐ c ∂((map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW)) ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s))), ((M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y (Z.image SWIGNode.random ∪ W) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW) (s, c)) B
= ((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, valuesProjection (subset_union_right (s₁ := Z.image SWIGNode.random) (s₂ := W)) c)) B
Proof (Lean source)
lemma obsCondKernel_dSep_collapse_ae
(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)
[∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)]
(hdSep : (M'.fixSet Z hZ_obs hZ_fixed).dag.dSep
Y (Z.image SWIGNode.random)
(W ∪ (M'.fixSet Z hZ_obs hZ_fixed).fixed))
[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Ω Ω))]
(s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues)
{B : Set (ValuesOn Y (swigΩ Ω))} :
let hZr : Z.image SWIGNode.random ⊆ M'.observed := by
intro v hv
rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩
exact hZ_obs D hD
let hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed :=
Finset.union_subset hZr hW
∀ᵐ c ∂((map
(valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW))
((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s))),
((M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y
(Z.image SWIGNode.random ∪ W)
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY)
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW)
(s, c)) B
= ((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, valuesProjection
(Finset.subset_union_right
(s₁ := Z.image SWIGNode.random) (s₂ := W)) c)) B := by
classical
have hZr : Z.image SWIGNode.random ⊆ M'.observed := by
intro v hv
rcases Finset.mem_image.mp hv with ⟨D, hD, rfl⟩
exact hZ_obs D hD
have hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed := Finset.union_subset hZr hW
have hDisj_YZr : Disjoint Y (Z.image SWIGNode.random) := hdSep.1
have hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W :=
Disjoint.mono_right Finset.subset_union_left hdSep.2.2.1
have hDisj_YW : Disjoint Y W :=
Disjoint.mono_right Finset.subset_union_left hdSep.2.1
-- Abbreviations.
let M2 := M'.fixSet Z hZ_obs hZ_fixed
let Zr := Z.image SWIGNode.random
let μ := M2.obsKernel s
have hM2_def : M2 = M'.fixSet Z hZ_obs hZ_fixed := rfl
have hZr_def : Zr = Z.image SWIGNode.random := rfl
have hμ_def : μ = M2.obsKernel s := rfl
have hY_M2 : Y ⊆ M2.observed := by
rw [show M2.observed = M'.observed from fixSet_observed M' Z hZ_obs hZ_fixed]
exact hY
have hW_M2 : W ⊆ M2.observed := by
rw [show M2.observed = M'.observed from fixSet_observed M' Z hZ_obs hZ_fixed]
exact hW
have hZrW_M2 : Zr ∪ W ⊆ M2.observed := by
rw [show M2.observed = M'.observed from fixSet_observed M' Z hZ_obs hZ_fixed]
exact hZrW
have hZr_M2 : Zr ⊆ M2.observed := Finset.subset_union_left.trans hZrW_M2
-- Projection abbreviations.
let π_Y := valuesProjection (Ω := swigΩ Ω) hY_M2
let π_W := valuesProjection (Ω := swigΩ Ω) hW_M2
let π_Zr := valuesProjection (Ω := swigΩ Ω) hZr_M2
let π_C := valuesProjection (Ω := swigΩ Ω) hZrW_M2
have hπY_def : π_Y = valuesProjection (Ω := swigΩ Ω) hY_M2 := rfl
have hπW_def : π_W = valuesProjection (Ω := swigΩ Ω) hW_M2 := rfl
have hπZr_def : π_Zr = valuesProjection (Ω := swigΩ Ω) hZr_M2 := rfl
have hπC_def : π_C = valuesProjection (Ω := swigΩ Ω) hZrW_M2 := rfl
-- (i) globalMarkov_with_fixed (with Z_fix := M2.fixed) converts the
-- d-sep hypothesis into observational conditional independence.
have hCI : ObsCondIndep M2 Y Zr W hY_M2 hZr_M2 hW_M2 μ :=
globalMarkov_with_fixed M2 Y Zr W M2.fixed hY_M2 hZr_M2 hW_M2
(refl _) hdSep s
-- (ii) Symmetrize and apply Mathlib's `condIndepFun_iff_condDistrib_…`.
have hπY_meas : Measurable π_Y := measurable_valuesProjection _
have hπW_meas : Measurable π_W := measurable_valuesProjection _
have hπZr_meas : Measurable π_Zr := measurable_valuesProjection _
have hπC_meas : Measurable π_C := measurable_valuesProjection _
have hMathlib :
(fun ω => condDistrib π_Y
(fun ω' => (π_W ω', π_Zr ω')) μ ω)
=ᵐ[map
(fun ω' => (π_W ω', π_Zr ω')) μ]
(fun ω => (ProbabilityTheory.Kernel.prodMkRight
(ValuesOn Zr (swigΩ Ω))
(condDistrib π_Y π_W μ)) ω) :=
(ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight
(f := π_Y) (g := π_Zr) hπY_meas hπZr_meas hπW_meas).mp hCI.symm
-- (iii) Measurable equivalence `e : ValuesOn (Zr ∪ W) ≃ᵐ ValuesOn W × ValuesOn Zr`
-- via `valuesUnionEquiv` (giving `ValZr × ValW`) composed with `prodComm`.
let e : ValuesOn (Zr ∪ W) (swigΩ Ω) ≃ᵐ
ValuesOn W (swigΩ Ω) × ValuesOn Zr (swigΩ Ω) :=
(valuesUnionEquiv (A := Zr) (B := W) hDisj_ZrW).trans
(MeasurableEquiv.prodComm (α := ValuesOn Zr (swigΩ Ω))
(β := ValuesOn W (swigΩ Ω)))
have he_def : e = (valuesUnionEquiv (A := Zr) (B := W) hDisj_ZrW).trans
(MeasurableEquiv.prodComm (α := ValuesOn Zr (swigΩ Ω))
(β := ValuesOn W (swigΩ Ω))) := rfl
-- Pointwise: `e ∘ π_C = (π_W, π_Zr)` (both compute via valuesProjection of
-- subsets of `Zr ∪ W`).
have hW_sub : W ⊆ Zr ∪ W := Finset.subset_union_right
have hZr_sub : Zr ⊆ Zr ∪ W := Finset.subset_union_left
have h_e_comp : (fun ω => e (π_C ω)) = fun ω => (π_W ω, π_Zr ω) := by
funext ω
-- `e := (valuesUnionEquiv hDisj_ZrW).trans prodComm` gives at `π_C ω`:
-- `prodComm (valuesProjection subset_union_left (π_C ω),
-- valuesProjection subset_union_right (π_C ω))`
-- = `(valuesProjection subset_union_right (π_C ω),
-- valuesProjection subset_union_left (π_C ω))`.
-- Reduce LHS to the explicit pair form, then rewrite each coord.
have e_left :
valuesProjection hW_sub (π_C ω) = π_W ω := by
rw [hπW_def, hπC_def]
exact congrFun (valuesProjection_comp hW_sub hZrW_M2).symm ω
have e_right :
valuesProjection hZr_sub (π_C ω) = π_Zr ω := by
rw [hπZr_def, hπC_def]
exact congrFun (valuesProjection_comp hZr_sub hZrW_M2).symm ω
-- Both sides are pairs; use `Prod.ext` and pointwise.
apply Prod.ext
· -- `(e (π_C ω)).1 = π_W ω`
show valuesProjection hW_sub (π_C ω) = π_W ω
exact e_left
· show valuesProjection hZr_sub (π_C ω) = π_Zr ω
exact e_right
-- (iv) Use the change-of-variable lemma to transport `hMathlib` from
-- `μ.map (π_W, π_Zr)` ≡ `μ.map (e ∘ π_C)` to `μ.map π_C`-a.e.
have h_e_pi_C : ⇑e ∘ π_C = fun ω => (π_W ω, π_Zr ω) := by
funext ω; exact congrFun h_e_comp ω
-- Rewrite `μ.map (π_W, π_Zr)` to `μ.map (e ∘ π_C)`.
have hmap_eq :
map (fun ω => (π_W ω, π_Zr ω)) μ
= map (⇑e ∘ π_C) μ := by
rw [h_e_pi_C]
-- Apply the (C) helper: condDistrib π_Y (e ∘ π_C) μ (e c) = condDistrib π_Y π_C μ c
-- a.e. in c under μ.map π_C.
have h_cov : ∀ᵐ c ∂(μ.map π_C),
condDistrib π_Y (⇑e ∘ π_C) μ (e c)
= condDistrib π_Y π_C μ c :=
condDistrib_comp_right_measurableEquiv μ e hπY_meas hπC_meas
-- Transport `hMathlib` via `ae_of_ae_map` for `e`.
-- Step: `hMathlib` is ae on `μ.map (e ∘ π_C) = (μ.map π_C).map e`.
have hMathlib' :
(fun b => condDistrib π_Y
(fun ω' => (π_W ω', π_Zr ω')) μ b)
=ᵐ[map (⇑e ∘ π_C) μ]
(fun b => (ProbabilityTheory.Kernel.prodMkRight
(ValuesOn Zr (swigΩ Ω))
(condDistrib π_Y π_W μ)) b) := by
rw [← hmap_eq]; exact hMathlib
have hmap_compose : map (⇑e ∘ π_C) μ
= map ⇑e (μ.map π_C) :=
(MeasureTheory.Measure.map_map e.measurable hπC_meas).symm
rw [hmap_compose] at hMathlib'
have hMathlib_pulled :
∀ᵐ c ∂(μ.map π_C),
condDistrib π_Y
(fun ω' => (π_W ω', π_Zr ω')) μ (e c)
= (ProbabilityTheory.Kernel.prodMkRight
(ValuesOn Zr (swigΩ Ω))
(condDistrib π_Y π_W μ)) (e c) :=
MeasureTheory.ae_of_ae_map (μ := μ.map π_C) (f := ⇑e)
e.measurable.aemeasurable hMathlib'
-- (v) Bridge `condDistrib` back to `obsCondKernel` via
-- `obsCondKernel_ae_eq_condDistrib`, twice.
have h_bridge_C :
(fun c => M2.obsCondKernel Y (Zr ∪ W) hY_M2 hZrW_M2 (s, c))
=ᵐ[μ.map π_C]
condDistrib π_Y π_C μ :=
obsCondKernel_ae_eq_condDistrib M2 Y (Zr ∪ W) hY_M2 hZrW_M2 s
have h_bridge_W :
(fun w => M2.obsCondKernel Y W hY_M2 hW_M2 (s, w))
=ᵐ[μ.map π_W]
condDistrib π_Y π_W μ :=
obsCondKernel_ae_eq_condDistrib M2 Y W hY_M2 hW_M2 s
-- (vi) The RHS-side bridge transports `h_bridge_W` from `μ.map π_W`-a.e.
-- to `μ.map π_C`-a.e. via the projection `π_W^C : ValC → ValW`.
-- Note: `μ.map π_W = (μ.map π_C).map π_W^C` because `π_W = π_W^C ∘ π_C`.
let π_W_C : ValuesOn (Zr ∪ W) (swigΩ Ω) → ValuesOn W (swigΩ Ω) :=
valuesProjection hW_sub
have hπW_C_def : π_W_C = valuesProjection (Ω := swigΩ Ω) hW_sub := rfl
have hπW_C_meas : Measurable π_W_C := measurable_valuesProjection _
have hπW_factor : π_W = π_W_C ∘ π_C := by
rw [hπW_def, hπW_C_def, hπC_def]
exact valuesProjection_comp hW_sub hZrW_M2
have hmap_W_via_C :
μ.map π_W = (μ.map π_C).map π_W_C := by
rw [hπW_factor, ← MeasureTheory.Measure.map_map hπW_C_meas hπC_meas]
rw [hmap_W_via_C] at h_bridge_W
have h_bridge_W_pulled :
∀ᵐ c ∂(μ.map π_C),
M2.obsCondKernel Y W hY_M2 hW_M2 (s, π_W_C c)
= condDistrib π_Y π_W μ (π_W_C c) :=
MeasureTheory.ae_of_ae_map (μ := μ.map π_C) (f := π_W_C)
hπW_C_meas.aemeasurable h_bridge_W
-- (vii) Combine all ae statements and conclude.
filter_upwards [h_bridge_C, hMathlib_pulled, h_cov, h_bridge_W_pulled]
with c hbC hMl hcov hbW
-- Goal: M2.obsCondKernel Y (Zr ∪ W) (s, c) B
-- = M2.obsCondKernel Y W (s, π_W_C c) B
-- where π_W_C uses `subset_union_right`.
rw [hbC]
-- Now LHS: condDistrib π_Y π_C μ c B
rw [← hcov]
-- Now LHS: condDistrib π_Y (e ∘ π_C) μ (e c) B
-- … truncated; follow the source link for the rest …
lemma obsCondKernel_cross_SCM_ae_eq_on_fillZrW reviewed
⚑ flagged
Causalean.SCM
Cross-SCM conditional kernels agree along the fillZrW filled assignment. For the intervention on names Z, whose random copies are observed in the base model and whose fixed copies are not yet part of the base model's fixed coordinates, with outcome set Y contained in the observed variables and conditioning set W, the union of the random copies of Z and W contained in the observed variables with the random copies of Z disjoint from W, fix an intervened fixed assignment s; then for a measurable outcome set B and almost every conditioning value w, taken with respect to the pullback of the base model's law on Z.random ∪ W under the filled-assignment map, the base model's conditional distribution of Y given Z.random ∪ W, evaluated at the filled point built from w, and the intervened model's corresponding conditional distribution, evaluated at the same filled point, assign B the same probability.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
hY :
Y ⊆ M'.observed
hZrW :
Z.image SWIGNode.random ∪ W ⊆ M'.observed
hDisj_ZrW :
Disjoint (Z.image SWIGNode.random) W
CountableOrCountablyGenerated (M'.fixSet Z hZ_obs hZ_fixed).FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))
s :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
hB :
conclusion
∀ᵐ w ∂((map (valuesProjection hZrW) (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s))).comap (M'.fillZrW Z hZ_obs hZ_fixed W s)), (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (M'.fixSetProj Z hZ_obs hZ_fixed s, M'.fillZrW Z hZ_obs hZ_fixed W s w)) B
= ((M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y (Z.image SWIGNode.random ∪ W) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY) ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW) (s, M'.fillZrW Z hZ_obs hZ_fixed W s w)) B
Proof (Lean source)
lemma obsCondKernel_cross_SCM_ae_eq_on_fillZrW
(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)
(hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed)
(hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W)
[StandardBorelSpace (ValuesOn Y (swigΩ Ω))]
[Nonempty (ValuesOn Y (swigΩ Ω))]
[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Ω Ω))]
[MeasurableSingletonClass
(ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))]
(s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues)
{B : Set (ValuesOn Y (swigΩ Ω))} (hB : MeasurableSet B) :
∀ᵐ w ∂((map (valuesProjection hZrW)
(M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s))).comap
(M'.fillZrW Z hZ_obs hZ_fixed W s)),
(M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW
(M'.fixSetProj Z hZ_obs hZ_fixed s,
M'.fillZrW Z hZ_obs hZ_fixed W s w)) B
= ((M'.fixSet Z hZ_obs hZ_fixed).obsCondKernel Y
(Z.image SWIGNode.random ∪ W)
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY)
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW)
(s, M'.fillZrW Z hZ_obs hZ_fixed W s w)) B := by
-- Proof skeleton for the rectangle identity. The measure-uniqueness bridge
-- is packaged in the helper lemmas below; this block keeps the notation
-- aligned with the obs-side and do-side kernels.
--
-- Notation.
-- M1 := M',
-- M2 := M'.fixSet Z _ _,
-- sM1 := M'.fixSetProj Z _ _ s,
-- F := M'.fillZrW Z _ _ W s,
-- C := Z.image .random ∪ W,
-- μ_C := (M1.obsKernel sM1).map π_C (M1 marginal on C)
-- ν_C := (M2.obsKernel s ).map π_C (M2 marginal on C)
-- μ_F := μ_C.comap F (pullback via the
-- measurable embedding F)
-- f1 w := M1.obsCondKernel Y C (sM1, F w) B,
-- f2 w := M2.obsCondKernel Y C (s , F w) B.
--
-- We want `f1 =ᵐ[μ_F] f2`. By
-- `MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite` it
-- suffices to check, for every measurable `A ⊆ ValuesOn W`,
--
-- ∫_A f1 dμ_F = ∫_A f2 dμ_F. (★)
--
-- Reducing both sides to the rectangle measure
-- `M.obsKernel _ (π_C⁻¹ F''A ∩ π_Y⁻¹ B)`:
--
-- LHS (★) chain.
-- ∫_A f1 dμ_F
-- = ∫_{F''A} g1 c dμ_C [MeasurableEmbedding.comap +
-- `lintegral_indicator`,
-- restriction along F]
-- = M1.obsKernel sM1 (π_C⁻¹ F''A ∩ π_Y⁻¹ B)
-- [`obsKernel_disintegrate_rect`
-- with `M := M1`, `D := F''A`]
-- = M2.obsKernel s (π_C⁻¹ F''A ∩ π_Y⁻¹ B)
-- [`obsKernel_inter_Wset_Zrand_levelset_eq`
-- with `S := π_Y⁻¹ B`]
--
-- RHS (★) chain.
-- ∫_A f2 dμ_F
-- = ∫_{F''A} g2 c dμ_C|_{range F} [same comap rewrite]
-- = ∫_{F''A} g2 c dν_C [restricted range measure equality]
-- = M2.obsKernel s (π_C⁻¹ F''A ∩ π_Y⁻¹ B) [`obsKernel_disintegrate_rect`
-- with `M := M2`]
--
-- The two chains coincide exactly after proving the restricted range equality
--
-- μ_C |_{range F} = ν_C |_{range F} as measures on range F, (♭)
--
-- holds. The π-system of filled-assignment cylinders `{ F''A_W : A_W meas }`
-- generates the trace σ-algebra on range F, and
-- `obsKernel_inter_Wset_Zrand_levelset_eq` with `S := univ` shows the
-- two measures agree on each such cylinder; promoting this to a full
-- The proof splits into the measure equality on `range F` and the
-- disintegration-uniqueness step on that range. The helper infrastructure
-- below packages the measurable-embedding and restricted-measure facts used
-- in those two steps.
classical
let M2 := M'.fixSet Z hZ_obs hZ_fixed
let sM1 : M'.FixedValues := M'.fixSetProj Z hZ_obs hZ_fixed s
let Zr := Z.image SWIGNode.random
let F := M'.fillZrW Z hZ_obs hZ_fixed W s
have hM2_def : M2 = M'.fixSet Z hZ_obs hZ_fixed := rfl
have hsM1_def : sM1 = M'.fixSetProj Z hZ_obs hZ_fixed s := rfl
have hZr_def : Zr = Z.image SWIGNode.random := rfl
have hF_def : F = M'.fillZrW Z hZ_obs hZ_fixed W s := rfl
have hZrW_M2 : Zr ∪ W ⊆ M2.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW
-- F is a measurable embedding.
have hF_emb : MeasurableEmbedding F :=
measurableEmbedding_fillZrW M' Z hZ_obs hZ_fixed W hDisj_ZrW s
-- μ_C and ν_C: M1 and M2 marginal pushforwards on C := Zr ∪ W.
let μ_C : Measure (ValuesOn (Zr ∪ W) (swigΩ Ω)) :=
(M'.obsKernel sM1).map (valuesProjection hZrW)
let ν_C : Measure (ValuesOn (Zr ∪ W) (swigΩ Ω)) :=
(M2.obsKernel s).map (valuesProjection hZrW_M2)
have hμC_def : μ_C =
(M'.obsKernel sM1).map (valuesProjection (Ω := swigΩ Ω) hZrW) := rfl
have hνC_def : ν_C =
(M2.obsKernel s).map (valuesProjection (Ω := swigΩ Ω) hZrW_M2) := rfl
-- Both μ_C and ν_C are finite (pushforwards of finite measures).
have hπC_M1_meas : Measurable (valuesProjection (Ω := swigΩ Ω) hZrW) :=
measurable_valuesProjection _
have hπC_M2_meas : Measurable (valuesProjection (Ω := swigΩ Ω) hZrW_M2) :=
measurable_valuesProjection _
haveI : IsFiniteMeasure μ_C := by
rw [hμC_def]; exact (M'.obsKernel sM1).isFiniteMeasure_map _
haveI : IsFiniteMeasure ν_C := by
rw [hνC_def]; exact (M2.obsKernel s).isFiniteMeasure_map _
----------------------------------------------------------------
-- **Part A** : `μ_C.restrict (range F) = ν_C.restrict (range F)`.
----------------------------------------------------------------
have hPartA :
μ_C.restrict (range F) = ν_C.restrict (range F) := by
refine
restrict_range_eq_of_forall_image hF_emb μ_C ν_C
?_
intro A hA
-- ν_C (F''A) = M2.obsKernel s (π_C^{M2}⁻¹(F''A))
-- μ_C (F''A) = M1.obsKernel sM1 (π_C^{M1}⁻¹(F''A))
-- The cross-SCM cylinder bridge with `S := univ` gives equality.
have hImg_meas : MeasurableSet (F '' A) := hF_emb.measurableSet_image' hA
have hMap_M1 :
μ_C (F '' A)
= M'.obsKernel sM1
((valuesProjection hZrW)⁻¹' (F '' A)) := by
rw [hμC_def, MeasureTheory.Measure.map_apply hπC_M1_meas hImg_meas]
have hMap_M2 :
ν_C (F '' A)
= M2.obsKernel s
((valuesProjection hZrW_M2)⁻¹' (F '' A)) := by
rw [hνC_def, MeasureTheory.Measure.map_apply hπC_M2_meas hImg_meas]
-- Cross-SCM bridge with S := univ.
have hBridge :
M2.obsKernel s
(univ ∩ (valuesProjection hZrW_M2)⁻¹' (F '' A))
= M'.obsKernel sM1
(univ ∩ (valuesProjection hZrW)⁻¹' (F '' A)) :=
obsKernel_inter_Wset_Zrand_levelset_eq M' Z hZ_obs hZ_fixed W
hZrW hDisj_ZrW s MeasurableSet.univ hA
rw [Set.univ_inter, Set.univ_inter] at hBridge
rw [hMap_M1, hMap_M2, hBridge]
----------------------------------------------------------------
-- **Part B** : disintegration uniqueness on `range F`.
--
-- From `hPartA`, the M1 and M2 joint measures agree on every set of
-- the form `π_C⁻¹ E ∩ π_Y⁻¹ B` for measurable `E ⊆ range F`. Their
-- disintegrations along `π_C` (via `obsKernel_disintegrate_rect`)
-- coincide as the same conditional kernel up to a μ_C|_{range F}-null
-- set. Concretely, for every measurable `E ⊆ ValuesOn (Zr ∪ W)`:
--
-- ∫⁻ c in E ∩ range F, M1.obsCondKernel Y C (sM1, c) B dμ_C
-- = M1.obsKernel sM1 (π_C⁻¹ (E ∩ range F) ∩ π_Y⁻¹ B)
-- = M2.obsKernel s (π_C⁻¹ (E ∩ range F) ∩ π_Y⁻¹ B) -- bridge
-- = ∫⁻ c in E ∩ range F, M2.obsCondKernel Y C (s, c) B dν_C
-- = ∫⁻ c in E ∩ range F, M2.obsCondKernel Y C (s, c) B dμ_C
-- -- via Part A
--
-- Apply `MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite`
-- to `g1 c := M1.obsCondKernel Y C (sM1, c) B` and
-- `g2 c := M2.obsCondKernel Y C (s, c) B` on `μ_C.restrict (range F)`.
-- Then transport `g1 ∘ F =ᵐ[μ_F] g2 ∘ F` from
-- `g1 =ᵐ[μ_C.restrict (range F)] g2` via
-- `MeasurableEmbedding.ae_map_iff` and `hF_emb.map_comap`.
--
----------------------------------------------------------------
-- **Part B** : disintegration uniqueness on `range F`.
----------------------------------------------------------------
-- M2-side `Y ⊆ M2.observed`.
have hY_M2 : Y ⊆ M2.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY
-- Measurability of the π_Y-preimage of B on both sides.
have hπY_M1_meas : Measurable (valuesProjection (Ω := swigΩ Ω) hY) :=
measurable_valuesProjection _
have hπY_M2_meas : Measurable (valuesProjection (Ω := swigΩ Ω) hY_M2) :=
measurable_valuesProjection _
have hπYB_M1 : MeasurableSet ((valuesProjection (Ω := swigΩ Ω) hY)⁻¹' B) :=
hπY_M1_meas hB
have hπYB_M2 : MeasurableSet ((valuesProjection (Ω := swigΩ Ω) hY_M2)⁻¹' B) :=
hπY_M2_meas hB
-- The integrand functions `f1`, `f2` (M1 and M2 conditional kernels at B).
let f1 : ValuesOn (Zr ∪ W) (swigΩ Ω) → ENNReal :=
fun c => M'.obsCondKernel Y (Zr ∪ W) hY hZrW (sM1, c) B
let f2 : ValuesOn (Zr ∪ W) (swigΩ Ω) → ENNReal :=
fun c => M2.obsCondKernel Y (Zr ∪ W) hY_M2 hZrW_M2 (s, c) B
have hf1_meas : Measurable f1 :=
(ProbabilityTheory.Kernel.measurable_coe _ hB).comp
(prodMk measurable_const measurable_id)
have hf2_meas : Measurable f2 :=
(ProbabilityTheory.Kernel.measurable_coe _ hB).comp
(prodMk measurable_const measurable_id)
-- **Step 1.** For every measurable `A ⊆ ValuesOn W`,
-- … truncated; follow the source link for the rest …
WMarginal 2 core · 4 supporting This file proves the filled-assignment measure identities used in the conditional version of Rule 2. ★ obsKernel_fixSet_W_marginal_pushforward_eq★ obsKernel_fixSet_W_rect_integral_eq
Marginal Identities for Rule 2
This file proves the filled-assignment measure identities used in the
conditional version of Rule 2. The helper lemmas describe the image of a
measurable W-event under fillZrW, prove that fillZrW is injective and a
measurable embedding, and use that embedding in
obsKernel_fixSet_W_marginal_pushforward_eq. The theorem
obsKernel_fixSet_W_rect_integral_eq then gives the rectangle integral identity
under the explicit hypothesis that the intervened random treatment copies equal
their assigned fixed intervention values almost surely. These conditional
identities are later upgraded to the full kernel statement of Rule 2.
lemma obsKernel_fixSet_W_marginal_pushforward_eq reviewed
⚑ flagged
Causalean.SCM
W-marginal pushforward identity. 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 an observation block W such that the union of Z's random copies and W is observed and disjoint from Z's random copies. If, under the intervened model's law of the observed variables given the fixed values s', the post-intervention random copies of Z almost surely equal their assigned intervention values, then for every measurable W-event A, the intervened model's marginal probability of A on W equals the base model's probability of the image of A under the map that fills in the pinned Z-random-copy coordinates alongside W.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
hZrW :
Z.image SWIGNode.random ∪ W ⊆ M'.observed
hDisj_ZrW :
Disjoint (Z.image SWIGNode.random) W
s' :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
hPinned :
∀ᵐ ω ∂((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s'), ∀ D (hD : D ∈ Z), ω ⟨SWIGNode.random D, hZ_obs D hD⟩
= s' ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩
hA :
conclusion
((map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ (by intro v hv exact hZrW (mem_union_right _ hv)))) ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s'))) A
= ((map (valuesProjection hZrW) (M'.obsKernel (M'.fixSetProj Z hZ_obs hZ_fixed s')))) ((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A)
Proof (Lean source)
lemma obsKernel_fixSet_W_marginal_pushforward_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)
(W : Finset (SWIGNode N))
(hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed)
(hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W)
[MeasurableSingletonClass
(ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))]
(s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues)
(hPinned : ∀ᵐ ω ∂((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s'),
∀ D (hD : D ∈ Z),
ω ⟨SWIGNode.random D, hZ_obs D hD⟩
= s' ⟨SWIGNode.fixed D,
SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩)
{A : Set (ValuesOn W (swigΩ Ω))} (hA : MeasurableSet A) :
((map
(valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸
(by
intro v hv
exact hZrW (mem_union_right _ hv))))
((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s'))) A
= ((map
(valuesProjection hZrW)
(M'.obsKernel
(M'.fixSetProj Z hZ_obs hZ_fixed s'))))
((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A) := by
classical
have hW : W ⊆ M'.observed := by
intro v hv
exact hZrW (mem_union_right _ hv)
-- Abbreviations.
let M2 := M'.fixSet Z hZ_obs hZ_fixed
let sM1 : M'.FixedValues := M'.fixSetProj Z hZ_obs hZ_fixed s'
let F := M'.fillZrW Z hZ_obs hZ_fixed W s'
have hZrW_M2 : Z.image SWIGNode.random ∪ W ⊆ M2.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW
have hW_M2 : W ⊆ M2.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW
have hπW_M2 : Measurable
(valuesProjection hW_M2 : M2.ObservedValues → _) :=
measurable_valuesProjection _
have hπC_M1 : Measurable
(valuesProjection hZrW : M'.ObservedValues → _) :=
measurable_valuesProjection _
have hImg_meas : MeasurableSet (F '' A) :=
measurableSet_fillZrW_image M' Z hZ_obs hZ_fixed W hDisj_ZrW s' hA
-- Rewrite the maps as obsKernel applied to preimages.
rw [MeasureTheory.Measure.map_apply hπW_M2 hA,
MeasureTheory.Measure.map_apply hπC_M1 hImg_meas]
-- Now: M2.obsKernel s' (π_W⁻¹ A) = M1.obsKernel sM1 (π_C⁻¹ (F''A)).
-- Step 1: by (★), M2(π_W⁻¹A) = M2(π_W⁻¹A ∩ π_Zr⁻¹ {ζ_s}).
-- We instead show that π_W⁻¹A = π_C⁻¹(F''A) ∪ N for a null set N under M2,
-- and π_C⁻¹(F''A) ⊆ π_W⁻¹A. Then the measures are equal.
-- Concrete plan: show that on the event {ω : π_Zr ω = ζ_s} (M2-a.e.),
-- π_W ω ∈ A ↔ π_C ω ∈ F''A,
-- so the two preimages agree M2-a.e.
set ζ_s : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) :=
zFixedAsRandom
(valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s')
with hζ_def
have hZr_subset : Z.image SWIGNode.random ⊆ M2.observed := by
intro v hv
exact hZrW_M2 (subset_union_left hv)
have hImgExpand : F '' A =
(fun c : ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) =>
valuesProjection
(Finset.subset_union_right (s₁ := Z.image SWIGNode.random)) c)⁻¹' A ∩
(fun c => valuesProjection
(subset_union_left (s₂ := W)) c)⁻¹' ({ζ_s} :
Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))) :=
fillZrW_image_eq M' Z hZ_obs hZ_fixed W hDisj_ZrW s' A
-- Step A: apply Helper 1 with S := π_W⁻¹A to get
-- M2(π_W⁻¹A ∩ π_C⁻¹(F''A)) = M1(π_W⁻¹A ∩ π_C⁻¹(F''A))
-- (where π_W⁻¹A on the M2 side uses hW_M2; same on M1 side with hW).
-- But we want bare π_C⁻¹(F''A), so use S = univ.
have hHelper1 :
M2.obsKernel s'
(univ ∩ (valuesProjection hZrW_M2)⁻¹' (F '' A))
= M'.obsKernel sM1
(univ ∩ (valuesProjection hZrW)⁻¹' (F '' A)) :=
obsKernel_inter_Wset_Zrand_levelset_eq M' Z hZ_obs hZ_fixed W
hZrW hDisj_ZrW s' MeasurableSet.univ hA
rw [Set.univ_inter, Set.univ_inter] at hHelper1
-- Now rewrite RHS = M1(π_C⁻¹(F''A)) using hHelper1 (reversed).
rw [← hHelper1]
-- Goal: M2.obsKernel s' (π_W⁻¹ A) = M2.obsKernel s' (π_C⁻¹ (F '' A))
-- where π_W uses hW_M2 and π_C uses hZrW_M2.
-- Use the (★) hypothesis to show these sets agree M2-a.e.
refine MeasureTheory.measure_congr ?_
refine Filter.Eventually.mono hPinned ?_
intro ω hω
-- hω : ∀ D ∈ Z, ω ⟨.random D, hZ_obs D _⟩ = s' ⟨.fixed D, _⟩
-- Show: π_W⁻¹A ω ↔ π_C⁻¹(F''A) ω
apply propext
constructor
· intro hπW_mem
-- We have π_W ω ∈ A. Show π_C ω ∈ F''A by exhibiting `w = π_W ω`.
change ω ∈ valuesProjection hZrW_M2 ⁻¹' (F '' A)
refine ⟨valuesProjection hW_M2 ω, hπW_mem, ?_⟩
funext ⟨v, hv⟩
simp only [F, fillZrW]
rcases Finset.mem_union.mp hv with hZrV | hWV
· rw [valuesUnionMk_apply_left _ _ hZrV]
obtain ⟨D, hDZ, hDeq⟩ := Finset.mem_image.mp hZrV
cases hDeq
simp only [zFixedAsRandom, valuesProjection]
-- Goal: s' ⟨.fixed D, _⟩ = ω ⟨.random D, _⟩ (from valuesUnionMk_apply_left)
exact (hω D hDZ).symm
· by_cases hZrV' : v ∈ Z.image SWIGNode.random
· rw [valuesUnionMk_apply_left _ _ hZrV']
obtain ⟨D, hDZ, hDeq⟩ := Finset.mem_image.mp hZrV'
cases hDeq
simp only [zFixedAsRandom, valuesProjection]
exact (hω D hDZ).symm
· rw [valuesUnionMk_apply_right _ _ _ hZrV']
simp only [valuesProjection]
· intro hMem
-- π_C ω = F w₀ for some w₀ ∈ A. Show π_W ω ∈ A.
obtain ⟨w₀, hw₀A, hF_eq⟩ := hMem
-- The W-coordinate of F w₀ equals w₀ (since W is disjoint from Z.image .random).
suffices h : valuesProjection hW_M2 ω = w₀ by
change ω ∈ valuesProjection hW_M2 ⁻¹' A
rw [Set.mem_preimage, h]; exact hw₀A
funext ⟨v, hvW⟩
have hv_in : v ∈ Z.image SWIGNode.random ∪ W :=
Finset.subset_union_right hvW
have hvNotZr : v ∉ Z.image SWIGNode.random := fun hvZr =>
Finset.disjoint_left.mp hDisj_ZrW hvZr hvW
have hcoord := congrFun hF_eq ⟨v, hv_in⟩
simp only [valuesProjection, F, fillZrW] at hcoord ⊢
rw [valuesUnionMk_apply_right _ _ hv_in hvNotZr] at hcoord
exact hcoord.symm
theorem obsKernel_fixSet_W_rect_integral_eq reviewed
⚑ flagged
Causalean.SCM
Cross-SCM rectangle bridge for the W-marginal. 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, together with an outcome block Y and a conditioning block W of observed variables such that the union of Z's random copies and W is observed and disjoint from Z's random copies. At fixed values s, assume that under the intervened model's law, the post-intervention random copies of Z almost surely equal their assigned intervention values. Then for every measurable W-event A and every measurable Y-event B, integrating, over A and with respect to the intervened model's W-marginal, the base model's conditional probability of B given the outcome of filling in Z's pinned random-copy values alongside each w reconstructs the intervened model's probability that both the W-event A and the Y-event B occur.
Formal statement
hypotheses
N :
Type u_1
N → Type u_2
M' :
SCM N Ω
Z :
Finset N
hZ_obs :
∀ D ∈ Z, SWIGNode.random D ∈ M'.observed
hZ_fixed :
∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed
hY :
Y ⊆ M'.observed
hW :
W ⊆ M'.observed
hZrW :
Z.image SWIGNode.random ∪ W ⊆ M'.observed
hDisj_ZrW :
Disjoint (Z.image SWIGNode.random) W
s :
(M'.fixSet Z hZ_obs hZ_fixed).FixedValues
hPinned :
∀ᵐ ω ∂((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s), ∀ D (hD : D ∈ Z), ω ⟨SWIGNode.random D, hZ_obs D hD⟩
= s ⟨SWIGNode.fixed D, SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩
hA :
hB :
conclusion
∫⁻ w in A, (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW (M'.fixSetProj Z hZ_obs hZ_fixed s, M'.fillZrW Z hZ_obs hZ_fixed W s w)) B ∂(map (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW)) ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s))
= ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s) ((valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW))⁻¹' A ∩ (valuesProjection ((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY))⁻¹' B)
Proof (Lean source)
theorem obsKernel_fixSet_W_rect_integral_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)
(Y W : Finset (SWIGNode N))
(hY : Y ⊆ M'.observed) (hW : W ⊆ M'.observed)
(hZrW : Z.image SWIGNode.random ∪ W ⊆ M'.observed)
(hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W)
[StandardBorelSpace (ValuesOn Y (swigΩ Ω))]
[Nonempty (ValuesOn Y (swigΩ Ω))]
[CountableOrCountablyGenerated
M'.FixedValues (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))]
[MeasurableSingletonClass
(ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))]
(s : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues)
(hPinned : ∀ᵐ ω ∂((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s),
∀ D (hD : D ∈ Z),
ω ⟨SWIGNode.random D, hZ_obs D hD⟩
= s ⟨SWIGNode.fixed D,
SCM.fixed_mem_fixSet M' Z hZ_obs hZ_fixed hD⟩)
{A : Set (ValuesOn W (swigΩ Ω))}
{B : Set (ValuesOn Y (swigΩ Ω))}
(hA : MeasurableSet A) (hB : MeasurableSet B) :
∫⁻ w in A,
(M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW
(M'.fixSetProj Z hZ_obs hZ_fixed s,
M'.fillZrW Z hZ_obs hZ_fixed W s w)) B
∂(map
(valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW))
((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s))
= ((M'.fixSet Z hZ_obs hZ_fixed).obsKernel s)
((valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW))⁻¹' A
∩ (valuesProjection
((fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY))⁻¹' B) := by
-- ============================================================
-- Proof strategy (using the (★) hypothesis `hPinned`):
--
-- Let M1 = M', M2 = M'.fixSet Z hZ_obs hZ_fixed,
-- sM1 = M'.fixSetProj Z hZ_obs hZ_fixed s,
-- F = fillZrW Z hZ_obs hZ_fixed W s.
-- Let ν_W := (M2.obsKernel s).map π_W, μ_C := (M1.obsKernel sM1).map π_C.
-- Let ĥ(c) := M1.obsCondKernel Y (Z.image .random ∪ W) (sM1, c) B.
--
-- LHS = ∫⁻ w in A, ĥ(F w) d ν_W
-- = ∫⁻ c in F''A, ĥ(c) d (ν_W.map F) [change of vars, F MeasEmb]
-- = ∫⁻ c in F''A, ĥ(c) d (μ_C.restrict (range F))[ν_W = μ_C.comap F via helper]
-- = ∫⁻ c in F''A, ĥ(c) d μ_C [F''A ⊆ range F]
-- = M1.obsKernel sM1 (π_C⁻¹(F''A) ∩ π_Y⁻¹ B) [Helper 2 / M1 disintegration]
-- = M2.obsKernel s (π_C⁻¹(F''A) ∩ π_Y⁻¹ B) [Helper 1, S := π_Y⁻¹B]
-- = M2.obsKernel s (π_W⁻¹A ∩ π_Y⁻¹ B) [by (★) and hImg]
-- = RHS.
-- ============================================================
classical
let M1 := M'
let M2 := M'.fixSet Z hZ_obs hZ_fixed
let sM1 : M1.FixedValues := M'.fixSetProj Z hZ_obs hZ_fixed s
let F := M'.fillZrW Z hZ_obs hZ_fixed W s
have hZrW_M2 : Z.image SWIGNode.random ∪ W ⊆ M2.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hZrW
have hW_M2 : W ⊆ M2.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hW
have hY_M2 : Y ⊆ M2.observed :=
(fixSet_observed M' Z hZ_obs hZ_fixed).symm ▸ hY
-- F is a MeasurableEmbedding.
have hME : MeasurableEmbedding F :=
measurableEmbedding_fillZrW M' Z hZ_obs hZ_fixed W hDisj_ZrW s
have hF_meas : Measurable F :=
M'.measurable_fillZrW Z hZ_obs hZ_fixed W s
have hπW_M2 : Measurable
(valuesProjection hW_M2 : M2.ObservedValues → _) :=
measurable_valuesProjection _
have hπC_M1 : Measurable
(valuesProjection hZrW : M1.ObservedValues → _) :=
measurable_valuesProjection _
have hπC_M2 : Measurable
(valuesProjection hZrW_M2 : M2.ObservedValues → _) :=
measurable_valuesProjection _
have hπY_M2 : Measurable
(valuesProjection hY_M2 : M2.ObservedValues → _) :=
measurable_valuesProjection _
have hπY_M1 : Measurable
(valuesProjection hY : M1.ObservedValues → _) :=
measurable_valuesProjection _
-- Abbreviations for measures and integrand.
set ν_W : Measure (ValuesOn W (swigΩ Ω)) :=
(M2.obsKernel s).map (valuesProjection hW_M2) with hν_W_def
set μ_C : Measure
(ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω)) :=
(M1.obsKernel sM1).map (valuesProjection hZrW) with hμ_C_def
let ĥ : ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) → ENNReal :=
fun c => (M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW
(sM1, c)) B
-- Image of A is measurable in `ValuesOn (Z.image .random ∪ W)`.
have hImg_meas : MeasurableSet (F '' A) := hME.measurableSet_image' hA
-- The pushforward identity from the helper.
have hPushApply : ∀ ⦃S : Set (ValuesOn W (swigΩ Ω))⦄, MeasurableSet S →
ν_W S = μ_C (F '' S) := by
intro S hS
simp only [hν_W_def, hμ_C_def]
exact obsKernel_fixSet_W_marginal_pushforward_eq M' Z hZ_obs hZ_fixed W
hZrW hDisj_ZrW s hPinned hS
-- ν_W = μ_C.comap F as measures on `ValuesOn W`.
have hcomap_eq : ν_W = μ_C.comap F := by
refine MeasureTheory.Measure.ext ?_
intro S hS
rw [hME.comap_apply, hPushApply hS]
-- ν_W.map F = μ_C.restrict (range F).
have hmap_F : ν_W.map F = μ_C.restrict (range F) := by
rw [hcomap_eq, hME.map_comap]
-- ----------------------------------------------------------------
-- Step 1: rewrite LHS using `MeasurableEmbedding.lintegral_map`.
-- LHS = ∫⁻ c in F''A, ĥ(c) d (ν_W.map F).
-- ----------------------------------------------------------------
-- The current LHS displays the measure as
-- `Measure.map (valuesProjection ((fixSet_observed ...).symm ▸ hW)) (M2.obsKernel s)`
-- which is definitionally equal to `ν_W`. Likewise the integrand is `ĥ ∘ F`.
have hLHS_step1 :
∫⁻ w in A,
(M'.obsCondKernel Y (Z.image SWIGNode.random ∪ W) hY hZrW
(sM1, F w)) B ∂ν_W
= ∫⁻ c in F '' A, ĥ c ∂(ν_W.map F) := by
-- ∫⁻ c in F''A, ĥ c d (ν_W.map F)
-- = ∫⁻ c, indicator(F''A) c · ĥ c d (ν_W.map F)
-- = ∫⁻ w, indicator(F''A) (F w) · ĥ (F w) d ν_W [lintegral_map]
-- = ∫⁻ w, indicator(A) w · ĥ (F w) d ν_W [F injective]
-- = ∫⁻ w in A, ĥ (F w) d ν_W
rw [← MeasureTheory.lintegral_indicator hImg_meas,
hME.lintegral_map (fun c => (F '' A).indicator ĥ c),
← MeasureTheory.lintegral_indicator hA]
refine MeasureTheory.lintegral_congr ?_
intro w
by_cases hw : w ∈ A
· have hFw : F w ∈ F '' A := ⟨w, hw, rfl⟩
simp [Set.indicator_of_mem hw, Set.indicator_of_mem hFw, ĥ]
· have hFw : F w ∉ F '' A := by
rintro ⟨w', hw', heq⟩
exact hw (hME.injective heq ▸ hw')
simp [Set.indicator_of_notMem hw, Set.indicator_of_notMem hFw]
-- ----------------------------------------------------------------
-- Step 2: ∫⁻ c in F''A, ĥ d (ν_W.map F) = ∫⁻ c in F''A, ĥ d μ_C
-- using ν_W.map F = μ_C.restrict (range F) and F''A ⊆ range F.
-- ----------------------------------------------------------------
have hRangeF : F '' A ⊆ range F :=
Set.image_subset_range _ _
have hLHS_step2 :
∫⁻ c in F '' A, ĥ c ∂(ν_W.map F)
= ∫⁻ c in F '' A, ĥ c ∂μ_C := by
rw [hmap_F]
-- (μ_C.restrict (range F)).restrict (F''A) = μ_C.restrict ((F''A) ∩ range F)
-- = μ_C.restrict (F''A) since F''A ⊆ range F.
rw [MeasureTheory.Measure.restrict_restrict_of_subset hRangeF]
-- ----------------------------------------------------------------
-- Step 3: ∫⁻ c in F''A, ĥ d μ_C = M1.obsKernel sM1 (π_C⁻¹ (F''A) ∩ π_Y⁻¹ B)
-- via Helper 2 (M1 disintegration along π_C, CC := Z.image .random ∪ W).
-- ----------------------------------------------------------------
have hLHS_step3 :
∫⁻ c in F '' A, ĥ c ∂μ_C
= M1.obsKernel sM1
((valuesProjection hZrW)⁻¹' (F '' A)
∩ (valuesProjection hY)⁻¹' B) := by
rw [hμ_C_def]
exact (obsKernel_disintegrate_rect M1 Y (Z.image SWIGNode.random ∪ W)
hY hZrW sM1 hImg_meas hB).symm
-- ----------------------------------------------------------------
-- Step 4: swap M1 to M2 using Helper 1 (S := π_Y⁻¹ B).
-- ----------------------------------------------------------------
have hHelper1 :
M2.obsKernel s
((valuesProjection hY_M2)⁻¹' B
∩ (valuesProjection hZrW_M2)⁻¹' (F '' A))
= M1.obsKernel sM1
((valuesProjection hY)⁻¹' B
∩ (valuesProjection hZrW)⁻¹' (F '' A)) :=
obsKernel_inter_Wset_Zrand_levelset_eq M' Z hZ_obs hZ_fixed W
hZrW hDisj_ZrW s (hπY_M1 hB) hA
-- Both intersections appear in either order: align via Set.inter_comm.
have hLHS_step4 :
M1.obsKernel sM1
((valuesProjection hZrW)⁻¹' (F '' A)
∩ (valuesProjection hY)⁻¹' B)
= M2.obsKernel s
((valuesProjection hZrW_M2)⁻¹' (F '' A)
∩ (valuesProjection hY_M2)⁻¹' B) := by
rw [Set.inter_comm ((valuesProjection hZrW)⁻¹' (F '' A))
((valuesProjection hY)⁻¹' B),
Set.inter_comm ((valuesProjection hZrW_M2)⁻¹' (F '' A))
((valuesProjection hY_M2)⁻¹' B)]
exact hHelper1.symm
-- ----------------------------------------------------------------
-- Step 5: M2(π_C⁻¹(F''A) ∩ π_Y⁻¹B) = M2(π_W⁻¹A ∩ π_Y⁻¹B) by (★).
-- ----------------------------------------------------------------
have hLHS_step5 :
M2.obsKernel s
((valuesProjection hZrW_M2)⁻¹' (F '' A)
∩ (valuesProjection hY_M2)⁻¹' B)
= M2.obsKernel s
((valuesProjection hW_M2)⁻¹' A
∩ (valuesProjection hY_M2)⁻¹' B) := by
refine MeasureTheory.measure_congr ?_
refine Filter.Eventually.mono hPinned ?_
intro ω hω
-- Show: ω ∈ π_C⁻¹(F''A) ∩ π_Y⁻¹B ↔ ω ∈ π_W⁻¹A ∩ π_Y⁻¹B
apply propext
constructor
· rintro ⟨hπCmem, hπYmem⟩
refine ⟨?_, hπYmem⟩
-- ω ∈ π_C⁻¹(F''A) gives w₀ ∈ A with F w₀ = π_C ω.
-- W-coord of F w₀ is w₀; project to extract.
obtain ⟨w₀, hw₀A, hF_eq⟩ := hπCmem
change ω ∈ valuesProjection hW_M2 ⁻¹' A
suffices h : valuesProjection hW_M2 ω = w₀ by
rw [Set.mem_preimage, h]; exact hw₀A
funext ⟨v, hvW⟩
have hv_in : v ∈ Z.image SWIGNode.random ∪ W :=
Finset.subset_union_right hvW
have hvNotZr : v ∉ Z.image SWIGNode.random := fun hvZr =>
Finset.disjoint_left.mp hDisj_ZrW hvZr hvW
have hcoord := congrFun hF_eq ⟨v, hv_in⟩
simp only [valuesProjection, F, fillZrW] at hcoord ⊢
rw [valuesUnionMk_apply_right _ _ hv_in hvNotZr] at hcoord
-- … truncated; follow the source link for the rest …
4 supporting declarations (lemmas, instances)
-
fillZrW_image_eqlemma — The image of a W-event under the filled-assignment map fillZrW Z hZ_obs hZ_fixed W s is exactly the set of assignments on Z.image .random ∪ W whose W-projection lies in the event and whose Z.image .random projection equals the fixed intervention value zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset ...) s).hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhDisj_ZrW :Disjoint (Z.image SWIGNode.random) Ws' :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesconclusion(M'.fillZrW Z hZ_obs hZ_fixed W s') '' A= (fun c : ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) => valuesProjection (subset_union_right (s₁ := Z.image SWIGNode.random)) c)⁻¹' A ∩ (fun c => valuesProjection (subset_union_left (s₂ := W)) c)⁻¹' ({zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s')} : Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω)))Proof (Lean source)
lemma fillZrW_image_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) (W : Finset (SWIGNode N)) (hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W) (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) (A : Set (ValuesOn W (swigΩ Ω))) : (M'.fillZrW Z hZ_obs hZ_fixed W s') '' A = (fun c : ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω) => valuesProjection (Finset.subset_union_right (s₁ := Z.image SWIGNode.random)) c)⁻¹' A ∩ (fun c => valuesProjection (subset_union_left (s₂ := W)) c)⁻¹' ({zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s')} : Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))) := by classical let F := M'.fillZrW Z hZ_obs hZ_fixed W s' let ζ_s : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) := zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s') ext c constructor · rintro ⟨w, hwA, rfl⟩ refine ⟨?_, ?_⟩ · simp only [Set.mem_preimage] have : valuesProjection (Finset.subset_union_right : W ⊆ _) (F w) = w := by funext ⟨v, hv⟩ simp only [valuesProjection, F, fillZrW] by_cases hvA : v ∈ Z.image SWIGNode.random · exfalso exact Finset.disjoint_left.mp hDisj_ZrW hvA hv · rw [valuesUnionMk_apply_right _ _ _ hvA] rw [this] exact hwA · simp only [Set.mem_preimage, Set.mem_singleton_iff] funext ⟨v, hv⟩ simp only [valuesProjection, fillZrW] rw [valuesUnionMk_apply_left _ _ hv] · rintro ⟨hW_mem, hZr_mem⟩ simp only [Set.mem_preimage] at hW_mem simp only [Set.mem_preimage, Set.mem_singleton_iff] at hZr_mem refine ⟨valuesProjection (Finset.subset_union_right : W ⊆ _) c, hW_mem, ?_⟩ funext ⟨v, hv⟩ simp only [fillZrW] rcases Finset.mem_union.mp hv with hZrV | hWV · rw [valuesUnionMk_apply_left _ _ hZrV] have := congrFun hZr_mem ⟨v, hZrV⟩ simp only [valuesProjection] at this exact this.symm · by_cases hZrV' : v ∈ Z.image SWIGNode.random · rw [valuesUnionMk_apply_left _ _ hZrV'] have := congrFun hZr_mem ⟨v, hZrV'⟩ simp only [valuesProjection] at this exact this.symm · rw [valuesUnionMk_apply_right _ _ _ hZrV'] simp only [valuesProjection] -
fillZrW_injectivelemma — fillZrW Z _ _ W s' is injective when Z.image .random and W are disjoint.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhDisj_ZrW :Disjoint (Z.image SWIGNode.random) Ws' :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesconclusionInjective (M'.fillZrW Z hZ_obs hZ_fixed W s')Proof (Lean source)
lemma fillZrW_injective (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (W : Finset (SWIGNode N)) (hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W) (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) : Injective (M'.fillZrW Z hZ_obs hZ_fixed W s') := by classical intro w₁ w₂ h funext ⟨v, hv⟩ -- Project both sides of `h` to the W-coordinate v. have h_in : v ∈ Z.image SWIGNode.random ∪ W := Finset.subset_union_right hv have hvNotZr : v ∉ Z.image SWIGNode.random := fun hvZr => Finset.disjoint_left.mp hDisj_ZrW hvZr hv have hcoord := congrFun h ⟨v, h_in⟩ simp only [fillZrW] at hcoord rw [valuesUnionMk_apply_right _ _ h_in hvNotZr, valuesUnionMk_apply_right _ _ h_in hvNotZr] at hcoord exact hcoord -
measurableSet_fillZrW_imagelemma — A measurable W-event has a measurable image under fillZrW.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhDisj_ZrW :Disjoint (Z.image SWIGNode.random) Ws' :(M'.fixSet Z hZ_obs hZ_fixed).FixedValueshA :conclusionMeasurableSet ((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A)Proof (Lean source)
lemma measurableSet_fillZrW_image (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (W : Finset (SWIGNode N)) (hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W) [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) {A : Set (ValuesOn W (swigΩ Ω))} (hA : MeasurableSet A) : MeasurableSet ((M'.fillZrW Z hZ_obs hZ_fixed W s') '' A) := by classical let ζ_s : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) := zFixedAsRandom (valuesProjection (fixSet_image_fixed_subset M' Z hZ_obs hZ_fixed) s') by_cases hW : Nonempty (ValuesOn W (swigΩ Ω)) · obtain ⟨w₀⟩ := hW -- The Zr-singleton `{ζ_s}` is measurable (pulled back from the -- measurable singleton in `ValuesOn (Zr ∪ W)`). have hSingZr : MeasurableSet ({ζ_s} : Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))) := by have hmeas : Measurable (fun ζ : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) => valuesUnionMk ζ w₀) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ by_cases hvZ : v ∈ Z.image SWIGNode.random · have h_eq : (fun ζ : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) => valuesUnionMk ζ w₀ ⟨v, hv⟩) = (fun ζ => ζ ⟨v, hvZ⟩) := funext fun _ => valuesUnionMk_apply_left _ _ hvZ rw [h_eq] exact measurable_pi_apply _ · have hvW : v ∈ W := (Finset.mem_union.mp hv).resolve_left hvZ have h_eq : (fun ζ : ValuesOn (Z.image SWIGNode.random) (swigΩ Ω) => valuesUnionMk ζ w₀ ⟨v, hv⟩) = (fun _ => w₀ ⟨v, hvW⟩) := funext fun _ => valuesUnionMk_apply_right _ _ hv hvZ rw [h_eq] exact measurable_const have h_pre : ({ζ_s} : Set (ValuesOn (Z.image SWIGNode.random) (swigΩ Ω))) = (fun ζ => valuesUnionMk ζ w₀)⁻¹' ({valuesUnionMk ζ_s w₀} : Set (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))) := by ext ζ simp only [Set.mem_singleton_iff, Set.mem_preimage] refine ⟨fun h => by rw [h], fun h => ?_⟩ funext ⟨v, hv⟩ have hv_union : v ∈ Z.image SWIGNode.random ∪ W := subset_union_left hv have h_coord := congrFun h ⟨v, hv_union⟩ rw [valuesUnionMk_apply_left _ _ hv, valuesUnionMk_apply_left _ _ hv] at h_coord exact h_coord rw [h_pre] exact hmeas (measurableSet_singleton _) rw [fillZrW_image_eq M' Z hZ_obs hZ_fixed W hDisj_ZrW s' A] refine MeasurableSet.inter ?_ ?_ · exact (measurable_valuesProjection _) hA · exact (measurable_valuesProjection _) hSingZr · -- `ValuesOn W` empty: A = ∅, so F '' A = ∅. have hA_empty : A = ∅ := by ext w exact ⟨fun _ => (hW ⟨w⟩).elim, fun h => h.elim⟩ rw [hA_empty, Set.image_empty] exact MeasurableSet.empty -
measurableEmbedding_fillZrWlemma — fillZrW Z _ _ W s' is a MeasurableEmbedding when Z.image .random and W are disjoint.hypothesesN :sharedType u_1N → Type u_2M' :SCM N ΩZ :Finset NhZ_obs :∀ D ∈ Z, SWIGNode.random D ∈ M'.observedhZ_fixed :∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixedhDisj_ZrW :Disjoint (Z.image SWIGNode.random) Ws' :(M'.fixSet Z hZ_obs hZ_fixed).FixedValuesconclusionMeasurableEmbedding (M'.fillZrW Z hZ_obs hZ_fixed W s')Proof (Lean source)
lemma measurableEmbedding_fillZrW (M' : SCM N Ω) (Z : Finset N) (hZ_obs : ∀ D ∈ Z, SWIGNode.random D ∈ M'.observed) (hZ_fixed : ∀ D ∈ Z, SWIGNode.fixed D ∉ M'.fixed) (W : Finset (SWIGNode N)) (hDisj_ZrW : Disjoint (Z.image SWIGNode.random) W) [MeasurableSingletonClass (ValuesOn (Z.image SWIGNode.random ∪ W) (swigΩ Ω))] (s' : (M'.fixSet Z hZ_obs hZ_fixed).FixedValues) : MeasurableEmbedding (M'.fillZrW Z hZ_obs hZ_fixed W s') := { injective := fillZrW_injective M' Z hZ_obs hZ_fixed W hDisj_ZrW s' measurable := measurable_fillZrW M' Z hZ_obs hZ_fixed W s' measurableSet_image' := fun _ hA => measurableSet_fillZrW_image M' Z hZ_obs hZ_fixed W hDisj_ZrW s' hA }