SCM.ID.Graphical­Thms

theorem subset_fixAncestralSet (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) : Y ⊆ fixAncestralSet M X hObs hFix Y := (M.fixSet X hObs hFix).toSWIGGraph.dag.subset_ancestralSet Y

lemma splitMono_edge_from_unobserved_iff (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) {u v : SWIGNode N} (hu : u ∈ G.unobserved) : (G.splitMono X hObs hFix).dag.edge u v ↔ G.dag.edge u v := by obtain ⟨d, rfl⟩ := G.unobserved_is_random u hu have hdX : d ∉ X := by intro hd exact (Finset.disjoint_left.mp G.obs_unobs_disjoint (hObs d hd)) hu simp [SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel, hdX]

lemma splitMono_directlyConfounded_iff (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) (v₁ v₂ : SWIGNode N) : (G.splitMono X hObs hFix).directlyConfounded v₁ v₂ ↔ G.directlyConfounded v₁ v₂ := by constructor · rintro ⟨hne, u, hu, hu₁, hu₂⟩ exact ⟨hne, u, hu, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mp hu₁, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mp hu₂⟩ · rintro ⟨hne, u, hu, hu₁, hu₂⟩ exact ⟨hne, u, hu, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mpr hu₁, (splitMono_edge_from_unobserved_iff G X hObs hFix hu).mpr hu₂⟩

lemma splitMono_bidirectedReachable_iff (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) (v w : SWIGNode N) : (G.splitMono X hObs hFix).bidirectedReachable v w ↔ G.bidirectedReachable v w := by constructor · intro h induction h with | refl hv => exact SWIGGraph.bidirectedReachable.refl hv | step hreach hconf ih => exact SWIGGraph.bidirectedReachable.step ih ((splitMono_directlyConfounded_iff G X hObs hFix _ _).mp hconf) · intro h induction h with | refl hv => exact SWIGGraph.bidirectedReachable.refl hv | step hreach hconf ih => exact SWIGGraph.bidirectedReachable.step ih ((splitMono_directlyConfounded_iff G X hObs hFix _ _).mpr hconf)

lemma splitMono_cComponentOf_eq (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) (v : SWIGNode N) : (G.splitMono X hObs hFix).cComponentOf v = G.cComponentOf v := by by_cases hv : v ∈ G.observed · apply Finset.Subset.antisymm · intro w hw rw [G.mem_cComponentOf_iff_reachable hv] exact (splitMono_bidirectedReachable_iff G X hObs hFix v w).mp (((G.splitMono X hObs hFix).mem_cComponentOf_iff_reachable hv).mp hw) · intro w hw rw [(G.splitMono X hObs hFix).mem_cComponentOf_iff_reachable hv] exact (splitMono_bidirectedReachable_iff G X hObs hFix v w).mpr ((G.mem_cComponentOf_iff_reachable hv).mp hw) · simp [SWIGGraph.cComponentOf, SWIGGraph.bidirectedBFS, hv]

lemma splitMono_cComponentSet_eq (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) : (G.splitMono X hObs hFix).cComponentSet = G.cComponentSet := by ext C simp [SWIGGraph.cComponentSet, splitMono_cComponentOf_eq G X hObs hFix]

lemma splitMono_no_edge_from_intervened_random (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) {d : N} (hd : d ∈ X) (v : SWIGNode N) : ¬ (G.splitMono X hObs hFix).dag.edge (SWIGNode.random d) v := by simp [SWIGGraph.splitMono, SWIGGraph.splitMonoDAG, SWIGGraph.splitMonoEdgeRel, hd]

lemma splitMono_not_isAncestor_from_intervened_random (G : SWIGGraph N) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ G.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ G.fixed) {d : N} (hd : d ∈ X) (v : SWIGNode N) : ¬ (G.splitMono X hObs hFix).dag.isAncestor (SWIGNode.random d) v := by intro h induction h with | edge he => exact splitMono_no_edge_from_intervened_random G X hObs hFix hd _ he | trans _ _ ih => exact ih

lemma random_intervened_mem_fixAncestralSet_iff_mem_Y (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) {d : N} (hd : d ∈ X) : SWIGNode.random d ∈ fixAncestralSet M X hObs hFix Y ↔ SWIGNode.random d ∈ Y := by constructor · intro h unfold fixAncestralSet at h rcases Finset.mem_union.mp h with hY | hAnc · exact hY · simp only [DAG.ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hAnc obtain ⟨v, hvY, hanc⟩ := hAnc have hno := splitMono_not_isAncestor_from_intervened_random (M.toSWIGGraph) X hObs hFix hd v have hno' : ¬ (M.fixSet X hObs hFix).toSWIGGraph.dag.isAncestor (SWIGNode.random d) v := by simpa [SCM.fixSet, SCM.fixMono] using hno exact elim (hno' hanc) · intro hY exact (M.fixSet X hObs hFix).toSWIGGraph.dag.subset_ancestralSet Y hY

lemma pinnedExtend_projection_eq [∀ n, Nonempty (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (sDo : (M.fixSet X hObs hFix).FixedValues) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (pinnedExtend M X hObs hFix Y sDo xD) = xD := by intro xD funext v rcases v with ⟨v, hv⟩ cases v with | random d => have hvD : SWIGNode.random d ∈ fixObservedAncestralSet M X hObs hFix Y := hv have hnotX : d ∉ X := by intro hd have hAnc : SWIGNode.random d ∈ fixAncestralSet M X hObs hFix Y := (Finset.mem_inter.mp hvD).1 have hYd : SWIGNode.random d ∈ Y := (random_intervened_mem_fixAncestralSet_iff_mem_Y M X hObs hFix Y hd).mp hAnc exact hYX d hd hYd simp [valuesProjection, pinnedExtend, hnotX, hvD] | fixed d => have hvD : SWIGNode.fixed d ∈ fixObservedAncestralSet M X hObs hFix Y := hv simp [valuesProjection, pinnedExtend, hvD]

lemma pinnedExtend_pin_eq [∀ n, Nonempty (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (sDo : (M.fixSet X hObs hFix).FixedValues) : ∀ xD (D : N) (hD : D ∈ X), pinnedExtend M X hObs hFix Y sDo xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩ := by intro xD D hD simp [pinnedExtend, hD]

lemma fixSet_cComponentSet_eq (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) : (M.fixSet X hObs hFix).toSWIGGraph.cComponentSet = M.toSWIGGraph.cComponentSet := by simpa [SCM.fixSet, SCM.fixMono] using (splitMono_cComponentSet_eq (M.toSWIGGraph) X hObs hFix)

lemma fixSet_cComponentSet_mem (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (S : Finset (SWIGNode N)) : S ∈ (M.fixSet X hObs hFix).toSWIGGraph.cComponentSet ↔ S ∈ M.toSWIGGraph.cComponentSet := by rw [fixSet_cComponentSet_eq M X hObs hFix]

lemma fixObservedAncestralSet_obsParent_closed (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) : (M.fixSet X hObs hFix).ObsParentClosed (fixObservedAncestralSet M X hObs hFix Y) := by refine ⟨Finset.inter_subset_right, ?_⟩ intro v hv w hw hEdge have hvAnc : v ∈ fixAncestralSet M X hObs hFix Y := (Finset.mem_inter.mp hv).1 have hwAnc : w ∈ fixAncestralSet M X hObs hFix Y := by unfold fixAncestralSet at hvAnc ⊢ exact DAG.mem_ancestralSet_of_edge_to_mem (M.fixSet X hObs hFix).toSWIGGraph.dag hEdge hvAnc exact Finset.mem_inter.mpr ⟨hwAnc, hw⟩

theorem inducedAncestral_parent_closed (G : SWIGGraph N) {T C : Finset (SWIGNode N)} (hT : T ⊆ G.observed) : ∀ v ∈ T, ∀ w ∈ inducedAncestral G T C, G.dag.edge v w → v ∈ inducedAncestral G T C := by classical intro v hvT w hw hEdge unfold inducedAncestral at hw ⊢ rcases Finset.mem_inter.mp hw with ⟨hwAnc, hwIndObs⟩ have hvIndObs : v ∈ (G.induce T).observed := by simp [SWIGGraph.induce, hvT, hT hvT] have hwIndObs' : w ∈ T ∩ G.observed := by simpa [SWIGGraph.induce] using hwIndObs have hEdgeInd : (G.induce T).dag.edge v w := by rw [SWIGGraph.induce] rw [SWIGGraph.inducedDag_edge_iff] refine ⟨hEdge, ?_, ?_⟩ · simp [hvT, hT hvT] · simp [(Finset.mem_inter.mp hwIndObs').1, (Finset.mem_inter.mp hwIndObs').2] have hvAnc : v ∈ (G.induce T).dag.ancestralSet C := by rcases Finset.mem_union.mp hwAnc with hwC | hwA · exact (G.induce T).dag.mem_ancestralSet_of_isAncestor hwC (DAG.isAncestor.edge hEdgeInd) · apply mem_union_right simp only [DAG.ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hwA ⊢ obtain ⟨c, hcC, hwc⟩ := hwA exact ⟨c, hcC, (G.induce T).dag.isAncestor_trans (DAG.isAncestor.edge hEdgeInd) hwc⟩ exact Finset.mem_inter.mpr ⟨hvAnc, hvIndObs⟩

theorem containingCComponent_of_mem_cComponentSet (G : SWIGGraph N) (S : Finset (SWIGNode N)) (hS : S ∈ G.cComponentSet) : containingCComponent G S = S := by simp only [SWIGGraph.cComponentSet] at hS obtain ⟨v, hv, rfl⟩ := Finset.mem_image.mp hS have hne : (G.cComponentOf v).Nonempty := ⟨v, G.mem_cComponentOf_self hv⟩ simp only [containingCComponent, dif_pos hne] have hreach : G.bidirectedReachable v hne.choose := (G.mem_cComponentOf_iff_reachable hv).mp hne.choose_spec exact (G.cComponentOf_eq_of_reachable hreach).symm

theorem inducedAncestral_self_of_mem_cComponentSet (G : SWIGGraph N) (S : Finset (SWIGNode N)) (hS : S ∈ G.cComponentSet) : inducedAncestral G S S = S := by have hSobs : S ⊆ G.observed := G.cComponentSet_subset_observed S hS have hobs : (G.induce S).observed = S := by change S ∩ G.observed = S exact Finset.inter_eq_left.mpr hSobs rw [inducedAncestral, hobs] apply Finset.Subset.antisymm · exact inter_subset_right · intro x hx exact Finset.mem_inter.mpr ⟨(G.induce S).dag.subset_ancestralSet S hx, hx⟩

lemma qFactorParents_subset_observed (C : Finset (SWIGNode N)) : G.qFactorParents C ⊆ G.observed := by intro w hw rcases Finset.mem_sdiff.mp hw with ⟨hw_union, _⟩ rcases Finset.mem_biUnion.mp hw_union with ⟨v, _, hw_pred⟩ exact G.observedPredecessors_subset_observed v hw_pred

lemma mem_prefixIn_iff (H : SWIGGraph N) (D : Finset (SWIGNode N)) (n : ℕ) (v : SWIGNode N) : v ∈ H.prefixIn D n ↔ ∃ h : v ∈ D, (H.nodeIndex D ⟨v, h⟩).val < n := by unfold SWIGGraph.prefixIn constructor · intro hv rcases Finset.mem_filter.mp hv with ⟨hD, hltif⟩ exact ⟨hD, by simpa [hD] using hltif⟩ · rintro ⟨hD, hlt⟩ exact Finset.mem_filter.mpr ⟨hD, by simpa [hD] using hlt⟩

lemma prefixIn_zero (H : SWIGGraph N) (D : Finset (SWIGNode N)) : H.prefixIn D 0 = ∅ := by ext v constructor · intro hv rcases (mem_prefixIn_iff H D 0 v).mp hv with ⟨_, hlt⟩ omega · simp

lemma nodesAt_mem_prefixIn_iff (H : SWIGGraph N) (D : Finset (SWIGNode N)) (n : ℕ) (i : Fin D.card) : (H.nodesAt D i).val ∈ H.prefixIn D n ↔ i.val < n := by rw [mem_prefixIn_iff] constructor · rintro ⟨hD, hlt⟩ have hidx : H.nodeIndex D ⟨(H.nodesAt D i).val, hD⟩ = i := by have hsub : (⟨(H.nodesAt D i).val, hD⟩ : {v // v ∈ D}) = H.nodesAt D i := Subtype.ext rfl rw [hsub] simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] rwa [hidx] at hlt · intro hlt exact ⟨(H.nodesAt D i).property, by have hidx : H.nodeIndex D (H.nodesAt D i) = i := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] simpa [hidx] using hlt⟩

lemma prefixIn_card (H : SWIGGraph N) (D : Finset (SWIGNode N)) : H.prefixIn D D.card = D := by ext v constructor · exact fun hv => H.prefixIn_subset D D.card hv · intro hv exact (mem_prefixIn_iff H D D.card v).mpr ⟨hv, (H.nodeIndex D ⟨v, hv⟩).isLt⟩

lemma prefixIn_mono (H : SWIGGraph N) (D : Finset (SWIGNode N)) {m k : ℕ} (h : m ≤ k) : H.prefixIn D m ⊆ H.prefixIn D k := by intro v hv rcases (mem_prefixIn_iff H D m v).mp hv with ⟨hD, hlt⟩ exact (mem_prefixIn_iff H D k v).mpr ⟨hD, lt_of_lt_of_le hlt h⟩

lemma nodesAt_not_mem_prefixIn (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : (H.nodesAt D ⟨n, hn⟩).val ∉ H.prefixIn D n := by rw [nodesAt_mem_prefixIn_iff H D n ⟨n, hn⟩] exact Nat.lt_irrefl n

lemma prefixIn_succ (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : H.prefixIn D (n + 1) = H.prefixIn D n ∪ {(H.nodesAt D ⟨n, hn⟩).val} := by ext v constructor · intro hv rcases (mem_prefixIn_iff H D (n + 1) v).mp hv with ⟨hD, hlt⟩ by_cases hlt_n : (H.nodeIndex D ⟨v, hD⟩).val < n · exact mem_union_left _ ((mem_prefixIn_iff H D n v).mpr ⟨hD, hlt_n⟩) · have hidx_val : (H.nodeIndex D ⟨v, hD⟩).val = n := by omega have hidx : H.nodeIndex D ⟨v, hD⟩ = ⟨n, hn⟩ := Fin.ext hidx_val have hv_eq : v = (H.nodesAt D ⟨n, hn⟩).val := by have hround : H.nodesAt D (H.nodeIndex D ⟨v, hD⟩) = ⟨v, hD⟩ := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] rw [hidx] at hround exact congrArg val hround.symm exact mem_union_right _ (by simp [hv_eq]) · intro hv rcases Finset.mem_union.mp hv with hvpre | hvlast · rcases (mem_prefixIn_iff H D n v).mp hvpre with ⟨hD, hlt⟩ exact (mem_prefixIn_iff H D (n + 1) v).mpr ⟨hD, by omega⟩ · have hv_eq : v = (H.nodesAt D ⟨n, hn⟩).val := by simpa using hvlast subst hv_eq rw [nodesAt_mem_prefixIn_iff H D (n + 1) ⟨n, hn⟩] exact Nat.lt_succ_self n

lemma prefixIn_disjoint_singleton_next (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : Disjoint (H.prefixIn D n) ({(H.nodesAt D ⟨n, hn⟩).val} : Finset (SWIGNode N)) := by rw [Finset.disjoint_singleton_right] exact nodesAt_not_mem_prefixIn H D hn

lemma measurable_extendTianPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : Measurable (extendTianPrefix (Ω := Ω) H D hn) := by unfold extendTianPrefix exact (valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hn).symm).measurable.comp (measurable_valuesUnionMk (Ω := swigΩ Ω))

lemma valuesUnionEquiv_extendTianPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) (p : ValuesOn (H.prefixIn D n) (swigΩ Ω) × ValuesOn ({(H.nodesAt D ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) : valuesUnionEquiv (Ω := Ω) (prefixIn_disjoint_singleton_next H D hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hn)) (extendTianPrefix (Ω := Ω) H D hn p)) = p := by unfold extendTianPrefix exact valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk (prefixIn_disjoint_singleton_next H D hn) (prefixIn_succ H D hn) p

lemma jointRef_extendTianPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) {k : ℕ} (hk : k < D.card) : ((jointRef ref (H.prefixIn D k)).prod (jointRef ref ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)))).map (extendTianPrefix (Ω := Ω) H D hk) = jointRef ref (H.prefixIn D (k + 1)) := by classical let v : SWIGNode N := (H.nodesAt D ⟨k, hk⟩).val let A : Finset (SWIGNode N) := H.prefixIn D k let B : Finset (SWIGNode N) := ({v} : Finset (SWIGNode N)) let hDisj : Disjoint A B := by simpa [A, B, v] using prefixIn_disjoint_singleton_next H D hk have hunion : ((jointRef ref A).prod (jointRef ref B)).map ((valuesUnionEquiv (Ω := Ω) hDisj).symm) = jointRef ref (A ∪ B) := by have hmp := (measurePreserving_valuesUnionEquiv (Ω := Ω) hDisj ref.μ).symm (valuesUnionEquiv (Ω := Ω) hDisj) simpa [jointRef] using hmp.map_eq unfold extendTianPrefix change (((jointRef ref A).prod (jointRef ref B)).map ((valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hk).symm) ∘ (fun p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk p.1 p.2))) = jointRef ref (H.prefixIn D (k + 1)) rw [← MeasureTheory.Measure.map_map] · have hinner : (fun p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk p.1 p.2) = ((valuesUnionEquiv (Ω := Ω) hDisj).symm) := by rfl rw [hinner, hunion] rw [jointRef, map_pi_valuesEquivOfEq] rfl · exact (valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hk).symm).measurable · exact measurable_valuesUnionMk (Ω := swigΩ Ω)

lemma jointRef_map_prefixIn_absolutelyContinuous (H : SWIGGraph N) (D : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (k : ℕ) : (jointRef ref D).map (valuesProjection (H.prefixIn_subset D k)) ≪ jointRef ref (H.prefixIn D k) := by classical have hsubset : H.prefixIn D k ⊆ D := H.prefixIn_subset D k have hDisj : Disjoint (H.prefixIn D k) (D \ H.prefixIn D k) := disjoint_sdiff_self_right have hAB : H.prefixIn D k ∪ (D \ H.prefixIn D k) = D := Finset.union_sdiff_of_subset hsubset have hfun : (valuesProjection (Ω := swigΩ Ω) hsubset) = fst ∘ (valuesUnionEquiv (Ω := Ω) hDisj) ∘ (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm) := by funext ω i rfl have hmarg : (jointRef ref D).map (valuesProjection hsubset) = (jointRef ref (D \ H.prefixIn D k) univ) • jointRef ref (H.prefixIn D k) := by rw [hfun] rw [← MeasureTheory.Measure.map_map measurable_fst ((valuesUnionEquiv (Ω := Ω) hDisj).measurable.comp (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm).measurable)] rw [← MeasureTheory.Measure.map_map (valuesUnionEquiv (Ω := Ω) hDisj).measurable (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm).measurable] rw [jointRef, map_pi_valuesEquivOfEq hAB.symm (fun i : {i // i ∈ D} => ref.μ i.val)] have hsplit : (pi (fun j : {j // j ∈ H.prefixIn D k ∪ (D \ H.prefixIn D k)} => ref.μ j.val)).map (valuesUnionEquiv (Ω := Ω) hDisj) = (jointRef ref (H.prefixIn D k)).prod (jointRef ref (D \ H.prefixIn D k)) := by have hmp := measurePreserving_valuesUnionEquiv (Ω := Ω) hDisj ref.μ simpa [jointRef] using hmp.map_eq rw [hsplit, MeasureTheory.Measure.map_fst_prod] rw [hmarg] intro t ht simp [MeasureTheory.Measure.smul_apply, ht]

lemma measure_map_prefixIn_absolutelyContinuous_jointRef (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) (hdom : μ ≪ jointRef ref D) (k : ℕ) : μ.map (valuesProjection (H.prefixIn_subset D k)) ≪ jointRef ref (H.prefixIn D k) := by exact ((hdom.map (measurable_valuesProjection (H.prefixIn_subset D k))).trans (jointRef_map_prefixIn_absolutelyContinuous H D ref k))

lemma tianPrefixDensityProductInPrefix_eq_range_product (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [IsFiniteMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (k : ℕ) (hk : k ≤ D.card) (z : ValuesOn (H.prefixIn D k) (swigΩ Ω)) : tianPrefixDensityProductInPrefix H D μ ref k z = ∏ i ∈ range k, tianPrefixStepDensityInPrefix H D μ ref k z i := by induction k with | zero => simp [tianPrefixDensityProductInPrefix] | succ k ih => have hkcard : k < D.card := Nat.lt_of_succ_le hk rw [tianPrefixDensityProductInPrefix] rw [ih (le_of_succ_le hk) (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z)] rw [Finset.prod_range_succ] congr 1 · refine Finset.prod_congr rfl ?_ intro i hi have hik : i < k := Finset.mem_range.mp hi have hisucc : i < k + 1 := Nat.lt_succ_of_lt hik have hicard : i < D.card := lt_of_lt_of_le hik (le_of_succ_le hk) have hproj : valuesProjection (prefixIn_mono H D (le_of_lt hik)) (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z) = valuesProjection (prefixIn_mono H D (le_of_lt hisucc)) z := by funext a rfl have hnode : valuesProjection (show ({(H.nodesAt D ⟨i, hicard⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D k from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D k ⟨i, hicard⟩] exact hik) (valuesProjection (prefixIn_mono H D (Nat.le_succ k)) z) = valuesProjection (show ({(H.nodesAt D ⟨i, hicard⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D (k + 1) from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D (k + 1) ⟨i, hicard⟩] exact hisucc) z := by funext a rfl simp [tianPrefixStepDensityInPrefix, hik, hisucc, hicard, hproj, hnode] · simp [tianPrefixStepDensityInPrefix, hkcard]

lemma tianPrefixDensityProductInPrefix_card_eq_tianDensityProduct (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [IsFiniteMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (y : ValuesOn (H.prefixIn D D.card) (swigΩ Ω)) : tianPrefixDensityProductInPrefix H D μ ref D.card y = tianDensityProduct H D μ ref ((valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_card H D)) y) := by rw [tianPrefixDensityProductInPrefix_eq_range_product H D μ ref D.card (le_refl _) y] rw [Finset.prod_range] simp only [tianDensityProduct, tianPrefixStepDensity, tianPrefixStepDensityInPrefix, coe_valuesEquivOfEq] refine Finset.prod_congr rfl ?_ intro i _hi have hproj : valuesProjection (H.prefixIn_subset D i.val) (valuesProjection (le_of_eq (prefixIn_card H D).symm) y) = valuesProjection (prefixIn_mono H D (le_of_lt i.isLt)) y := by funext a rfl have hnode : valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) (valuesProjection (le_of_eq (prefixIn_card H D).symm) y) = valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D D.card from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D D.card i] exact i.isLt) y := by funext a rfl simp [i.isLt, hproj, hnode]

lemma measure_prefixIn_rnDeriv_eq_tianPrefixDensityProductInPrefix (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] [StandardBorelSpace (ValuesOn D (swigΩ Ω))] [IsProbabilityMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (hdom : μ ≪ Causalean.SCM.jointRef ref D) : ∀ (k : ℕ) (_hk : k ≤ D.card), (μ.map (valuesProjection (H.prefixIn_subset D k))).rnDeriv (Causalean.SCM.jointRef ref (H.prefixIn D k)) =ᵐ[Causalean.SCM.jointRef ref (H.prefixIn D k)] tianPrefixDensityProductInPrefix H D μ ref k := by intro k induction k with | zero => intro _hk have hsub : Subsingleton (ValuesOn (H.prefixIn D 0) (swigΩ Ω)) := ⟨fun a b => funext fun i => absurd (prefixIn_zero H D ▸ i.property) (notMem_empty i.val)⟩ have heq : μ.map (valuesProjection (H.prefixIn_subset D 0)) = Causalean.SCM.jointRef ref (H.prefixIn D 0) := by refine MeasureTheory.Measure.ext fun A _ => ?_ rcases Set.eq_empty_or_nonempty A with rfl | hA · simp · obtain ⟨a, ha⟩ := hA have hAuniv : A = univ := Set.eq_univ_of_forall fun x => (hsub.elim x a) ▸ ha subst hAuniv rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection (H.prefixIn_subset D 0)) MeasurableSet.univ] simp only [Set.preimage_univ] rw [MeasureTheory.measure_univ, Causalean.SCM.jointRef, MeasureTheory.Measure.pi_univ] symm apply Finset.prod_eq_one intro i hi have : i.val ∈ (∅ : Finset (SWIGNode N)) := by simpa [prefixIn_zero H D] using i.property simp at this rw [heq] have h1 : tianPrefixDensityProductInPrefix H D μ ref 0 = (fun _ => (1 : ENNReal)) := rfl rw [h1] exact MeasureTheory.Measure.rnDeriv_self _ | succ k ih => intro hk classical have hkc : k < D.card := Nat.lt_of_succ_le hk have hkprev : k ≤ D.card := Nat.le_of_succ_le hk let node : SWIGNode N := (H.nodesAt D ⟨k, hkc⟩).val let A : Finset (SWIGNode N) := H.prefixIn D k let B : Finset (SWIGNode N) := ({node} : Finset (SWIGNode N)) let νk : Measure (ValuesOn A (swigΩ Ω)) := Causalean.SCM.jointRef ref A let ρ : Measure (ValuesOn B (swigΩ Ω)) := Causalean.SCM.jointRef ref B let prefixMap : ValuesOn D (swigΩ Ω) → ValuesOn A (swigΩ Ω) := valuesProjection (H.prefixIn_subset D k) let nodeMap : ValuesOn D (swigΩ Ω) → ValuesOn B (swigΩ Ω) := valuesProjection (show B ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨k, hkc⟩).property) let succMap : ValuesOn D (swigΩ Ω) → ValuesOn (H.prefixIn D (k + 1)) (swigΩ Ω) := valuesProjection (H.prefixIn_subset D (k + 1)) let chain : Measure (ValuesOn A (swigΩ Ω)) := μ.map prefixMap let stepK : Kernel (ValuesOn A (swigΩ Ω)) (ValuesOn B (swigΩ Ω)) := ProbabilityTheory.condDistrib nodeMap prefixMap μ let ext : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) → ValuesOn (H.prefixIn D (k + 1)) (swigΩ Ω) := extendTianPrefix (Ω := Ω) H D hkc have hcomp_ext : ext ∘ (fun x : ValuesOn D (swigΩ Ω) => (prefixMap x, nodeMap x)) = succMap := by funext x ext a by_cases hmem : a.val ∈ H.prefixIn D k · simp [ext, prefixMap, nodeMap, succMap, A, B, node, extendTianPrefix, coe_valuesEquivOfEq, valuesProjection, valuesUnionMk, hmem] · simp [ext, prefixMap, nodeMap, succMap, A, B, node, extendTianPrefix, coe_valuesEquivOfEq, valuesProjection, valuesUnionMk, hmem] have hchainSucc : μ.map succMap = (chain ⊗ₘ stepK).map ext := by have hpair : chain ⊗ₘ stepK = μ.map (fun x : ValuesOn D (swigΩ Ω) => (prefixMap x, nodeMap x)) := by dsimp [chain, stepK] exact ProbabilityTheory.compProd_map_condDistrib ((measurable_valuesProjection (Ω' := swigΩ Ω) (show B ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨k, hkc⟩).property)).aemeasurable) rw [hpair] rw [MeasureTheory.Measure.map_map] · rw [hcomp_ext] · exact measurable_extendTianPrefix (Ω := Ω) H D hkc · exact (measurable_valuesProjection (Ω' := swigΩ Ω) (H.prefixIn_subset D k)).prod (measurable_valuesProjection (Ω' := swigΩ Ω) (show B ⊆ D from by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D ⟨k, hkc⟩).property)) have hrefSucc : Causalean.SCM.jointRef ref (H.prefixIn D (k + 1)) = (νk.prod ρ).map ext := by dsimp [νk, ρ, A, B, node, ext] exact (jointRef_extendTianPrefix H D ref hkc).symm have hext_emb : MeasurableEmbedding ext := by dsimp [ext, A, B, node] unfold extendTianPrefix refine (valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_succ H D hkc).symm).measurableEmbedding.comp ?_ change MeasurableEmbedding (fun p : ValuesOn (H.prefixIn D k) (swigΩ Ω) × ValuesOn ({(H.nodesAt D ⟨k, hkc⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) => valuesUnionMk p.1 p.2) have hfun : (fun p : ValuesOn (H.prefixIn D k) (swigΩ Ω) × ValuesOn ({(H.nodesAt D ⟨k, hkc⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) => valuesUnionMk p.1 p.2) = ((valuesUnionEquiv (Ω := Ω) (prefixIn_disjoint_singleton_next H D hkc)).symm) := by rfl rw [hfun] exact ((valuesUnionEquiv (Ω := Ω) (prefixIn_disjoint_singleton_next H D hkc)).symm.measurableEmbedding) have hcore : (chain ⊗ₘ stepK).rnDeriv (νk.prod ρ) =ᵐ[νk.prod ρ] fun p => tianPrefixDensityProductInPrefix H D μ ref k p.1 * (stepK p.1).rnDeriv ρ p.2 := by have hchain_ac : chain ≪ νk := by dsimp [chain, νk, prefixMap, A] exact measure_map_prefixIn_absolutelyContinuous_jointRef H D μ ref hdom k have hsucc_ac : μ.map succMap ≪ Causalean.SCM.jointRef ref (H.prefixIn D (k + 1)) := by dsimp [succMap] exact measure_map_prefixIn_absolutelyContinuous_jointRef H D μ ref hdom (k + 1) have hjoint_map : (chain ⊗ₘ stepK).map ext ≪ (νk.prod ρ).map ext := by simpa [hchainSucc, hrefSucc] using hsucc_ac have hjoint : chain ⊗ₘ stepK ≪ νk.prod ρ := absolutelyContinuous_of_map_measurableEmbedding hext_emb hjoint_map -- In this finite/discrete setting `ρ` is finite, so `Kernel.const _ ρ` is a -- finite kernel and fibre domination follows from joint domination. have hfiber : ∀ᵐ a ∂chain, stepK a ≪ ρ := by have hjoint_const : chain ⊗ₘ stepK ≪ νk ⊗ₘ const _ ρ := by rwa [MeasureTheory.Measure.compProd_const] filter_upwards [hjoint_const.kernel_of_compProd] with a ha simpa [ProbabilityTheory.Kernel.const_apply] using ha have hfiber_meas : AEMeasurable (fun p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => (stepK p.1).rnDeriv ρ p.2) (νk.prod ρ) := aemeasurable_fiber_rnDeriv_of_finite (νk.prod ρ) ρ stepK exact rnDeriv_compProd_prod_sigmaFinite chain νk ρ stepK (tianPrefixDensityProductInPrefix H D μ ref k) hchain_ac hfiber hfiber_meas (ih hkprev) rw [hchainSucc, hrefSucc, EventuallyEq, hext_emb.ae_map_iff] filter_upwards [hext_emb.rnDeriv_map (chain ⊗ₘ stepK) (νk.prod ρ), hcore] with p hmap hp rw [hmap, hp] dsimp [ext, stepK, ρ, B, node] have hpair := valuesUnionEquiv_extendTianPrefix H D hkc p have hproj_ext : valuesProjection (prefixIn_mono H D (Nat.le_succ k)) (extendTianPrefix (Ω := Ω) H D hkc p) = p.1 := by funext i have hi := congrArg (fun q => q.1 i) hpair simpa [valuesUnionEquiv, valuesProjection, coe_valuesEquivOfEq] using hi have hnode_ext : valuesProjection (show ({(H.nodesAt D ⟨k, hkc⟩).val} : Finset (SWIGNode N)) ⊆ H.prefixIn D (k + 1) from by intro v hv rw [mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D (k + 1) ⟨k, hkc⟩] exact Nat.lt_succ_self k) (extendTianPrefix (Ω := Ω) H D hkc p) = p.2 := by funext i have hi := congrArg (fun q => q.2 i) hpair simpa [valuesUnionEquiv, valuesProjection, coe_valuesEquivOfEq] using hi rw [tianPrefixDensityProductInPrefix] simp [hkc, hproj_ext, hnode_ext, A, B, node, prefixMap, nodeMap]

theorem rnDeriv_eq_tianDensityProduct (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] [StandardBorelSpace (ValuesOn D (swigΩ Ω))] [IsProbabilityMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (hdom : μ ≪ jointRef ref D) : μ.rnDeriv (jointRef ref D) =ᵐ[jointRef ref D] tianDensityProduct H D μ ref := by classical set e := valuesEquivOfEq (Ω := swigΩ Ω) (prefixIn_card H D) with he have hf : MeasurableEmbedding (e : ValuesOn (H.prefixIn D D.card) (swigΩ Ω) → ValuesOn D (swigΩ Ω)) := e.measurableEmbedding have hμe : (μ.map e.symm).map e = μ := by rw [MeasureTheory.Measure.map_map e.measurable e.symm.measurable] have hcomp : (e : ValuesOn (H.prefixIn D D.card) (swigΩ Ω) → ValuesOn D (swigΩ Ω)) ∘ e.symm = id := by funext x exact e.right_inv x rw [hcomp, MeasureTheory.Measure.map_id] have href : (jointRef ref (H.prefixIn D D.card)).map e = jointRef ref D := by rw [jointRef, jointRef, map_pi_valuesEquivOfEq] have hprefixMap : valuesProjection (H.prefixIn_subset D D.card) = (e.symm : ValuesOn D (swigΩ Ω) → ValuesOn (H.prefixIn D D.card) (swigΩ Ω)) := by funext x i rfl have hprefix : (μ.map e.symm).rnDeriv (jointRef ref (H.prefixIn D D.card)) =ᵐ[jointRef ref (H.prefixIn D D.card)] tianPrefixDensityProductInPrefix H D μ ref D.card := by simpa [hprefixMap] using (measure_prefixIn_rnDeriv_eq_tianPrefixDensityProductInPrefix H D μ ref hdom D.card (le_refl _)) have hmap : μ.rnDeriv (jointRef ref D) =ᵐ[jointRef ref D] fun x => ((μ.map e.symm).rnDeriv (jointRef ref (H.prefixIn D D.card))) (e.symm x) := by rw [← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hf.rnDeriv_map (μ.map e.symm) (jointRef ref (H.prefixIn D D.card))] with y hy simpa [hμe] using hy refine hmap.trans ?_ rw [← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hprefix] with y hy have hleft : e.symm (e y) = y := e.left_inv y rw [hleft, hy] simpa using tianPrefixDensityProductInPrefix_card_eq_tianDensityProduct H D μ ref y

theorem doObsKernelAncestralMarginal_globalMarkovOn [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) [StandardBorelSpace (M.fixSet X hObs hFix).RandomValues] [StandardBorelSpace (M.fixSet X hObs hFix).ObservedValues] [∀ s : (M.fixSet X hObs hFix).FixedValues, IsFiniteMeasure ((M.fixSet X hObs hFix).jointKernel s)] [∀ s : (M.fixSet X hObs hFix).FixedValues, IsFiniteMeasure ((M.fixSet X hObs hFix).obsKernel s)] (s : (M.fixSet X hObs hFix).FixedValues) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y s)] : let A := fixAncestralSet M X hObs hFix Y let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce A KernelGlobalMarkovOn H D (doObsKernelAncestralMarginal M X hObs hFix Y s) := by classical let M' := M.fixSet X hObs hFix let A := fixAncestralSet M X hObs hFix Y let D := fixObservedAncestralSet M X hObs hFix Y change KernelGlobalMarkovOn (M'.toSWIGGraph.induce A) D ((doObsKernelAncestralMarginal M X hObs hFix Y) s) dsimp [KernelGlobalMarkovOn] intro X' Y' Z' hX hY hZ hXY hXZ hYZ hdSep have hD_obs : D ⊆ M'.observed := by intro v hv exact (Finset.mem_inter.mp hv).2 have hX_obs : X' ⊆ M'.observed := fun v hv => hD_obs (hX hv) have hY_obs : Y' ⊆ M'.observed := fun v hv => hD_obs (hY hv) have hZ_obs : Z' ⊆ M'.observed := fun v hv => hD_obs (hZ hv) have hA_closed : M'.dag.ancestralSet A = A := by simpa [A, fixAncestralSet, M'] using (M'.dag.ancestralSet_idem Y) have hdSep_fixed : M'.dag.dSep X' Y' (Z' ∪ M'.fixed) := by simpa [A, D, M'] using (M'.toSWIGGraph.dSep_union_fixed_of_induce_dSep A X' Y' Z' hX hY hZ (by simp [hA_closed]) hdSep) have hCI_obs : SCM.ObsCondIndep M' X' Y' Z' hX_obs hY_obs hZ_obs (M'.obsKernel s) := SCM.globalMarkov_with_fixed M' X' Y' Z' M'.fixed hX_obs hY_obs hZ_obs (by intro v hv; exact hv) hdSep_fixed s unfold KernelObsCondIndepOn unfold SCM.ObsCondIndep at hCI_obs have hCI_pre : CondIndepFun (comap (valuesProjection hZ ∘ valuesProjection hD_obs) inferInstance) (comap_le ((measurable_valuesProjection hZ).comp (measurable_valuesProjection hD_obs))) (valuesProjection hX ∘ valuesProjection hD_obs) (valuesProjection hY ∘ valuesProjection hD_obs) (M'.obsKernel s) := by convert hCI_obs using 2 <;> rfl have hCI_map : CondIndepFun (comap (valuesProjection hZ) inferInstance) (comap_valuesProjection_le hZ) (valuesProjection hX) (valuesProjection hY) ((M'.obsKernel s).map (valuesProjection hD_obs)) := condIndepFun_of_map (φ := valuesProjection hD_obs) (measurable_valuesProjection hD_obs) (measurable_valuesProjection hX) (measurable_valuesProjection hY) (measurable_valuesProjection hZ) hCI_pre convert hCI_map using 2 rw [doObsKernelAncestralMarginal, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection hD_obs)]

lemma tian_full_cComponent_density_recovery_core [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hStd : M.isStandard) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (sDo : (M.fixSet X hObs hFix).FixedValues) (S : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hSfull : S ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD) = xD) (hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S =ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD) := by exact tian_full_cComponent_density_recovery_core_direct M X hStd hObs hFix Y ref href sDo S hS hSfull hpos hYX extend hExtend hExtendX

lemma doAncestralDistrictDensity_recovered_from_obs_core_self [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hStd : M.isStandard) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (sDo : (M.fixSet X hObs hFix).FixedValues) (S : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hSfull : S ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD) = xD) (hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S =ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD) := by exact tian_full_cComponent_density_recovery_core M X hStd hObs hFix Y ref href sDo S hS hSfull hpos hYX extend hExtend hExtendX

lemma doAncestralDistrictDensity_recovered_from_obs_core [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hStd : M.isStandard) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (sDo : (M.fixSet X hObs hFix).FixedValues) (S C : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hReach : cFactorReachable M.toSWIGGraph C S) (hCmem : C ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD) = xD) (hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S =ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) C (extend xD) := by classical rcases hReach with ⟨hSnonempty, hSsubC, hSmem⟩ have hCS : C = S := by by_contra hne rcases hSnonempty with ⟨v, hvS⟩ have hvC : v ∈ C := hSsubC hvS have hdisj := M.toSWIGGraph.cComponentSet_pairwise_disjoint hCmem hSmem hne exact (Finset.disjoint_left.mp hdisj) hvC hvS subst C exact doAncestralDistrictDensity_recovered_from_obs_core_self M X hStd hObs hFix Y ref href sDo S hS hSmem hpos hYX extend hExtend hExtendX

theorem standardFixedValues_heq (M₁ M₂ : SCM N Ω) (hf : M₁.fixed = M₂.fixed) (h₁ : M₁.isStandard) : HEq (standardFixedValues M₁ h₁) (standardFixedValues M₂ (by change M₂.fixed = ∅ rw [← hf] exact h₁)) := by have h₁' : M₁.fixed = (∅ : Finset (SWIGNode N)) := h₁ haveI hempty : IsEmpty {v // v ∈ M₁.fixed} := ⟨fun i => absurd (h₁' ▸ i.property) (notMem_empty i.val)⟩ haveI hsub₁ : Subsingleton M₁.FixedValues := ⟨fun a b => funext fun i => isEmptyElim i⟩ exact Subsingleton.helim (congrArg (fun S => ValuesOn S (swigΩ Ω)) hf) _ _

theorem doObsKernelYMarginal_eq_ancestralMarginal_map (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) : doObsKernelYMarginal M X hObs hFix Y hY = (doObsKernelAncestralMarginal M X hObs hFix Y).map (valuesProjection (subset_fixObservedAncestralSet M X hObs hFix Y hY)) := by -- Name both inclusions with their *folded* types: the auto-generated proof -- inside `doObsKernelAncestralMarginal` records the unfolded intersection type, -- which blocks `rw` after `unfold` (defeq only at default transparency). have hJI : fixObservedAncestralSet M X hObs hFix Y ⊆ (M.fixSet X hObs hFix).observed := Finset.inter_subset_right have hKJ : Y ⊆ fixObservedAncestralSet M X hObs hFix Y := subset_fixObservedAncestralSet M X hObs hFix Y hY show (M.fixSet X hObs hFix).obsKernel.map (valuesProjection (hKJ.trans hJI)) = ((M.fixSet X hObs hFix).obsKernel.map (valuesProjection hJI)).map (valuesProjection hKJ) rw [← ProbabilityTheory.Kernel.map_comp_right _ (measurable_valuesProjection hJI) (measurable_valuesProjection hKJ), valuesProjection_comp hKJ hJI]

theorem doObsKernelYMarginal_heq_of_ancestralMarginal_heq (X : Finset N) (Y : Finset (SWIGNode N)) (M₁ M₂ : SCM N Ω) (hsg : M₁.toSWIGGraph = M₂.toSWIGGraph) (hObs₁ : ∀ D ∈ X, SWIGNode.random D ∈ M₁.observed) (hFix₁ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₁.fixed) (hObs₂ : ∀ D ∈ X, SWIGNode.random D ∈ M₂.observed) (hFix₂ : ∀ D ∈ X, SWIGNode.fixed D ∉ M₂.fixed) (hY₁ : Y ⊆ M₁.observed) (hY₂ : Y ⊆ M₂.observed) (hAnc : HEq (doObsKernelAncestralMarginal M₁ X hObs₁ hFix₁ Y) (doObsKernelAncestralMarginal M₂ X hObs₂ hFix₂ Y)) : HEq (doObsKernelYMarginal M₁ X hObs₁ hFix₁ Y hY₁) (doObsKernelYMarginal M₂ X hObs₂ hFix₂ Y hY₂) := by rw [doObsKernelYMarginal_eq_ancestralMarginal_map M₁ X hObs₁ hFix₁ Y hY₁, doObsKernelYMarginal_eq_ancestralMarginal_map M₂ X hObs₂ hFix₂ Y hY₂] obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases hsg apply heq_of_eq congr 1 exact eq_of_heq hAnc

theorem doObsKernelAncestralMarginal_dominated [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (s : (M.fixSet X hObs hFix).FixedValues) : doObsKernelAncestralMarginal M X hObs hFix Y s ≪ jointRef ref (fixObservedAncestralSet M X hObs hFix Y) := by exact absolutelyContinuous_jointRef_of_faithful ref href (fixObservedAncestralSet M X hObs hFix Y) (doObsKernelAncestralMarginal M X hObs hFix Y s)

theorem doObsKernelAncestralMarginal_heq_of_obsDensity_heq [∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (_hID : idSucceeds X Y G) (M₁ M₂ : SCM N Ω) (_hsg₁ : M₁.toSWIGGraph = G) (_hsg₂ : M₂.toSWIGGraph = G) (_hdom₁ : DominatedObs M₁ ref) (_hdom₂ : DominatedObs M₂ ref) (hpos₁ : DiscreteID.DiscretePositive M₁) (hpos₂ : DiscreteID.DiscretePositive M₂) (_hden : HEq (M₁.obsDensity ref) (M₂.obsDensity ref)) (hvalid₁ : interventionalQueryValid X Y M₁) (hvalid₂ : interventionalQueryValid X Y M₂) : HEq (doObsKernelAncestralMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y) (doObsKernelAncestralMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y) := by classical have hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y := by rcases _hID with ⟨_, hIDrest⟩ exact hIDrest.2.1 have hobs : HEq M₁.obsKernel M₂.obsKernel := obsKernel_heq_of_obsDensity_heq M₁ M₂ ref (_hsg₁.trans _hsg₂.symm) _hdom₁ _hdom₂ _hden have hsg : M₁.toSWIGGraph = M₂.toSWIGGraph := _hsg₁.trans _hsg₂.symm -- Materialize the marginals' finiteness as local instances while the models are -- still named; they survive the structural `obtain` below, where the global -- instance no longer matches the constructor form. haveI hfin1 : ∀ s, IsFiniteMeasure ((doObsKernelAncestralMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y) s) := fun s => inferInstance haveI hfin2 : ∀ s, IsFiniteMeasure ((doObsKernelAncestralMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y) s) := fun s => inferInstance haveI hobsfin1 : ∀ s, IsFiniteMeasure (M₁.obsKernel s) := fun s => inferInstance haveI hobsfin2 : ∀ s, IsFiniteMeasure (M₂.obsKernel s) := fun s => inferInstance obtain ⟨⟨dag₁, fixed₁, observed₁, unobserved₁, fio₁, oi₁, od₁, oou₁, foi₁, fou₁, aic₁, dc₁, foff₁, aco₁⟩, eT₁, iota₁, sf₁, mf₁, lD₁, pL₁⟩ := M₁ obtain ⟨⟨dag₂, fixed₂, observed₂, unobserved₂, fio₂, oi₂, od₂, oou₂, foi₂, fou₂, aic₂, dc₂, foff₂, aco₂⟩, eT₂, iota₂, sf₂, mf₂, lD₂, pL₂⟩ := M₂ cases hsg have hfio : fio₂ = fio₁ := Subsingleton.elim _ _ subst fio₂ have hoi : oi₂ = oi₁ := Subsingleton.elim _ _ subst oi₂ have hod : od₂ = od₁ := Subsingleton.elim _ _ subst od₂ have hoou : oou₂ = oou₁ := Subsingleton.elim _ _ subst oou₂ have hfoi : foi₂ = foi₁ := Subsingleton.elim _ _ subst foi₂ have hfou : fou₂ = fou₁ := Subsingleton.elim _ _ subst fou₂ have haic : aic₂ = aic₁ := Subsingleton.elim _ _ subst aic₂ have hdc : dc₂ = dc₁ := Subsingleton.elim _ _ subst dc₂ have hfoff : foff₂ = foff₁ := Subsingleton.elim _ _ subst foff₂ have haco : aco₂ = aco₁ := Subsingleton.elim _ _ subst aco₂ apply heq_of_eq refine ProbabilityTheory.Kernel.ext (fun s => ?_) -- `s` is typed against the *first* model's fixed-value space, so the `∀ s` -- instances above are only usable after one application at default -- transparency; instance synthesis alone cannot bridge the two (definitionally -- equal) fixed-value types. Specialize them here so the shapes match -- syntactically at every later call site. haveI hfin1s := hfin1 s haveI hfin2s := hfin2 s -- The two ancestral marginals share the coordinate reference `jointRef ref D` -- (`D = fixObservedAncestralSet` reads only the shared SWIG graph, so the two -- syntactic copies are definitionally equal), and both are dominated by it -- (`doObsKernelAncestralMarginal_dominated`). A measure is determined by its -- density against a fixed reference (`Measure.eq_of_rnDeriv_eq`), so it suffices -- to show the two Radon–Nikodym derivatives agree a.e. Applying the lemma as a -- term (not by `rw`) lets unification absorb the definitional `D₁ = D₂` gap that -- previously made the rewrite route brittle. refine eq_of_rnDeriv_eq (doObsKernelAncestralMarginal_dominated _ X hvalid₁.1 hvalid₁.2.1 Y ref href s) (doObsKernelAncestralMarginal_dominated _ X hvalid₂.1 hvalid₂.2.1 Y ref href s) ?_ -- Remaining density (rnDeriv) transport. By the Tian wrapper each side's density -- is the product over the districts of `G_X[D]` of the district factors -- (`doObsKernelAncestralMarginal_tian_cfactorization_density`); by T2 each district -- factor equals a recovered full-graph c-factor -- (`doAncestralDistrictDensity_recovered_from_obs`); and equal observational kernels -- give equal recovered factors (`cComponentDensityFactor_heq_of_obsKernel_heq`), -- so the two products — hence the two densities — agree a.e. have w1 := doObsKernelAncestralMarginal_tian_cfactorization_density _ X hvalid₁.1 hvalid₁.2.1 Y ref s (doObsKernelAncestralMarginal_dominated _ X hvalid₁.1 hvalid₁.2.1 Y ref href s) have w2 := doObsKernelAncestralMarginal_tian_cfactorization_density _ X hvalid₂.1 hvalid₂.2.1 Y ref s (doObsKernelAncestralMarginal_dominated _ X hvalid₂.1 hvalid₂.2.1 Y ref href s) refine w1.trans (Filter.EventuallyEq.trans ?_ w2.symm) let M₁' : SCM N Ω := { dag := dag₁, fixed := fixed₁, observed := observed₁, unobserved := unobserved₁, fixed_is_fixed := fio₁, observed_is_random := oi₁, unobserved_is_random := od₁, obs_unobs_disjoint := oou₁, dag_edges_classified := foi₁, fixed_image_in_observed := fou₁, fixed_are_roots := aic₁, unobs_are_roots := dc₁, fixed_outside_fixed_isolated := foff₁, all_children_in_observed := aco₁, edgeTypes := eT₁, iota_valueSpace := iota₁, structFun := sf₁, structFun_measurable := mf₁, latentDist := lD₁, isProbability_latent := pL₁ } let M₂' : SCM N Ω := { dag := dag₁, fixed := fixed₁, observed := observed₁, unobserved := unobserved₁, fixed_is_fixed := fio₁, observed_is_random := oi₁, unobserved_is_random := od₁, obs_unobs_disjoint := oou₁, dag_edges_classified := foi₁, fixed_image_in_observed := fou₁, fixed_are_roots := aic₁, unobs_are_roots := dc₁, fixed_outside_fixed_isolated := foff₁, all_children_in_observed := aco₁, edgeTypes := eT₂, iota_valueSpace := iota₂, structFun := sf₂, structFun_measurable := mf₂, latentDist := lD₂, isProbability_latent := pL₂ } let D := fixObservedAncestralSet M₁' X hvalid₁.1 hvalid₁.2.1 Y let H := (M₁'.fixSet X hvalid₁.1 hvalid₁.2.1).toSWIGGraph.induce (fixAncestralSet M₁' X hvalid₁.1 hvalid₁.2.1 Y) haveI hν₁ : IsFiniteMeasure ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) := hfin1 s haveI hν₂ : IsFiniteMeasure ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) := hfin2 s haveI hν₂D : IsFiniteMeasure (show Measure (ValuesOn D (swigΩ Ω)) from ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s)) := by change IsFiniteMeasure ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) exact hfin2 s change (fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S x) =ᵐ[jointRef ref D] (fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S x) have hfac : ∀ S ∈ H.cComponentSet, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S =ᵐ[jointRef ref D] tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S := by intro S hS have hIDM : idSucceeds X Y M₁'.toSWIGGraph := by rw [_hsg₁] exact _hID rcases hIDM with ⟨hX, hIDrest⟩ have hSreach : S ∈ ((M₁'.toSWIGGraph.splitMono X hX.1 hX.2).induce ((M₁'.toSWIGGraph.splitMono X hX.1 hX.2).dag.ancestralSet Y)).cComponentSet := by exact hS let C := containingCComponent M₁'.toSWIGGraph S have hReach : cFactorReachable M₁'.toSWIGGraph C S := by simpa [C] using hIDrest.2.2 S hSreach have hCmem : C ∈ M₁'.toSWIGGraph.cComponentSet := by have hSne : S.Nonempty := hReach.1 have hSobs : S ⊆ M₁'.toSWIGGraph.observed := M₁'.toSWIGGraph.cComponentSet_subset_observed S hReach.2.2 have hchoose : hSne.choose ∈ M₁'.toSWIGGraph.observed := hSobs hSne.choose_spec simp only [C, containingCComponent, dif_pos hSne, SWIGGraph.cComponentSet] exact Finset.mem_image.mpr ⟨hSne.choose, hchoose, rfl⟩ let extend : ValuesOn D (swigΩ Ω) → ValuesOn M₁'.observed (swigΩ Ω) := pinnedExtend M₁' X hvalid₁.1 hvalid₁.2.1 Y s have hExtend : ∀ xD, valuesProjection (show D ⊆ M₁'.observed from inter_subset_right) (extend xD) = xD := pinnedExtend_projection_eq M₁' X hvalid₁.1 hvalid₁.2.1 Y s hYX have hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hvalid₁.1 D hD⟩ = s ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩ := pinnedExtend_pin_eq M₁' X hvalid₁.1 hvalid₁.2.1 Y s have hpos₁' : ∀ s' : M₁'.FixedValues, DiscreteID.PositiveMass (M₁'.obsKernel s') := hpos₁ have hpos₂' : ∀ s' : M₂'.FixedValues, DiscreteID.PositiveMass (M₂'.obsKernel s') := hpos₂ haveI hobsfin₁ : ∀ s' : M₁'.FixedValues, IsFiniteMeasure (M₁'.obsKernel s') := hobsfin1 haveI hobsfin₂ : ∀ s' : M₂'.FixedValues, IsFiniteMeasure (M₂'.obsKernel s') := hobsfin2 have t1 := doAncestralDistrictDensity_recovered_from_obs M₁' X hvalid₁.2.2.2 hvalid₁.1 hvalid₁.2.1 Y ref href s S C (by simpa [H, fixTruncCComponentSet] using hS) hReach hCmem hpos₁' hYX extend hExtend hExtendX have t2 := doAncestralDistrictDensity_recovered_from_obs M₂' X hvalid₂.2.2.2 hvalid₂.1 hvalid₂.2.1 Y ref href s S C (by exact hS) (by simpa [M₁', M₂'] using hReach) (by simpa [M₁', M₂'] using hCmem) hpos₂' hYX extend (by exact hExtend) (by exact hExtendX) have hrec := cComponentDensityFactor_heq_of_obsKernel_heq M₁' M₂' ref C rfl hobs have hrec_fun : (fun s' => M₁'.cComponentDensityFactor ref s' C) = (fun s' => M₂'.cComponentDensityFactor ref s' C) := eq_of_heq hrec have hrec_s := congrFun hrec_fun (M₁'.fixSetProj X hvalid₁.1 hvalid₁.2.1 s) refine t1.trans ?_ filter_upwards [t2.symm] with x hx exact hrec_s ▸ hx clear w1 w2 have hprod : ∀ I : Finset (Finset (SWIGNode N)), (∀ S ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S =ᵐ[jointRef ref D] tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S) → (fun x => ∏ S ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₁' X hvalid₁.1 hvalid₁.2.1 Y) s) ref S x) =ᵐ[jointRef ref D] (fun x => ∏ S ∈ I, tianDistrictDensity H D ((doObsKernelAncestralMarginal M₂' X hvalid₂.1 hvalid₂.2.1 Y) s) ref S x) := by intro I hIall induction I using Finset.induction_on with | empty => -- … truncated; follow the source link for the rest …

theorem doObsKernelYMarginal_heq_of_obsDensity_heq [∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (_hID : idSucceeds X Y G) (M₁ M₂ : SCM N Ω) (_hsg₁ : M₁.toSWIGGraph = G) (_hsg₂ : M₂.toSWIGGraph = G) (_hdom₁ : DominatedObs M₁ ref) (_hdom₂ : DominatedObs M₂ ref) (hpos₁ : DiscreteID.DiscretePositive M₁) (hpos₂ : DiscreteID.DiscretePositive M₂) (_hden : HEq (M₁.obsDensity ref) (M₂.obsDensity ref)) (hvalid₁ : interventionalQueryValid X Y M₁) (hvalid₂ : interventionalQueryValid X Y M₂) : HEq (doObsKernelYMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1) (doObsKernelYMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1) := by -- Split off the easy `Y ← (Ystar ∩ observed)` projection; the genuine content -- is the observed-ancestral marginal identification. have hsg : M₁.toSWIGGraph = M₂.toSWIGGraph := _hsg₁.trans _hsg₂.symm exact doObsKernelYMarginal_heq_of_ancestralMarginal_heq X Y M₁ M₂ hsg hvalid₁.1 hvalid₁.2.1 hvalid₂.1 hvalid₂.2.1 hvalid₁.2.2.1 hvalid₂.2.2.1 (doObsKernelAncestralMarginal_heq_of_obsDensity_heq X Y G ref href _hID M₁ M₂ _hsg₁ _hsg₂ _hdom₁ _hdom₂ hpos₁ hpos₂ _hden hvalid₁ hvalid₂)

theorem doObsKernelYMarginal_heq_of_obsKernel_heq [∀ n, StandardBorelSpace (Ω n)] [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (X : Finset N) (Y : Finset (SWIGNode N)) (G : SWIGGraph N) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (hID : idSucceeds X Y G) (M₁ M₂ : SCM N Ω) (hsg₁ : M₁.toSWIGGraph = G) (hsg₂ : M₂.toSWIGGraph = G) (hdom₁ : DominatedObs M₁ ref) (hdom₂ : DominatedObs M₂ ref) (hpos₁ : DiscreteID.DiscretePositive M₁) (hpos₂ : DiscreteID.DiscretePositive M₂) (hobs : HEq M₁.obsKernel M₂.obsKernel) (hvalid₁ : interventionalQueryValid X Y M₁) (hvalid₂ : interventionalQueryValid X Y M₂) : HEq (doObsKernelYMarginal M₁ X hvalid₁.1 hvalid₁.2.1 Y hvalid₁.2.2.1) (doObsKernelYMarginal M₂ X hvalid₂.1 hvalid₂.2.1 Y hvalid₂.2.2.1) := -- The observational law enters the do-law `Y`-marginal *only* through its -- density: equal `obsKernel` gives equal `obsDensity` (`obsDensity_heq_of_obsKernel_heq`), -- and the g-formula core consumes that density. doObsKernelYMarginal_heq_of_obsDensity_heq X Y G ref href hID M₁ M₂ hsg₁ hsg₂ hdom₁ hdom₂ hpos₁ hpos₂ (obsDensity_heq_of_obsKernel_heq M₁ M₂ ref (hsg₁.trans hsg₂.symm) hobs) hvalid₁ hvalid₂