SCM.Model

theorem observed_parent_index_lt (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) {p : SWIGNode N} (hparent : M.dag.edge p (M.observedAt ⟨n, hn⟩).val) (hobs : p ∈ M.observed) : M.observedIndex ⟨p, hobs⟩ < ⟨n, hn⟩ := by classical letI := M.topoLinearOrder have hp_lt : (⟨p, hobs⟩ : {v // v ∈ M.observed}) < M.observedAt ⟨n, hn⟩ := by change p < (M.observedAt ⟨n, hn⟩).val exact M.dag.topoOrder_lt p _ hparent have hidx : (M.observed.orderIsoOfFin rfl).symm ⟨p, hobs⟩ < (M.observed.orderIsoOfFin rfl).symm (M.observedAt ⟨n, hn⟩) := (M.observed.orderIsoOfFin rfl).symm.strictMono hp_lt simpa [SCM.observedIndex, SCM.observedAt] using hidx

lemma Equiv.trans {M₁ M₂ M₃ : SCM N Ω} (h₁ : Equiv M₁ M₂) (h₂ : Equiv M₂ M₃) : Equiv M₁ M₃ := by rcases h₁ with ⟨hG₁, hE₁, hF₁, hL₁⟩ rcases h₂ with ⟨hG₂, hE₂, hF₂, hL₂⟩ refine intro (trans hG₁ hG₂) ?_ refine intro ?_ ?_ · intro u v hu have hM₂_edge : M₂.dag.edge u v := (hG₁.1 u v).1 hu exact (hE₁ u v hu).trans (hE₂ u v hM₂_edge) · exact intro (hF₁.trans hF₂) (hL₁.trans hL₂)

theorem ancestralFactorization (M : SCM N Ω) (T : Finset (SWIGNode N)) {s s' : FixedValues M} {ℓ ℓ' : LatentValues M} (hs : ∀ (d : SWIGNode N) (hd : d ∈ M.fixed), (∃ v ∈ T, d = v ∨ M.dag.isAncestor d v) → s ⟨d, hd⟩ = s' ⟨d, hd⟩) (hℓ : ∀ (u : SWIGNode N) (hu : u ∈ M.unobserved), (∃ v ∈ T, u = v ∨ M.dag.isAncestor u v) → ℓ ⟨u, hu⟩ = ℓ' ⟨u, hu⟩) {v : SWIGNode N} (hv : v ∈ T) (hv_obs : v ∈ M.observed) : M.evalMap s ℓ ⟨v, mem_union_left _ hv_obs⟩ = M.evalMap s' ℓ' ⟨v, mem_union_left _ hv_obs⟩ := by rw [evalMap_observed M s ℓ ⟨v, mem_union_left _ hv_obs⟩ hv_obs, evalMap_observed M s' ℓ' ⟨v, mem_union_left _ hv_obs⟩ hv_obs] congr 1 apply evalObservedAux_agree_anc M T hs hℓ refine ⟨v, hv, inl ?_⟩ exact M.observedAt_observedIndex ⟨v, hv_obs⟩

lemma jointKernel_apply_eq (M : SCM N Ω) (s : FixedValues M) : M.jointKernel s = M.latentProduct.map (fun ℓ => M.evalMap s ℓ) := by have hf : Measurable (fun ℓ : LatentValues M => M.evalMap s ℓ) := by have : M.evalMap s = fun ℓ => uncurry M.evalMap (s, ℓ) := rfl rw [this] exact M.evalMap_measurable.comp (prodMk measurable_const measurable_id) refine MeasureTheory.Measure.ext fun A hA => ?_ unfold jointKernel rw [ProbabilityTheory.Kernel.map_apply _ measurable_snd, MeasureTheory.Measure.map_apply measurable_snd hA, ProbabilityTheory.Kernel.compProd_apply (measurable_snd hA), ProbabilityTheory.Kernel.const_apply, MeasureTheory.Measure.map_apply hf hA] -- LHS: ∫⁻ ℓ, (deterministic (uncurry evalMap)) (s, ℓ) -- (Prod.mk ℓ ⁻¹' (snd ⁻¹' A)) ∂latentProduct -- RHS: latentProduct ((fun ℓ => evalMap s ℓ) ⁻¹' A) simp only [ProbabilityTheory.Kernel.deterministic_apply, Function.uncurry_apply_pair] -- Simplify the preimage `Prod.mk ℓ ⁻¹' (snd ⁻¹' A) = A` (rfl on Set membership). have hset : ∀ ℓ : LatentValues M, (Prod.mk ℓ ⁻¹' (snd ⁻¹' A) : Set (RandomValues M)) = A := fun _ => rfl simp only [hset] -- Goal: ∫⁻ ℓ, Measure.dirac (M.evalMap s ℓ) A ∂latentProduct -- = latentProduct ((fun ℓ => evalMap s ℓ) ⁻¹' A) -- Bridge through indicator form. trans (∫⁻ ℓ, indicator ((fun ℓ => M.evalMap s ℓ) ⁻¹' A) (fun _ => (1 : ENNReal)) ℓ ∂M.latentProduct) · apply MeasureTheory.lintegral_congr intro ℓ rw [MeasureTheory.Measure.dirac_apply' _ hA] simp only [indicator, Set.mem_preimage, Pi.one_apply] rfl · exact MeasureTheory.lintegral_indicator_one (hf hA)

theorem obsCondKernel_ae_eq_condDistrib (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 (FixedValues M) (ValuesOn CC (swigΩ Ω))] (s : M.FixedValues) : (fun c => M.obsCondKernel Y CC hY hCC (s, c)) =ᵐ[(M.obsKernel s).map (valuesProjection hCC)] condDistrib (valuesProjection hY) (valuesProjection hCC) (M.obsKernel s) := by letI : IsMarkovKernel (M.obsCondPairKernel Y CC hY hCC) := by unfold obsCondPairKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (prodMk (measurable_valuesProjection hCC) (measurable_valuesProjection hY)) -- `Kernel.condKernel_apply_eq_condKernel` gives a.e. equality with the -- measure-level `condKernel`; rewrite `Kernel.fst` of the pair kernel. have h := ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel (M.obsCondPairKernel Y CC hY hCC) s -- `Kernel.fst (M.obsKernel.map (π_CC, π_Y)) s = (M.obsKernel s).map π_CC`. have hfst : ProbabilityTheory.Kernel.fst (M.obsCondPairKernel Y CC hY hCC) s = (M.obsKernel s).map (valuesProjection hCC) := by unfold obsCondPairKernel rw [ProbabilityTheory.Kernel.fst_map_prod _ (measurable_valuesProjection hY), ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection hCC)] rw [hfst] at h -- `condDistrib π_Y π_CC μ = (μ.map (π_CC, π_Y)).condKernel = (obsCondPairKernel s).condKernel`. have hmap : (M.obsCondPairKernel Y CC hY hCC) s = map (fun ω => (valuesProjection hCC ω, valuesProjection hY ω)) (M.obsKernel s) := by unfold obsCondPairKernel exact ProbabilityTheory.Kernel.map_apply M.obsKernel ((measurable_valuesProjection hCC).prodMk (measurable_valuesProjection hY)) s have hcd : condDistrib (valuesProjection hY) (valuesProjection hCC) (M.obsKernel s) = (M.obsCondPairKernel Y CC hY hCC s).condKernel := by rw [condDistrib] congr 1 exact hmap.symm rw [hcd] exact h

theorem fixSet_empty_equiv (M : SCM N Ω) : SCM.Equiv (M.fixSet ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))) M := by let hObs : ∀ D ∈ (∅ : Finset N), SWIGNode.random D ∈ M.observed := fun _ hD => absurd hD (notMem_empty _) let hFix : ∀ D ∈ (∅ : Finset N), SWIGNode.fixed D ∉ M.fixed := fun _ hD => absurd hD (notMem_empty _) -- (1) Graph-level equivalence (reused for the parent-set transport below). have hGraph : SWIGGraph.Equivalent (M.fixSet ∅ (fun _ hD => absurd hD (notMem_empty _)) (fun _ hD => absurd hD (notMem_empty _))).toSWIGGraph M.toSWIGGraph := by refine ⟨?_, ?_, rfl, rfl⟩ · simpa [SCM.fixSet, SCM.fixMono] using fixSet_empty_edge M.toSWIGGraph · simp refine ⟨hGraph, ?_, ?_, ?_⟩ · -- (2) Edge-type agreement: the `∃ D ∈ ∅, u = .fixed D` guard is vacuous. intro u v _ change (if h : ∃ D ∈ (∅ : Finset N), u = SWIGNode.fixed D then M.edgeTypes.edgeType (SWIGNode.random (choose h)) v else M.edgeTypes.edgeType u v) = M.edgeTypes.edgeType u v rw [dif_neg] rintro ⟨D, hD, _⟩ exact absurd hD (notMem_empty _) · -- (3) HEq structFun, by the standard parent-tuple HEq recipe: -- outer `hfunext` over `{v // v ∈ observed}` (defeq on both sides), -- inner `hfunext` over parent tuples (domains propositionally equal via -- `hGraph.parents_eq`), then reduce `HEq` to `Eq` and show the -- `fixMonoParentMap ∅` reindex is the pointwise identity. refine Function.hfunext rfl ?_ rintro v _ hv have hv_eq : v = _ := eq_of_heq hv subst hv_eq refine Function.hfunext ?_ ?_ · rw [SWIGGraph.Equivalent.parents_eq hGraph.1 v.val] · rintro ξ₁ ξ₂ hξ apply heq_of_eq have hP : (M.fixSet ∅ hObs hFix).toSWIGGraph.dag.parents v.val = M.toSWIGGraph.dag.parents v.val := SWIGGraph.Equivalent.parents_eq hGraph.1 v.val -- Pointwise equality of ξ₁ and ξ₂ at matching coordinates, obtained by -- reverting both and rewriting `hP` so they end up with the same type. have hξ_apply : ∀ (x : SWIGNode N) (h₁ : x ∈ (M.fixSet ∅ hObs hFix).toSWIGGraph.dag.parents v.val) (h₂ : x ∈ M.toSWIGGraph.dag.parents v.val), ξ₁ ⟨x, h₁⟩ = ξ₂ ⟨x, h₂⟩ := by revert ξ₁ ξ₂ hξ rw [hP] rintro ξ₁ ξ₂ hξ x h₁ h₂ have hξ_eq : ξ₁ = ξ₂ := eq_of_heq hξ subst hξ_eq rfl have h_obs_M : v.val ∈ M.observed := v.property -- Unfold `(M.fixSet ∅).structFun v ξ₁` via its `fixMono` definition. change M.structFun ⟨v.val, h_obs_M⟩ (fixMonoParentMap M.toSWIGGraph ∅ hObs hFix v.val ξ₁) = M.structFun v ξ₂ -- Peel `M.structFun ⟨v.val, _⟩`; reduce to tuple-level equality. congr 1 funext ⟨w, hw⟩ cases w with | random u => -- `u ∈ ∅` is vacuous, so `fixMonoParentMap` reads `ξ₁` at `.random u`. have hu : u ∉ (∅ : Finset N) := notMem_empty _ rw [fixMonoParentMap_apply_random_notMem M.toSWIGGraph ∅ hObs hFix v.val ξ₁ u hu hw] exact hξ_apply (SWIGNode.random u) _ hw | fixed d => -- `fixMonoParentMap` on a `.fixed` coordinate is `rfl`-identity. rw [fixMonoParentMap_apply_fixed M.toSWIGGraph ∅ hObs hFix v.val ξ₁ d hw] exact hξ_apply (SWIGNode.fixed d) _ hw · -- (4) HEq latentDist: inherited verbatim by `fixMono`. rfl

theorem fixSet_equiv_congr {M₁ M₂ : SCM N Ω} (h : SCM.Equiv M₁ M₂) (X : Finset N) (hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed) (hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed) : let hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed := by intro D hD rw [← h.1.2.2.1] exact hObs₁ D hD let hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed := by intro D hD hDfix apply hFix₁ D hD rw [h.1.2.1] exact hDfix SCM.Equiv (M₁.fixSet X hObs₁ hFix₁) (M₂.fixSet X hObs₂ hFix₂) := by obtain ⟨hGraph, hEdgeType, hSF, hLat⟩ := h have hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed := by intro D hD rw [← hGraph.2.2.1] exact hObs₁ D hD have hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed := by intro D hD hDfix apply hFix₁ D hD rw [hGraph.2.1] exact hDfix change SCM.Equiv (M₁.fixSet X hObs₁ hFix₁) (M₂.fixSet X hObs₂ hFix₂) -- (1) Graph-level equivalence via `splitMono_congr`. have hGraph' : SWIGGraph.Equivalent (M₁.fixSet X hObs₁ hFix₁).toSWIGGraph (M₂.fixSet X hObs₂ hFix₂).toSWIGGraph := hGraph.splitMono_congr X hObs₁ hFix₁ hObs₂ hFix₂ refine ⟨hGraph', ?_, ?_, ?_⟩ · -- (2) Edge-type agreement. -- The `edgeType` of `fixSet` uses a `dite` on `∃ D ∈ X, u = .fixed D`. intro u v hu -- Both sides expand to the same dite structure; split on the guard. change (if hh : ∃ D ∈ X, u = SWIGNode.fixed D then M₁.edgeTypes.edgeType (SWIGNode.random (choose hh)) v else M₁.edgeTypes.edgeType u v) = (if hh : ∃ D ∈ X, u = SWIGNode.fixed D then M₂.edgeTypes.edgeType (SWIGNode.random (choose hh)) v else M₂.edgeTypes.edgeType u v) split_ifs with hh · -- u = .fixed D branch: underlying edge is M.dag.edge (.random D) v. -- Retrieve the underlying M₁ and M₂ edges from splitMonoEdgeRel. have hD := Classical.choose_spec hh -- hu : (M₁.fixSet X).dag.edge u v, which is splitMonoEdgeRel M₁.dag.edge X u v. -- With u = .fixed D and D ∈ X, this simplifies to M₁.dag.edge (.random D) v. have hu₁ : M₁.dag.edge (SWIGNode.random (choose hh)) v := by have huEq : u = SWIGNode.fixed (choose hh) := hD.2 rw [huEq] at hu simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel, if_pos hD.1] at hu exact hu exact hEdgeType _ _ hu₁ · -- else branch: direct M.dag.edge u v. have hu₁ : M₁.dag.edge u v := by simp only [SCM.fixSet, SCM.fixMono, SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel] at hu cases u with | random r => by_cases hr : r ∈ X · simp [hr] at hu · simpa [hr] using hu | fixed d => by_cases hd : d ∈ X · exfalso; apply hh; exact ⟨d, hd, rfl⟩ · simpa [hd] using hu exact hEdgeType _ _ hu₁ · -- (3) HEq structFun. -- Both `(M_i.fixSet X).structFun v' ξ` unfold to -- `M_i.structFun ⟨v'.val, _⟩ (fixMonoParentMap M_i.toSWIGGraph X _ _ v'.val ξ)`. -- Outer hfunext: observed domain. -- `(M_i.fixSet X).observed = M_i.observed` by rfl, and `M₁.observed = M₂.observed` by hGraph. have hObsSplit : (M₁.fixSet X hObs₁ hFix₁).observed = (M₂.fixSet X hObs₂ hFix₂).observed := hGraph'.2.2.1 refine Function.hfunext (by rw [hObsSplit]) ?_ rintro v₁ v₂ hv have hv_eq : v₁.val = v₂.val := by exact (Subtype.heq_iff_coe_eq (by intro x; rw [hObsSplit])).mp hv -- Inner hfunext: parent-tuple domain. -- Observed sets equal, so split parent sets are equal. have hPar : (M₁.fixSet X hObs₁ hFix₁).dag.parents v₁.val = (M₂.fixSet X hObs₂ hFix₂).dag.parents v₂.val := by rw [hv_eq]; exact SWIGGraph.Equivalent.parents_eq hGraph'.1 v₂.val refine Function.hfunext ?_ ?_ · rw [hPar] · rintro ξ₁ ξ₂ hξ -- Goal: (M₁.fixSet X).structFun v₁ ξ₁ ≍ (M₂.fixSet X).structFun v₂ ξ₂ -- Both sides unfold to M_i.structFun ⟨v_i.val, _⟩ (fixMonoParentMap ...). have hObsEq : M₁.observed = M₂.observed := hGraph.2.2.1 have hv_obs₁ : v₁.val ∈ M₁.observed := v₁.property have hv_obs₂' : v₂.val ∈ M₂.observed := v₂.property -- Parent sets. have hPar₀ : M₁.dag.parents v₁.val = M₂.dag.parents v₂.val := by rw [SWIGGraph.Equivalent.parents_eq hGraph.1 v₁.val, hv_eq] -- Split parent set equality (via hGraph' and hv_eq). have hSplitPar : (M₁.fixSet X hObs₁ hFix₁).dag.parents v₁.val = (M₂.fixSet X hObs₂ hFix₂).dag.parents v₂.val := by rw [SWIGGraph.Equivalent.parents_eq hGraph'.1 v₁.val, hv_eq] -- hξ_apply: pointwise equality from hξ : ξ₁ ≍ ξ₂ over propEq domain types. -- Use dcongr_heq since ξ₁, ξ₂ are dependent pi types. have hξ_apply : ∀ (x : SWIGNode N) (h₁ : x ∈ (M₁.fixSet X hObs₁ hFix₁).dag.parents v₁.val) (h₂ : x ∈ (M₂.fixSet X hObs₂ hFix₂).dag.parents v₂.val), ξ₁ ⟨x, h₁⟩ = ξ₂ ⟨x, h₂⟩ := by intro x h₁ h₂ apply eq_of_heq apply dcongr_heq · -- ⟨x, h₁⟩ ≍ ⟨x, h₂⟩ exact (Subtype.heq_iff_coe_eq (by intro a; rw [hSplitPar])).mpr rfl · -- type: swigΩ Ω t₁.val = swigΩ Ω t₂.val given t₁ ≍ t₂ intro t₁ t₂ ht have : t₁.val = t₂.val := (Subtype.heq_iff_coe_eq (by intro a; rw [hSplitPar])).mp ht simp [this] · -- function HEq intro _ _; exact hξ -- Step 1: HEq of the structFun applications at v₁ vs v₂. have hvHeq : (⟨v₁.val, hv_obs₁⟩ : {v // v ∈ M₁.observed}) ≍ (⟨v₂.val, hv_obs₂'⟩ : {v // v ∈ M₂.observed}) := by apply (Subtype.heq_iff_coe_eq (by intro x; rw [hObsEq])).mpr exact hv_eq have hApp : HEq (M₁.structFun ⟨v₁.val, hv_obs₁⟩) (M₂.structFun ⟨v₂.val, hv_obs₂'⟩) := by apply dcongr_heq hvHeq · intro t₁ t₂ ht have hval : t₁.val = t₂.val := (Subtype.heq_iff_coe_eq (by intro x; rw [hObsEq])).mp ht rw [hval, SWIGGraph.Equivalent.parents_eq hGraph.1 t₂.val] · intro _ _; exact hSF -- Step 2: HEq of the fixMonoParentMap outputs. -- Subtype domain equality for fixMonoParentMap. have hPar₀_sub : ({w // w ∈ M₁.dag.parents v₁.val} : Type _) = {w // w ∈ M₂.dag.parents v₂.val} := congrArg (fun s : Finset (SWIGNode N) => {w : SWIGNode N // w ∈ s}) hPar₀ have hξHeq : HEq (fixMonoParentMap M₁.toSWIGGraph X hObs₁ hFix₁ v₁.val ξ₁) (fixMonoParentMap M₂.toSWIGGraph X hObs₂ hFix₂ v₂.val ξ₂) := by apply Function.hfunext hPar₀_sub rintro ⟨w₁val, w₁prop⟩ ⟨w₂val, w₂prop⟩ hw have hwval : w₁val = w₂val := (Subtype.heq_iff_coe_eq (by intro x; rw [hPar₀])).mp hw subst hwval apply heq_of_eq cases w₁val with | random u => by_cases hu : u ∈ X · rw [fixMonoParentMap_apply_random M₁.toSWIGGraph X hObs₁ hFix₁ v₁.val u hu ξ₁ w₁prop, fixMonoParentMap_apply_random M₂.toSWIGGraph X hObs₂ hFix₂ v₂.val u hu ξ₂ w₂prop] exact hξ_apply (SWIGNode.fixed u) _ _ · rw [fixMonoParentMap_apply_random_notMem M₁.toSWIGGraph X hObs₁ hFix₁ v₁.val ξ₁ u hu w₁prop, fixMonoParentMap_apply_random_notMem M₂.toSWIGGraph X hObs₂ hFix₂ v₂.val ξ₂ u hu w₂prop] exact hξ_apply (SWIGNode.random u) _ _ | fixed d => rw [fixMonoParentMap_apply_fixed M₁.toSWIGGraph X hObs₁ hFix₁ v₁.val ξ₁ d w₁prop, fixMonoParentMap_apply_fixed M₂.toSWIGGraph X hObs₂ hFix₂ v₂.val ξ₂ d w₂prop] exact hξ_apply (SWIGNode.fixed d) _ _ -- Combine: goal unfolds definitionally to M_i.structFun at v_i applied to fixMonoParentMap. -- Use dcongr_heq: hξHeq as the argument HEq, hApp as the function HEq. -- Codomain: swigΩ Ω v₁.val = swigΩ Ω v₂.val follows from hv_eq. change HEq (M₁.structFun ⟨v₁.val, hv_obs₁⟩ (fixMonoParentMap M₁.toSWIGGraph X hObs₁ hFix₁ v₁.val ξ₁)) (M₂.structFun ⟨v₂.val, hv_obs₂'⟩ (fixMonoParentMap M₂.toSWIGGraph X hObs₂ hFix₂ v₂.val ξ₂)) exact dcongr_heq hξHeq (fun _ _ _ => by rw [hv_eq]) (fun _ _ => hApp) · -- (4) HEq latentDist: fixMono inherits latentDist by rfl; unobserved sets equal. -- Both `(M_i.fixSet X).latentDist = M_i.latentDist` by rfl (same unobserved Finset). -- `hLat : HEq M₁.latentDist M₂.latentDist`. exact hLat

theorem evalMap_overrideC_at_self (M : SCM N Ω) {Y C : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC : C ⊆ M.observed) (s : M.FixedValues) (ℓ : M.LatentValues) : M.evalMap_overrideC hY hC s (fun v' : {v // v ∈ C} => (M.observedAt_observedIndex ⟨v'.val, hC v'.property⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨v'.val, hC v'.property⟩).val (M.observedIndex ⟨v'.val, hC v'.property⟩).isLt) ℓ = fun v : {v // v ∈ Y} => (M.observedAt_observedIndex ⟨v.val, hY v.property⟩) ▸ evalObservedAux M s ℓ (M.observedIndex ⟨v.val, hY v.property⟩).val (M.observedIndex ⟨v.val, hY v.property⟩).isLt := by funext v rw [evalMap_overrideC_eq] congr 1 exact evalObservedAuxOverride_eq_evalObservedAux_at_self M hC s ℓ _ _

@[simp] lemma fixMono_latentDist (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (u : {u // u ∈ (M.fixMono X hObs hFix).unobserved}) : (M.fixMono X hObs hFix).latentDist u = M.latentDist u := rfl

theorem evalMap_fixSet_factual_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (s : SCM.FixedValues M) (ℓ : SCM.LatentValues M) (sx : SCM.FixedValues (M.fixSet X hObs hFix)) -- sx agrees with s on the original fixed coordinates (hOld : ∀ (v : SWIGNode N) (hv : v ∈ M.fixed), sx ⟨v, Finset.mem_union_left _ hv⟩ = s ⟨v, hv⟩) -- factual condition: base evaluation at .random D equals sx's new fixed value (hNew : ∀ D (hD : D ∈ X), M.evalMap s ℓ ⟨SWIGNode.random D, Finset.mem_union_left _ (hObs D hD)⟩ = sx ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) (v : {v // v ∈ M.observed}) : (M.fixSet X hObs hFix).evalMap sx ℓ ⟨v.val, Finset.mem_union_left _ v.property⟩ = M.evalMap s ℓ ⟨v.val, Finset.mem_union_left _ v.property⟩ := by classical -- Observed/unobserved/fixed-of-M coincide on (M.fixSet X); only X.image .fixed is extra. -- Strengthened claim: agreement at EVERY observed node, by strong induction on M's topo index. suffices hstr : ∀ (n : ℕ) (hn : n < M.observed.card), (M.fixSet X hObs hFix).evalMap sx ℓ ⟨(M.observedAt ⟨n, hn⟩).val, Finset.mem_union_left _ ((M.observedAt ⟨n, hn⟩).property)⟩ = M.evalMap s ℓ ⟨(M.observedAt ⟨n, hn⟩).val, Finset.mem_union_left _ ((M.observedAt ⟨n, hn⟩).property)⟩ by have hkey := hstr (M.observedIndex ⟨v.val, v.property⟩).val (M.observedIndex ⟨v.val, v.property⟩).isLt have hat : (M.observedAt (M.observedIndex ⟨v.val, v.property⟩)).val = v.val := M.observedAt_observedIndex ⟨v.val, v.property⟩ -- rewrite node back to v.val using subtype-value equality on both evalMap args have hsub : (⟨(M.observedAt (M.observedIndex ⟨v.val, v.property⟩)).val, Finset.mem_union_left M.unobserved (M.observedAt (M.observedIndex ⟨v.val, v.property⟩)).property⟩ : {w // w ∈ M.randomVars}) = ⟨v.val, Finset.mem_union_left _ v.property⟩ := Subtype.ext hat exact hsub ▸ hkey intro n induction n using Nat.strongRecOn with | _ n ih => intro hn -- The target observed node, viewed in M and in M.fixSet X (same observed set, by rfl). set w₀ : {v // v ∈ M.observed} := M.observedAt ⟨n, hn⟩ with hw₀ have hw₀' : w₀.val ∈ (M.fixSet X hObs hFix).observed := w₀.property -- Unfold both evalMap calls one structFun step. rw [evalMap_observed_unfold M s ℓ w₀, evalMap_observed_unfold (M.fixSet X hObs hFix) sx ℓ ⟨w₀.val, hw₀'⟩] -- The fixSet structFun is M.structFun reindexed via fixMonoParentMap (definitional). refine trans (b := M.structFun w₀ (fixMonoParentMap M.toSWIGGraph X hObs hFix w₀.val (fun w => if huo : (w : {w // w ∈ (M.fixSet X hObs hFix).dag.parents w₀.val}).val ∈ (M.fixSet X hObs hFix).unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ (M.fixSet X hObs hFix).fixed then sx ⟨w.val, hfix⟩ else (M.fixSet X hObs hFix).evalMap sx ℓ ⟨w.val, by rcases Finset.mem_union.mp (((M.fixSet X hObs hFix).dag_edges_classified _ _ ((M.fixSet X hObs hFix).dag.mem_parents.mp w.property)).1) with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact Finset.mem_union_left _ hob · exact absurd h2 huo⟩))) rfl ?_ -- Now: M.structFun w₀ (fixMonoParentMap ... ξdo) = M.structFun w₀ ξbase. -- Peel structFun, prove the parent tuples agree pointwise on M-parents. congr 1 funext w -- `w` is an M-parent of `w₀.val`; classify it. have hedgeM : M.dag.edge w.val w₀.val := M.dag.mem_parents.mp w.property obtain ⟨wVal, hwMem⟩ := w simp only at * cases wVal with | fixed d => -- `.fixed d` is an M-parent ⇒ it must be in `M.fixed` (else isolated). have hdfix : SWIGNode.fixed d ∈ M.fixed := by by_contra hdf have hiso := M.fixed_outside_fixed_isolated d hdf have : w₀.val ∈ M.dag.children (SWIGNode.fixed d) := M.dag.mem_children.mpr hedgeM rw [hiso.2] at this exact (notMem_empty _) this have hdfix' : SWIGNode.fixed d ∈ (M.fixSet X hObs hFix).fixed := Finset.mem_union_left _ hdfix have hdnuo : SWIGNode.fixed d ∉ M.unobserved := by intro h obtain ⟨m, hm⟩ := M.unobserved_is_random _ h exact absurd hm (by simp) rw [fixMonoParentMap_apply_fixed M.toSWIGGraph X hObs hFix w₀.val _ d hwMem] simp only [Subtype.coe_mk] -- ξdo at `.fixed d` reads sx; ξbase reads s; equal by hOld. split_ifs with h1 <;> first | exact hOld (SWIGNode.fixed d) hdfix | exact absurd h1 hdnuo | random u => by_cases hu : u ∈ X · -- intervened node: fixMonoParentMap reads `.fixed u`; equal by hNew. -- `.random u ∈ M.observed`, hence neither fixed nor unobserved. have hru_obs : SWIGNode.random u ∈ M.observed := hObs u hu have hru_nuo : SWIGNode.random u ∉ M.unobserved := fun h => (Finset.disjoint_left.mp M.obs_unobs_disjoint hru_obs) h have hru_nfix : SWIGNode.random u ∉ M.fixed := by intro h; obtain ⟨m, hm⟩ := M.fixed_is_fixed _ h; exact absurd hm (by simp) -- `.fixed u ∈ (M.fixSet X).fixed`, not unobserved. have hfu : SWIGNode.fixed u ∈ (M.fixSet X hObs hFix).fixed := fixed_mem_fixSet M X hObs hFix hu have hfu_nuo : SWIGNode.fixed u ∉ (M.fixSet X hObs hFix).unobserved := by intro h obtain ⟨m, hm⟩ := (M.fixSet X hObs hFix).unobserved_is_random _ h exact absurd hm (by simp) rw [fixMonoParentMap_apply_random M.toSWIGGraph X hObs hFix w₀.val u hu _ hwMem] simp only [Subtype.coe_mk] rw [dif_neg hru_nuo, dif_neg hru_nfix] -- ξdo at `.fixed u`: not unobserved, is fixed ⇒ sx ⟨.fixed u⟩. rw [dif_neg hfu_nuo, dif_pos hfu] exact (hNew u hu).symm · -- non-intervened random parent: same classification on both sides. have hru_nfix : SWIGNode.random u ∉ M.fixed := by intro h; obtain ⟨m, hm⟩ := M.fixed_is_fixed _ h; exact absurd hm (by simp) have hru_ndfix : SWIGNode.random u ∉ (M.fixSet X hObs hFix).fixed := by intro h obtain ⟨m, hm⟩ := (M.fixSet X hObs hFix).fixed_is_fixed _ h exact absurd hm (by simp) rw [fixMonoParentMap_apply_random_notMem M.toSWIGGraph X hObs hFix w₀.val _ u hu hwMem] simp only [Subtype.coe_mk] -- Same three-way classification on both sides; resolve simultaneously. split_ifs with hd hm hm · rfl -- both unobserved ⇒ ℓ · exact absurd hd hm -- fixSet-unobs but base-not-unobs (defeq contra) · exact absurd hm hd -- base-unobs but fixSet-not-unobs (defeq contra) · -- both observed: recurse via IH at strictly smaller M-index. have hru_obs : SWIGNode.random u ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedgeM).1 with hc1 | hc2 · rcases Finset.mem_union.mp hc1 with hfx | hob · exact absurd hfx hru_nfix · exact hob · exact absurd hc2 hm set j := M.observedIndex ⟨SWIGNode.random u, hru_obs⟩ with hj have hlt : j.val < n := M.observed_parent_index_lt hn hedgeM hru_obs have hihm := ih j.val hlt j.isLt -- `⟨j.val, j.isLt⟩ = j` by Fin eta (definitional); node value back to `.random u`. have hat : (M.observedAt ⟨j.val, j.isLt⟩).val = SWIGNode.random u := M.observedAt_observedIndex ⟨SWIGNode.random u, hru_obs⟩ have hsub : (⟨(M.observedAt ⟨j.val, j.isLt⟩).val, Finset.mem_union_left M.unobserved (M.observedAt ⟨j.val, j.isLt⟩).property⟩ : {w // w ∈ M.randomVars}) = ⟨SWIGNode.random u, Finset.mem_union_left _ hru_obs⟩ := Subtype.ext hat -- Transport `hihm` along the node-value equality via an explicit motive. refine Eq.ndrec (motive := fun w : {w // w ∈ M.randomVars} => (M.fixSet X hObs hFix).evalMap sx ℓ w = M.evalMap s ℓ w) hihm hsub

theorem evalMap_fixSet_union_eq (M : SCM N Ω) (X₁ X₂ : Finset N) (hObs₁ : ∀ D ∈ X₁, SWIGNode.random D ∈ M.observed) (hFix₁ : ∀ D ∈ X₁, SWIGNode.fixed D ∉ M.fixed) (hObsU : ∀ D ∈ X₁ ∪ X₂, SWIGNode.random D ∈ M.observed) (hFixU : ∀ D ∈ X₁ ∪ X₂, SWIGNode.fixed D ∉ M.fixed) (ℓ : SCM.LatentValues M) (sx₁ : SCM.FixedValues (M.fixSet X₁ hObs₁ hFix₁)) (sxU : SCM.FixedValues (M.fixSet (X₁ ∪ X₂) hObsU hFixU)) -- compatibility: sxU agrees with sx₁ on M.fixed ∪ X₁.image .fixed coords (hCompat_old : ∀ (v : SWIGNode N) (hv : v ∈ M.fixed), sxU ⟨v, Finset.mem_union_left _ hv⟩ = sx₁ ⟨v, Finset.mem_union_left _ hv⟩) (hCompat_x₁ : ∀ D (hD : D ∈ X₁), sxU ⟨SWIGNode.fixed D, Finset.mem_union_right _ (Finset.mem_image.mpr ⟨D, Finset.mem_union_left _ hD, rfl⟩)⟩ = sx₁ ⟨SWIGNode.fixed D, Finset.mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) -- intermediate condition: post-X₁ value of .random D equals sxU's X₂ fixed value (hIntermediate : ∀ D (hD : D ∈ X₂), (M.fixSet X₁ hObs₁ hFix₁).evalMap sx₁ ℓ ⟨SWIGNode.random D, Finset.mem_union_left _ (hObsU D (Finset.mem_union_right _ hD))⟩ = sxU ⟨SWIGNode.fixed D, Finset.mem_union_right _ (Finset.mem_image.mpr ⟨D, Finset.mem_union_right _ hD, rfl⟩)⟩) (v : {v // v ∈ M.observed}) : (M.fixSet (X₁ ∪ X₂) hObsU hFixU).evalMap sxU ℓ ⟨v.val, Finset.mem_union_left _ v.property⟩ = (M.fixSet X₁ hObs₁ hFix₁).evalMap sx₁ ℓ ⟨v.val, Finset.mem_union_left _ v.property⟩ := by classical -- Mirror of `evalMap_fixSet_factual_eq`: strong induction on M's topo index, -- comparing `(M.fixSet (X₁∪X₂)).evalMap sxU` with `(M.fixSet X₁).evalMap sx₁` -- at every observed node. The per-parent case analysis collapses the X₂ -- step via `hIntermediate` and the X₁ step via `hCompat_x₁`. suffices hstr : ∀ (n : ℕ) (hn : n < M.observed.card), (M.fixSet (X₁ ∪ X₂) hObsU hFixU).evalMap sxU ℓ ⟨(M.observedAt ⟨n, hn⟩).val, Finset.mem_union_left _ ((M.observedAt ⟨n, hn⟩).property)⟩ = (M.fixSet X₁ hObs₁ hFix₁).evalMap sx₁ ℓ ⟨(M.observedAt ⟨n, hn⟩).val, Finset.mem_union_left _ ((M.observedAt ⟨n, hn⟩).property)⟩ by have hkey := hstr (M.observedIndex ⟨v.val, v.property⟩).val (M.observedIndex ⟨v.val, v.property⟩).isLt have hat : (M.observedAt (M.observedIndex ⟨v.val, v.property⟩)).val = v.val := M.observedAt_observedIndex ⟨v.val, v.property⟩ have hsub : (⟨(M.observedAt (M.observedIndex ⟨v.val, v.property⟩)).val, Finset.mem_union_left M.unobserved (M.observedAt (M.observedIndex ⟨v.val, v.property⟩)).property⟩ : {w // w ∈ M.randomVars}) = ⟨v.val, Finset.mem_union_left _ v.property⟩ := Subtype.ext hat exact hsub ▸ hkey intro n induction n using Nat.strongRecOn with | _ n ih => intro hn set w₀ : {v // v ∈ M.observed} := M.observedAt ⟨n, hn⟩ with hw₀ have hw₀U : w₀.val ∈ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).observed := w₀.property have hw₀₁ : w₀.val ∈ (M.fixSet X₁ hObs₁ hFix₁).observed := w₀.property -- Unfold both evalMap calls one structFun step. rw [evalMap_observed_unfold (M.fixSet X₁ hObs₁ hFix₁) sx₁ ℓ ⟨w₀.val, hw₀₁⟩, evalMap_observed_unfold (M.fixSet (X₁ ∪ X₂) hObsU hFixU) sxU ℓ ⟨w₀.val, hw₀U⟩] -- Both fixSet structFuns are `M.structFun w₀` reindexed via `fixMonoParentMap`. -- Reduce to: M.structFun w₀ (fixMonoParentMap … X₁∪X₂ ξU) -- = M.structFun w₀ (fixMonoParentMap … X₁ ξ₁). refine trans (b := M.structFun w₀ (fixMonoParentMap M.toSWIGGraph (X₁ ∪ X₂) hObsU hFixU w₀.val (fun w => if huo : (w : {w // w ∈ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).dag.parents w₀.val}).val ∈ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).fixed then sxU ⟨w.val, hfix⟩ else (M.fixSet (X₁ ∪ X₂) hObsU hFixU).evalMap sxU ℓ ⟨w.val, by rcases Finset.mem_union.mp (((M.fixSet (X₁ ∪ X₂) hObsU hFixU).dag_edges_classified _ _ ((M.fixSet (X₁ ∪ X₂) hObsU hFixU).dag.mem_parents.mp w.property)).1) with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact Finset.mem_union_left _ hob · exact absurd h2 huo⟩))) rfl ?_ -- Now compare the two parent dispatches directly. refine symm (trans (b := M.structFun w₀ (fixMonoParentMap M.toSWIGGraph X₁ hObs₁ hFix₁ w₀.val (fun w => if huo : (w : {w // w ∈ (M.fixSet X₁ hObs₁ hFix₁).dag.parents w₀.val}).val ∈ (M.fixSet X₁ hObs₁ hFix₁).unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ (M.fixSet X₁ hObs₁ hFix₁).fixed then sx₁ ⟨w.val, hfix⟩ else (M.fixSet X₁ hObs₁ hFix₁).evalMap sx₁ ℓ ⟨w.val, by rcases Finset.mem_union.mp (((M.fixSet X₁ hObs₁ hFix₁).dag_edges_classified _ _ ((M.fixSet X₁ hObs₁ hFix₁).dag.mem_parents.mp w.property)).1) with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact Finset.mem_union_left _ hob · exact absurd h2 huo⟩))) rfl ?_) -- Peel structFun; prove the parent tuples agree pointwise on M-parents. -- Goal (after symm): structFun(X₁ ξ₁) = structFun(X₁∪X₂ ξU). congr 1 funext w have hedgeM : M.dag.edge w.val w₀.val := M.dag.mem_parents.mp w.property obtain ⟨wVal, hwMem⟩ := w simp only at * cases wVal with | fixed d => -- `.fixed d` M-parent ⇒ in M.fixed; both sides read their resp. fixed value. have hdfix : SWIGNode.fixed d ∈ M.fixed := by by_contra hdf have hiso := M.fixed_outside_fixed_isolated d hdf have : w₀.val ∈ M.dag.children (SWIGNode.fixed d) := M.dag.mem_children.mpr hedgeM rw [hiso.2] at this exact (notMem_empty _) this have hdnuo : SWIGNode.fixed d ∉ M.unobserved := by intro h obtain ⟨m, hm⟩ := M.unobserved_is_random _ h exact absurd hm (by simp) have hd1uo : SWIGNode.fixed d ∉ (M.fixSet X₁ hObs₁ hFix₁).unobserved := hdnuo have hdUuo : SWIGNode.fixed d ∉ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).unobserved := hdnuo have hd1fix : SWIGNode.fixed d ∈ (M.fixSet X₁ hObs₁ hFix₁).fixed := Finset.mem_union_left _ hdfix have hdUfix : SWIGNode.fixed d ∈ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).fixed := Finset.mem_union_left _ hdfix rw [fixMonoParentMap_apply_fixed M.toSWIGGraph X₁ hObs₁ hFix₁ w₀.val _ d hwMem, fixMonoParentMap_apply_fixed M.toSWIGGraph (X₁ ∪ X₂) hObsU hFixU w₀.val _ d hwMem] simp only [Subtype.coe_mk] rw [dif_neg hd1uo, dif_pos hd1fix, dif_neg hdUuo, dif_pos hdUfix] exact (hCompat_old (SWIGNode.fixed d) hdfix).symm | random u => have hru_nfix : SWIGNode.random u ∉ M.fixed := by intro h; obtain ⟨m, hm⟩ := M.fixed_is_fixed _ h; exact absurd hm (by simp) by_cases hu1 : u ∈ X₁ · -- u ∈ X₁ ⇒ u ∈ X₁∪X₂; both interventions fix it; equal by hCompat_x₁. have huU : u ∈ X₁ ∪ X₂ := Finset.mem_union_left _ hu1 have hru_nuo : SWIGNode.random u ∉ M.unobserved := fun h => (Finset.disjoint_left.mp M.obs_unobs_disjoint (hObs₁ u hu1)) h have hf1 : SWIGNode.fixed u ∈ (M.fixSet X₁ hObs₁ hFix₁).fixed := fixed_mem_fixSet M X₁ hObs₁ hFix₁ hu1 have hfU : SWIGNode.fixed u ∈ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).fixed := fixed_mem_fixSet M (X₁ ∪ X₂) hObsU hFixU huU have hf1_nuo : SWIGNode.fixed u ∉ (M.fixSet X₁ hObs₁ hFix₁).unobserved := by intro h obtain ⟨m, hm⟩ := (M.fixSet X₁ hObs₁ hFix₁).unobserved_is_random _ h exact absurd hm (by simp) have hfU_nuo : SWIGNode.fixed u ∉ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).unobserved := by intro h obtain ⟨m, hm⟩ := (M.fixSet (X₁ ∪ X₂) hObsU hFixU).unobserved_is_random _ h exact absurd hm (by simp) rw [fixMonoParentMap_apply_random M.toSWIGGraph X₁ hObs₁ hFix₁ w₀.val u hu1 _ hwMem, fixMonoParentMap_apply_random M.toSWIGGraph (X₁ ∪ X₂) hObsU hFixU w₀.val u huU _ hwMem] simp only [Subtype.coe_mk] rw [dif_neg hf1_nuo, dif_pos hf1, dif_neg hfU_nuo, dif_pos hfU] -- LHS: sx₁ ⟨.fixed u⟩, RHS: sxU ⟨.fixed u⟩; equal by hCompat_x₁ (symm). exact (hCompat_x₁ u hu1).symm · by_cases hu2 : u ∈ X₂ · -- u ∈ X₂ \ X₁: union fixes it (reads sxU ⟨.fixed u⟩); -- do(X₁) recurses (reads (M.fixSet X₁).evalMap sx₁ ⟨.random u⟩). have huU : u ∈ X₁ ∪ X₂ := Finset.mem_union_right _ hu2 have hru_obs : SWIGNode.random u ∈ M.observed := hObsU u (Finset.mem_union_right _ hu2) have hru_nuo : SWIGNode.random u ∉ M.unobserved := fun h => (Finset.disjoint_left.mp M.obs_unobs_disjoint hru_obs) h -- RHS (do X₁) side: u ∉ X₁, so reads .random u; classify it. have hru_nd1fix : SWIGNode.random u ∉ (M.fixSet X₁ hObs₁ hFix₁).fixed := by intro h obtain ⟨m, hm⟩ := (M.fixSet X₁ hObs₁ hFix₁).fixed_is_fixed _ h exact absurd hm (by simp) have hru_nd1uo : SWIGNode.random u ∉ (M.fixSet X₁ hObs₁ hFix₁).unobserved := hru_nuo -- LHS (union) side: reads .fixed u. have hfU : SWIGNode.fixed u ∈ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).fixed := fixed_mem_fixSet M (X₁ ∪ X₂) hObsU hFixU huU have hfU_nuo : SWIGNode.fixed u ∉ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).unobserved := by intro h obtain ⟨m, hm⟩ := (M.fixSet (X₁ ∪ X₂) hObsU hFixU).unobserved_is_random _ h exact absurd hm (by simp) rw [fixMonoParentMap_apply_random_notMem M.toSWIGGraph X₁ hObs₁ hFix₁ w₀.val _ u hu1 hwMem, fixMonoParentMap_apply_random M.toSWIGGraph (X₁ ∪ X₂) hObsU hFixU w₀.val u huU _ hwMem] simp only [Subtype.coe_mk] rw [dif_neg hru_nd1uo, dif_neg hru_nd1fix, dif_neg hfU_nuo, dif_pos hfU] -- Goal: (M.fixSet X₁).evalMap sx₁ ℓ ⟨.random u⟩ = sxU ⟨.fixed u⟩. -- This is exactly hIntermediate u hu2 (up to membership-proof irrelevance). exact hIntermediate u hu2 · -- u ∉ X₁ ∪ X₂: both recurse; equal by IH at strictly smaller index. have huU : u ∉ X₁ ∪ X₂ := fun h => (Finset.mem_union.mp h).elim hu1 hu2 have hru_nd1fix : SWIGNode.random u ∉ (M.fixSet X₁ hObs₁ hFix₁).fixed := by intro h obtain ⟨m, hm⟩ := (M.fixSet X₁ hObs₁ hFix₁).fixed_is_fixed _ h exact absurd hm (by simp) have hru_ndUfix : SWIGNode.random u ∉ (M.fixSet (X₁ ∪ X₂) hObsU hFixU).fixed := by intro h obtain ⟨m, hm⟩ := (M.fixSet (X₁ ∪ X₂) hObsU hFixU).fixed_is_fixed _ h exact absurd hm (by simp) rw [fixMonoParentMap_apply_random_notMem M.toSWIGGraph X₁ hObs₁ hFix₁ w₀.val _ u hu1 hwMem, fixMonoParentMap_apply_random_notMem M.toSWIGGraph (X₁ ∪ X₂) hObsU hFixU w₀.val _ u huU hwMem] simp only [Subtype.coe_mk] -- Same three-way classification on both sides. split_ifs with hd hm hm · rfl · exact absurd hd hm · exact absurd hm hd · -- both observed: recurse via IH at strictly smaller M-index. have hru_obs : SWIGNode.random u ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedgeM).1 with hc1 | hc2 · rcases Finset.mem_union.mp hc1 with hfx | hob · exact absurd hfx hru_nfix · exact hob · exact absurd hc2 hm set j := M.observedIndex ⟨SWIGNode.random u, hru_obs⟩ with hj have hlt : j.val < n := M.observed_parent_index_lt hn hedgeM hru_obs have hihm := ih j.val hlt j.isLt have hat : (M.observedAt ⟨j.val, j.isLt⟩).val = SWIGNode.random u := M.observedAt_observedIndex ⟨SWIGNode.random u, hru_obs⟩ have hsub : (⟨(M.observedAt ⟨j.val, j.isLt⟩).val, Finset.mem_union_left M.unobserved (M.observedAt ⟨j.val, j.isLt⟩).property⟩ : {w // w ∈ M.randomVars}) = ⟨SWIGNode.random u, Finset.mem_union_left _ hru_obs⟩ := Subtype.ext hat -- IH gives `(union).evalMap = (X₁).evalMap`; goal here is the symm. refine symm (Eq.ndrec (motive := fun w : {w // w ∈ M.randomVars} => (M.fixSet (X₁ ∪ X₂) hObsU hFixU).evalMap sxU ℓ w = -- … truncated; follow the source link for the rest …

theorem exists_evalMap_overrideC_factors_cutset (M : SCM N Ω) {Y C : Finset (SWIGNode N)} (hY : Y ⊆ M.observed) (hC : C ⊆ M.observed) (s : FixedValues M) (c : ValuesOn C (swigΩ Ω)) : ∃ h : ValuesOn (M.cutsetLatent Y C) (swigΩ Ω) → ValuesOn Y (swigΩ Ω), Measurable h ∧ ∀ ℓ : LatentValues M, M.evalMap_overrideC hY hC s c ℓ = h (valuesProjection (M.cutsetLatent_subset Y C) ℓ) := by classical -- Extend a cutset projection to a full latent vector (default off the cutset). let ℓ₀ : LatentValues M := fun u => by letI : IsProbabilityMeasure (M.latentDist u) := M.isProbability_latent u exact MeasureTheory.nonempty_of_isProbabilityMeasure (M.latentDist u) |>.some let extend : ValuesOn (M.cutsetLatent Y C) (swigΩ Ω) → LatentValues M := fun cwProj u => if h : u.val ∈ M.cutsetLatent Y C then cwProj ⟨u.val, h⟩ else ℓ₀ u have hext_meas : Measurable extend := by refine measurable_pi_lambda _ (fun u => ?_) by_cases h : u.val ∈ M.cutsetLatent Y C · have : (fun cwProj : ValuesOn (M.cutsetLatent Y C) (swigΩ Ω) => extend cwProj u) = fun cwProj => cwProj ⟨u.val, h⟩ := by funext cwProj; simp [extend, h] rw [this]; exact measurable_pi_apply _ · have : (fun cwProj : ValuesOn (M.cutsetLatent Y C) (swigΩ Ω) => extend cwProj u) = fun _ => ℓ₀ u := by funext cwProj; simp [extend, h] rw [this]; exact measurable_const refine ⟨fun cwProj => M.evalMap_overrideC hY hC s c (extend cwProj), ?_, ?_⟩ · -- Measurability: override map (jointly measurable) precomposed with `extend`. have hcomp : (fun cwProj => M.evalMap_overrideC hY hC s c (extend cwProj)) = (fun ℓ : LatentValues M => M.evalMap_overrideC hY hC s c ℓ) ∘ extend := by funext cwProj; rfl rw [hcomp] have hcurry : (fun ℓ : LatentValues M => M.evalMap_overrideC hY hC s c ℓ) = (fun p : (M.FixedValues × ValuesOn C (swigΩ Ω)) × M.LatentValues => M.evalMap_overrideC hY hC p.1.1 p.1.2 p.2) ∘ (fun ℓ => ((s, c), ℓ)) := by funext ℓ; rfl rw [hcurry, Function.comp_assoc] exact (measurable_evalMap_overrideC M hY hC).comp ((measurable_const.prodMk measurable_id).comp hext_meas) · -- Agreement: `extend (proj ℓ)` agrees with `ℓ` on the cutset, so apply (A). intro ℓ change M.evalMap_overrideC hY hC s c ℓ = M.evalMap_overrideC hY hC s c (extend (valuesProjection (M.cutsetLatent_subset Y C) ℓ)) refine evalMap_overrideC_agree_cutset M hY hC s c ℓ _ ?_ funext u simp only [valuesProjection, extend, dif_pos u.property]