SCM.ID.Graphical­Thms.Do­GFormula­Tian

lemma coe_valuesEquivOfEq {M : Type*} {I J : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)] (h : I = J) : (⇑(valuesEquivOfEq (Ω := Ω') h) : ValuesOn I Ω' → ValuesOn J Ω') = valuesProjection (le_of_eq h.symm) := rfl

@[fun_prop] 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 (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 (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 [Finset.mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D k ⟨i, hicard⟩] exact hik) (valuesProjection (prefixIn_mono H D (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 [Finset.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 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 [Finset.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 [Finset.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 [Finset.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 (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 [Finset.mem_singleton] at hv subst hv rw [nodesAt_mem_prefixIn_iff H D (k + 1) ⟨k, hkc⟩] exact 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)]