SCM.Factored

theorem measurable_observedPrefixValue (M : SCM N Ω) : ∀ {n : ℕ} (hn : n ≤ M.observed.card) (i : Fin n), Measurable (fun ξ : M.ObservedPrefixValues n hn => M.observedPrefixValue hn ξ i) | 0, _, i => Fin.elim0 i | k + 1, hn, i => Fin.lastCases (by have h : Measurable (fun ξ : M.ObservedPrefixValues k (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨k, hn⟩).val => ξ.2) := measurable_snd simp only [SCM.observedPrefixValue, Fin.lastCases_last] exact h) (fun j => by have h : Measurable (fun ξ : M.ObservedPrefixValues k (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨k, hn⟩).val => M.observedPrefixValue (le_of_succ_le hn) ξ.1 j) := (M.measurable_observedPrefixValue (le_of_succ_le hn) j).comp measurable_fst simp only [SCM.observedPrefixValue, Fin.lastCases_castSucc] exact h) i

theorem partialEvalMap_latent (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) : ∀ (n : ℕ) (hn : n ≤ M.observed.card), (M.partialEvalMap n hn s ℓ).1 = ℓ | 0, _ => rfl | k + 1, hn => by -- Unfold one step and reduce `extendOrderedLatentPrefix`. have ih := M.partialEvalMap_latent s ℓ k (le_of_succ_le hn) -- `partialEvalMap (k+1) hn s ℓ = extendOrderedLatentPrefix hn (prev, stepFun hn (s, prev))`. -- `extendOrderedLatentPrefix hn ((ℓ', ξ), y) = (ℓ', (ξ, y))`, so `.1 = prev.1 = ℓ` by IH. change (M.extendOrderedLatentPrefix hn (M.partialEvalMap k (le_of_succ_le hn) s ℓ, M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ))).1 = ℓ -- By definition of `extendOrderedLatentPrefix` on `((ℓ', ξ), y)`. set prev := M.partialEvalMap k (le_of_succ_le hn) s ℓ with hprev rcases hprev_eq : prev with ⟨ℓ', ξ⟩ have : ℓ' = ℓ := by have : prev.1 = ℓ := ih rw [hprev_eq] at this exact this subst this rfl

theorem measurable_partialEvalMap (M : SCM N Ω) : ∀ (n : ℕ) (hn : n ≤ M.observed.card), Measurable (fun sℓ : FixedValues M × LatentValues M => M.partialEvalMap n hn sℓ.1 sℓ.2) | 0, _ => by -- `partialEvalMap 0 _ s ℓ = (ℓ, PUnit.unit)`. change Measurable (fun sℓ : FixedValues M × LatentValues M => (sℓ.2, (PUnit.unit : PUnit.{uΩ + 1}))) exact prodMk measurable_snd measurable_const | k + 1, hn => by have ih := M.measurable_partialEvalMap k (le_of_succ_le hn) -- Build the pair `(prev, stepFun hn (s, prev))`, then apply -- `extendOrderedLatentPrefix hn`. have hpair : Measurable (fun sℓ : FixedValues M × LatentValues M => (M.partialEvalMap k (le_of_succ_le hn) sℓ.1 sℓ.2, M.stepFun hn (sℓ.1, M.partialEvalMap k (le_of_succ_le hn) sℓ.1 sℓ.2))) := by refine prodMk ih ?_ refine (M.measurable_stepFun hn).comp ?_ exact prodMk measurable_fst ih exact (M.measurable_extendOrderedLatentPrefix hn).comp hpair

lemma compProd_deterministic_apply {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (κ : Kernel α β) [IsSFiniteKernel κ] {f : α × β → γ} (hf : Measurable f) (a : α) : (κ ⊗ₖ deterministic f hf) a = (κ a).map (fun b => (b, f (a, b))) := by have hpair : Measurable (fun b : β => (b, f (a, b))) := prodMk measurable_id (hf.comp (prodMk measurable_const measurable_id)) refine MeasureTheory.Measure.ext fun A hA => ?_ rw [ProbabilityTheory.Kernel.compProd_apply hA, MeasureTheory.Measure.map_apply hpair hA] simp only [ProbabilityTheory.Kernel.deterministic_apply] trans (∫⁻ b, indicator ((fun b => (b, f (a, b))) ⁻¹' A) (fun _ => (1 : ENNReal)) b ∂(κ a)) · apply MeasureTheory.lintegral_congr intro b have hSlice : MeasurableSet (Prod.mk b ⁻¹' A) := measurable_prodMk_left hA rw [MeasureTheory.Measure.dirac_apply' _ hSlice] simp only [indicator, Set.mem_preimage, Pi.one_apply] rfl · exact MeasureTheory.lintegral_indicator_one (hpair hA)

lemma observedPrefixValue_succ_last (M : SCM N Ω) {k : ℕ} (hn : k + 1 ≤ M.observed.card) (ξ : M.ObservedPrefixValues k (le_of_succ_le hn)) (y : swigΩ Ω (M.observedAt ⟨k, hn⟩).val) : M.observedPrefixValue hn ((ξ, y) : M.ObservedPrefixValues (k + 1) hn) (last k) = y := by simp [observedPrefixValue, Fin.lastCases_last]

lemma observedPrefixValue_succ_castSucc (M : SCM N Ω) {k : ℕ} (hn : k + 1 ≤ M.observed.card) (ξ : M.ObservedPrefixValues k (le_of_succ_le hn)) (y : swigΩ Ω (M.observedAt ⟨k, hn⟩).val) (j : Fin k) : M.observedPrefixValue hn ((ξ, y) : M.ObservedPrefixValues (k + 1) hn) j.castSucc = M.observedPrefixValue (le_of_succ_le hn) ξ j := by simp [observedPrefixValue, Fin.lastCases_castSucc]

lemma partialEvalMap_succ_snd_fst (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) {k : ℕ} (hn : k + 1 ≤ M.observed.card) : ((M.partialEvalMap (k + 1) hn s ℓ).2 : M.ObservedPrefixValues (k + 1) hn).1 = (M.partialEvalMap k (le_of_succ_le hn) s ℓ).2 := by rfl

lemma partialEvalMap_succ_snd_snd (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) {k : ℕ} (hn : k + 1 ≤ M.observed.card) : ((M.partialEvalMap (k + 1) hn s ℓ).2 : M.ObservedPrefixValues (k + 1) hn).2 = M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ) := by rfl

theorem partialEvalMap_observedPrefixValue (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) : ∀ (n : ℕ) (hn : n ≤ M.observed.card) (i : Fin n), M.observedPrefixValue hn (M.partialEvalMap n hn s ℓ).2 i = M.evalObservedAux s ℓ i.val (lt_of_lt_of_le i.isLt hn) | 0, _, i => Fin.elim0 i | k + 1, hn, i => by refine Fin.lastCases ?_ ?_ i · -- Last slot: i = last k. LHS reduces to stepFun; RHS is evalObservedAux at k. -- Step 1: unfold `(partialEvalMap (k+1) hn s ℓ).2` as a pair. change M.observedPrefixValue hn ((M.partialEvalMap k (le_of_succ_le hn) s ℓ).2, M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ)) (last k) = _ -- Step 2: pick the `y` slot. rw [observedPrefixValue_succ_last] -- Step 3: unfold `stepFun` and `evalObservedAux_eq` on the RHS. unfold stepFun rw [evalObservedAux_eq] -- Step 4: the `structFun` head matches (both at `⟨k, hn⟩`); reduce to parent-arg eq. congr 1 funext w -- Step 5: split by the parent class (fixed / unobserved / observed) on both sides. have hfix_disj_unobs : ∀ u : SWIGNode N, u ∈ M.unobserved → u ∉ M.fixed := by intro u hu hf obtain ⟨m, hm⟩ := M.fixed_is_fixed u hf obtain ⟨j, hj⟩ := M.unobserved_is_random u hu rw [hm] at hj; cases hj simp only [parentValuesFromPrefix] by_cases hfix : w.val ∈ M.fixed · -- Fixed parent branch. simp only [dif_pos hfix] have huo : w.val ∉ M.unobserved := fun hu => hfix_disj_unobs _ hu hfix exact (parentMap_fixed M s ℓ _ _ w hfix).symm · simp only [dif_neg hfix] by_cases hobs : w.val ∈ M.observed · -- Observed parent branch: use IH on smaller prefix index. simp only [dif_pos hobs] have huo : w.val ∉ M.unobserved := not_unobs_of_obs M.toSWIGGraph hobs -- IH at (k, iobs) where iobs points to the parent's observed index. have hedge : M.dag.edge w.val (M.observedAt ⟨k, hn⟩).val := M.dag.mem_parents.mp w.property have hlt : M.observedIndex ⟨w.val, hobs⟩ < (⟨k, hn⟩ : Fin M.observed.card) := M.observed_parent_index_lt hn hedge hobs have hlt' : (M.observedIndex ⟨w.val, hobs⟩).val < k := hlt have ih := partialEvalMap_observedPrefixValue M s ℓ k (le_of_succ_le hn) ⟨(M.observedIndex ⟨w.val, hobs⟩).val, hlt'⟩ -- Rewrite `observedPrefixValue` via IH, so both sides become -- `castEq ▸ evalObservedAux s ℓ idx _` for the same equality. rw [ih] refine trans ?_ (parentMap_observed M s ℓ _ _ w hobs).symm -- Both sides transport the evaluator result along the same node -- equality. have hNode : (M.observedAt (M.observedIndex ⟨w.val, hobs⟩)).val = w.val := M.observedAt_observedIndex ⟨w.val, hobs⟩ simp [eqRec_eq_cast] · -- Unobserved parent branch. have hunobs : w.val ∈ M.unobserved := by have hedge : M.dag.edge w.val (M.observedAt ⟨k, hn⟩).val := M.dag.mem_parents.mp w.property have hclass : w.val ∈ M.fixed ∪ M.observed ∪ M.unobserved := (M.dag_edges_classified _ _ hedge).1 rcases Finset.mem_union.mp hclass with h | h · rcases Finset.mem_union.mp h with h | h · exact (hfix h).elim · exact (hobs h).elim · exact h simp only [dif_neg hobs] -- LHS: `sℓξ.2.1 ⟨w.val, hunobs⟩` where `sℓξ = (s, partialEvalMap k _ s ℓ)`, -- so `.2.1 = (partialEvalMap k _ s ℓ).1 = ℓ`. rw [partialEvalMap_latent] exact (parentMap_unobserved M s ℓ _ _ w hunobs).symm · -- Earlier slots: i = j.castSucc. Apply IH on (k, j). intro j have ih := partialEvalMap_observedPrefixValue M s ℓ k (le_of_succ_le hn) j -- Unfold `(partialEvalMap (k+1) hn s ℓ).2` as the pair `(prev.2, stepFun _)`, -- then use `observedPrefixValue_succ_castSucc` to recurse into `prev.2`. change M.observedPrefixValue hn ((M.partialEvalMap k (le_of_succ_le hn) s ℓ).2, M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ)) j.castSucc = _ rw [observedPrefixValue_succ_castSucc] simpa using ih

theorem measurable_orderedLatentPrefixFullToRandom (M : SCM N Ω) : Measurable M.orderedLatentPrefixFullToRandom := by classical refine measurable_pi_lambda _ ?_ intro ⟨n, hn⟩ simp only [orderedLatentPrefixFullToRandom] by_cases hobs : n ∈ M.observed · simp [hobs] have hNode : (M.observedAt (M.observedIndex ⟨n, hobs⟩)).val = n := M.observedAt_observedIndex ⟨n, hobs⟩ have hmeas : Measurable fun p : M.OrderedLatentPrefixValues M.observed.card (le_refl _) => M.observedPrefixValue (le_refl _) p.2 (M.observedIndex ⟨n, hobs⟩) := (M.measurable_observedPrefixValue (le_refl _) (M.observedIndex ⟨n, hobs⟩)).comp (measurable_snd : Measurable snd) exact (measurable_cast_family hNode).comp hmeas · have hunobs : n ∈ M.unobserved := by rcases Finset.mem_union.mp hn with hobs' | hunobs · exact elim (hobs hobs') · exact hunobs simp [hobs] exact ((measurable_pi_apply (⟨n, hunobs⟩ : {x // x ∈ M.unobserved})).comp (measurable_fst : Measurable fst))

theorem partialEvalMap_full_eq (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) : M.orderedLatentPrefixFullToRandom (M.partialEvalMap M.observed.card (le_refl _) s ℓ) = M.evalMap s ℓ := by funext v unfold orderedLatentPrefixFullToRandom by_cases hobs : v.val ∈ M.observed · -- Observed branch: both sides are (cast) of `evalObservedAux` at -- `observedIndex v`. simp only [hobs, dif_pos] -- LHS: cast hEq (observedPrefixValue ((partialEvalMap ...).2) (observedIndex v)) rw [M.partialEvalMap_observedPrefixValue s ℓ M.observed.card (le_refl _) (M.observedIndex ⟨v.val, hobs⟩)] -- RHS: evalMap_observed form rw [M.evalMap_observed s ℓ v hobs] -- Both sides transport the same `evalObservedAux` along the identity -- `(M.observedAt (observedIndex v)).val = v.val`. LHS uses `cast -- (congrArg (swigΩ Ω) h)`, RHS uses `h ▸ _`; they agree by the generic -- identity `cast (congrArg f h) x = h ▸ x` (both `mpr`/`mp` when -- `h` is used as a motive transport). -/ have hNode : (M.observedAt (M.observedIndex ⟨v.val, hobs⟩)).val = v.val := M.observedAt_observedIndex ⟨v.val, hobs⟩ -- Abstract the transported value as `aux` with the exact shape expected -- on the RHS: the `▸` motive transports along `hNode : (observedAt idx).val = v.val`, -- so `aux` must have type `swigΩ Ω (observedAt (observedIndex v)).val`. let aux0 : swigΩ Ω (M.observedAt (M.observedIndex ⟨v.val, hobs⟩)).val := M.evalObservedAux s ℓ (M.observedIndex ⟨v.val, hobs⟩).val (lt_of_lt_of_le (M.observedIndex ⟨v.val, hobs⟩).isLt (le_refl _)) -- Goal: cast hEq aux0 = hNode ▸ aux0; both transports use the same node -- equality, so they're equal via `eqRec_eq_cast`. change cast _ aux0 = hNode ▸ aux0 exact (eqRec_eq_cast (motive := fun x _ => swigΩ Ω x) aux0 hNode).symm · -- Unobserved branch: LHS reads `p.1 ⟨v.val, huo⟩ = ℓ ⟨v.val, huo⟩` by -- `partialEvalMap_latent`; RHS is `ℓ ⟨v.val, huo⟩` by `evalMap_unobserved`. simp only [hobs, dif_neg, not_false_eq_true] have hunobs : v.val ∈ M.unobserved := by rcases Finset.mem_union.mp v.property with hobs' | hunobs · exact elim (hobs hobs') · exact hunobs rw [M.evalMap_unobserved s ℓ v hunobs] -- LHS: `(partialEvalMap M.observed.card _ s ℓ).1 ⟨v.val, hunobs⟩` -- By `partialEvalMap_latent`, `.1 = ℓ`. have := M.partialEvalMap_latent s ℓ M.observed.card (le_refl _) rw [this]

lemma mem_prefixNodes_iff (M : SCM N Ω) (n : ℕ) (v : SWIGNode N) : v ∈ M.prefixNodes n ↔ ∃ h : v ∈ M.observed, (M.observedIndex ⟨v, h⟩).val < n := by unfold prefixNodes constructor · intro hv rcases Finset.mem_filter.mp hv with ⟨hobs, hltif⟩ exact ⟨hobs, by simpa [hobs] using hltif⟩ · rintro ⟨hobs, hlt⟩ exact Finset.mem_filter.mpr ⟨hobs, by simpa [hobs] using hlt⟩

lemma prefixNodes_zero (M : SCM N Ω) : M.prefixNodes 0 = ∅ := by ext v constructor · intro hv rcases (M.mem_prefixNodes_iff 0 v).mp hv with ⟨_, hlt⟩ omega · simp

lemma observedAt_mem_prefixNodes_iff (M : SCM N Ω) (n : ℕ) (i : Fin M.observed.card) : (M.observedAt i).val ∈ M.prefixNodes n ↔ i.val < n := by rw [M.mem_prefixNodes_iff] constructor · rintro ⟨hobs, hlt⟩ have hidx : M.observedIndex ⟨(M.observedAt i).val, hobs⟩ = i := by have hsub : (⟨(M.observedAt i).val, hobs⟩ : {v // v ∈ M.observed}) = M.observedAt i := Subtype.ext rfl rw [hsub] exact M.observedIndex_observedAt i rwa [hidx] at hlt · intro hlt exact ⟨(M.observedAt i).property, by simpa [M.observedIndex_observedAt i] using hlt⟩

lemma prefixNodes_card (M : SCM N Ω) (n : ℕ) (hn : M.observed.card ≤ n) : M.prefixNodes n = M.observed := by ext v constructor · exact fun hv => M.prefixNodes_subset_observed _ hv · intro hv exact (M.mem_prefixNodes_iff n v).mpr ⟨hv, lt_of_lt_of_le (M.observedIndex ⟨v, hv⟩).isLt hn⟩

lemma observedAt_not_mem_prefixNodes (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : (M.observedAt ⟨n, hn⟩).val ∉ M.prefixNodes n := by rw [M.observedAt_mem_prefixNodes_iff n ⟨n, hn⟩] exact Nat.lt_irrefl n

lemma prefixNodes_succ (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : M.prefixNodes (n + 1) = M.prefixNodes n ∪ {(M.observedAt ⟨n, hn⟩).val} := by ext v constructor · intro hv rcases (M.mem_prefixNodes_iff (n + 1) v).mp hv with ⟨hobs, hlt⟩ by_cases hlt_n : (M.observedIndex ⟨v, hobs⟩).val < n · exact mem_union_left _ ((M.mem_prefixNodes_iff n v).mpr ⟨hobs, hlt_n⟩) · have hidx_val : (M.observedIndex ⟨v, hobs⟩).val = n := by omega have hidx : M.observedIndex ⟨v, hobs⟩ = ⟨n, hn⟩ := Fin.ext hidx_val have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by have hround := M.observedAt_observedIndex ⟨v, hobs⟩ rw [hidx] at hround exact hround.symm exact mem_union_right _ (by simp [hv_eq]) · intro hv rcases Finset.mem_union.mp hv with hvpre | hvlast · rcases (M.mem_prefixNodes_iff n v).mp hvpre with ⟨hobs, hlt⟩ exact (M.mem_prefixNodes_iff (n + 1) v).mpr ⟨hobs, by omega⟩ · have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hvlast subst hv_eq rw [M.observedAt_mem_prefixNodes_iff (n + 1) ⟨n, hn⟩] exact Nat.lt_succ_self n

lemma prefixNodes_disjoint_singleton_next (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : Disjoint (M.prefixNodes n) ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) := by rw [Finset.disjoint_singleton_right] exact M.observedAt_not_mem_prefixNodes hn

lemma observedPredecessors_observedAt (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : M.toSWIGGraph.observedPredecessors (M.observedAt ⟨n, hn⟩).val = M.prefixNodes n := by classical letI := M.topoLinearOrder ext w constructor · intro hw rcases Finset.mem_filter.mp hw with ⟨hwobs, htopo⟩ have hw_lt : (⟨w, hwobs⟩ : {v // v ∈ M.observed}) < M.observedAt ⟨n, hn⟩ := by change w < (M.observedAt ⟨n, hn⟩).val exact htopo have hidx : M.observedIndex ⟨w, hwobs⟩ < M.observedIndex (M.observedAt ⟨n, hn⟩) := (M.observed.orderIsoOfFin rfl).symm.strictMono hw_lt rw [M.observedIndex_observedAt] at hidx exact (M.mem_prefixNodes_iff n w).mpr ⟨hwobs, hidx⟩ · intro hw rcases (M.mem_prefixNodes_iff n w).mp hw with ⟨hwobs, hidx_lt⟩ refine Finset.mem_filter.mpr ⟨hwobs, ?_⟩ have hfin : M.observedIndex ⟨w, hwobs⟩ < ⟨n, hn⟩ := by exact Fin.mk_lt_mk.mpr hidx_lt have hw_lt : (⟨w, hwobs⟩ : {v // v ∈ M.observed}) < M.observedAt ⟨n, hn⟩ := by have hmono := (M.observed.orderIsoOfFin rfl).strictMono (show (M.observed.orderIsoOfFin rfl).symm ⟨w, hwobs⟩ < (⟨n, hn⟩ : Fin M.observed.card) from hfin) rw [OrderIso.apply_symm_apply] at hmono exact hmono change w < (M.observedAt ⟨n, hn⟩).val at hw_lt exact hw_lt

lemma measurable_singletonValue {ι : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)] {v : ι} : Measurable (singletonValue (α := α) (v := v)) := by unfold singletonValue exact measurable_pi_apply (⟨v, by simp⟩ : {w // w ∈ ({v} : Finset ι)})

lemma measurable_singletonValues {ι : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)] {v : ι} : Measurable (singletonValues (α := α) (v := v)) := by refine measurable_pi_iff.mpr ?_ rintro ⟨w, hw⟩ have h : w = v := by simpa using hw subst w change Measurable (id : α v → α v) exact measurable_id

@[simp] lemma singletonValue_singletonValues {ι : Type*} {α : ι → Type*} {v : ι} (x : α v) : singletonValue (α := α) (v := v) (singletonValues (α := α) (v := v) x) = x := by rfl

@[simp] lemma singletonValues_singletonValue {ι : Type*} {α : ι → Type*} {v : ι} (x : ValuesOn ({v} : Finset ι) α) : singletonValues (α := α) (v := v) (singletonValue (α := α) (v := v) x) = x := by ext ⟨w, hw⟩ have hwv : w = v := by simpa using hw subst w rfl

lemma obsStepCondKernel_map_singletonValues (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) [StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))] : (M.obsStepCondKernel hn).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val)) = M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n) := by refine ProbabilityTheory.Kernel.ext fun sc => ?_ unfold obsStepCondKernel rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValues (α := swigΩ Ω))] rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValue (α := swigΩ Ω))] rw [MeasureTheory.Measure.map_map (measurable_singletonValues (α := swigΩ Ω)) (measurable_singletonValue (α := swigΩ Ω))] have hcomp : (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val) ∘ singletonValue (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val)) = (id : ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) → ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) := by funext x exact singletonValues_singletonValue (α := swigΩ Ω) x rw [hcomp, MeasureTheory.Measure.map_id]

lemma obsStepCondKernel_sectR_map_singletonValues (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) [StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))] (s : M.FixedValues) : ((M.obsStepCondKernel hn).sectR s).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val)) = (M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n)).sectR s := by refine ProbabilityTheory.Kernel.ext fun c => ?_ unfold sectR rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValues (α := swigΩ Ω))] rw [ProbabilityTheory.Kernel.comap_apply] rw [ProbabilityTheory.Kernel.comap_apply] have h := congrArg (fun k => k (s, c)) (M.obsStepCondKernel_map_singletonValues hn) change ((M.obsStepCondKernel hn).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val))) (s, c) = M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n) (s, c) at h rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValues (α := swigΩ Ω))] at h exact h

lemma measurable_extendObsPrefix (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : Measurable (M.extendObsPrefix hn) := by unfold extendObsPrefix exact (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn).symm).measurable.comp ((measurable_valuesUnionMk (Ω := swigΩ Ω)).comp (prodMk measurable_fst ((measurable_singletonValues (α := swigΩ Ω)).comp measurable_snd)))

lemma prefixSucc_projection_pair (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : (fun ω : M.ObservedValues => valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn)) (valuesProjection (M.prefixNodes_subset_observed (n + 1)) ω))) = (fun ω : M.ObservedValues => (valuesProjection (M.prefixNodes_subset_observed n) ω, valuesProjection (by intro w hw have hw_eq : w = (M.observedAt ⟨n, hn⟩).val := by simpa using hw simp [hw_eq, (M.observedAt ⟨n, hn⟩).property]) ω)) := by funext ω ext i · rfl · rfl

lemma valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk {A B C : Finset (SWIGNode N)} (hDisj : Disjoint A B) (hUnion : C = A ∪ B) (p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω)) : valuesUnionEquiv (Ω := Ω) hDisj ((valuesEquivOfEq (Ω := swigΩ Ω) hUnion) ((valuesEquivOfEq (Ω := swigΩ Ω) hUnion).symm (valuesUnionMk p.1 p.2))) = p := by rw [(valuesEquivOfEq (Ω := swigΩ Ω) hUnion).apply_symm_apply] exact (valuesUnionEquiv (Ω := Ω) hDisj).right_inv p

lemma valuesUnionEquiv_extendObsPrefix (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) (p : ValuesOn (M.prefixNodes n) (swigΩ Ω) × swigΩ Ω (M.observedAt ⟨n, hn⟩).val) : valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn)) (M.extendObsPrefix hn p)) = (p.1, singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val) p.2) := by unfold extendObsPrefix exact valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk (M.prefixNodes_disjoint_singleton_next hn) (M.prefixNodes_succ hn) (p.1, singletonValues p.2)

lemma obsCondPairKernel_apply_eq_compProd (M : SCM N Ω) (Y CC : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hCC : CC ⊆ M.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [CountableOrCountablyGenerated M.FixedValues (ValuesOn CC (swigΩ Ω))] (s : M.FixedValues) : M.obsCondPairKernel Y CC hY hCC s = ((M.obsKernel s).map (valuesProjection hCC)) ⊗ₘ (M.obsCondKernel Y CC hY hCC).sectR s := by classical have hπCC : Measurable (valuesProjection (Ω := swigΩ Ω) hCC) := measurable_valuesProjection _ have hπY : Measurable (valuesProjection (Ω := swigΩ Ω) hY) := measurable_valuesProjection _ set κ : Kernel M.FixedValues (ValuesOn CC (swigΩ Ω) × ValuesOn Y (swigΩ Ω)) := M.obsCondPairKernel Y CC hY hCC with hκ_def haveI : IsMarkovKernel κ := by rw [hκ_def] unfold obsCondPairKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (hπCC.prodMk hπY) have hDisint : κ.fst ⊗ₖ M.obsCondKernel Y CC hY hCC = κ := by change κ.fst ⊗ₖ κ.condKernel = κ exact ProbabilityTheory.Kernel.disintegrate _ _ haveI : IsMarkovKernel (M.obsCondKernel Y CC hY hCC) := by unfold obsCondKernel infer_instance have hAt : (κ.fst s) ⊗ₘ (M.obsCondKernel Y CC hY hCC).sectR s = κ s := by have h := congrArg (fun k => k s) hDisint change (κ.fst ⊗ₖ M.obsCondKernel Y CC hY hCC) s = κ s at h rw [ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR] at h exact h have hFst : κ.fst s = (M.obsKernel s).map (valuesProjection hCC) := by rw [hκ_def] unfold obsCondPairKernel rw [ProbabilityTheory.Kernel.fst_map_prod _ hπY, ProbabilityTheory.Kernel.map_apply _ hπCC] rw [hκ_def, ← hAt, hFst]

theorem obsKernel_map_prefixNodes (M : SCM N Ω) (s : M.FixedValues) [∀ (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 : Fin M.observed.card, CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))] : ∀ (n : ℕ) (hn : n ≤ M.observed.card), (M.obsKernel s).map (valuesProjection (M.prefixNodes_subset_observed n)) = M.obsChainKernel n hn s := by intro n induction n with | zero => intro hn change (M.obsKernel s).map (valuesProjection (M.prefixNodes_subset_observed 0)) = M.obsChainKernelZero s unfold obsChainKernelZero rw [ProbabilityTheory.Kernel.const_apply] refine MeasureTheory.Measure.ext fun A hA => ?_ have hsub : Subsingleton (ValuesOn (M.prefixNodes 0) (swigΩ Ω)) := by refine ⟨fun f g => ?_⟩ funext ⟨w, hw⟩ have : w ∈ (∅ : Finset (SWIGNode N)) := by rw [M.prefixNodes_zero] at hw exact hw exact absurd this (notMem_empty _) by_cases hmem : M.emptyPrefixValues ∈ A · have hAuniv : A = univ := by ext x constructor · intro _; trivial · intro _ have hx : x = M.emptyPrefixValues := Subsingleton.elim _ _ simpa [hx] using hmem rw [hAuniv] rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection (M.prefixNodes_subset_observed 0)) MeasurableSet.univ] simp [M.obsKernel_apply_univ s] · have hAempty : A = ∅ := by ext x constructor · intro hx have hx0 : x = M.emptyPrefixValues := Subsingleton.elim _ _ exact (hmem (by simpa [hx0] using hx)).elim · intro hx exact elim hx rw [hAempty] simp | succ n ih => intro hn classical have hk : n < M.observed.card := Nat.lt_of_succ_le hn letI : CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω)) := inferInstanceAs (CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes (⟨n, hk⟩ : Fin _).val) (swigΩ Ω))) let Y : Finset (SWIGNode N) := {(M.observedAt ⟨n, hk⟩).val} let hY : Y ⊆ M.observed := by intro v hv have hv_eq : v = (M.observedAt ⟨n, hk⟩).val := by simpa [Y] using hv simp [hv_eq, (M.observedAt ⟨n, hk⟩).property] let hCC : M.prefixNodes n ⊆ M.observed := M.prefixNodes_subset_observed n let e : ValuesOn (M.prefixNodes (n + 1)) (swigΩ Ω) ≃ᵐ ValuesOn (M.prefixNodes n) (swigΩ Ω) × ValuesOn Y (swigΩ Ω) := (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk)).trans (valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hk)) refine e.map_measurableEquiv_injective ?_ have hIH := ih (le_of_succ_le hn) change map e (map (valuesProjection (M.prefixNodes_subset_observed (n + 1))) (M.obsKernel s)) = map e ((((M.obsChainKernel n (le_of_succ_le hn)) ⊗ₖ (M.obsStepCondKernel hk)).map (M.extendObsPrefix hk)) s) rw [ProbabilityTheory.Kernel.map_apply _ (M.measurable_extendObsPrefix hk)] rw [ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR] rw [← hIH] rw [MeasureTheory.Measure.map_map e.measurable (measurable_valuesProjection (M.prefixNodes_subset_observed (n + 1)))] rw [MeasureTheory.Measure.map_map e.measurable (M.measurable_extendObsPrefix hk)] have hleft_fun : e ∘ valuesProjection (M.prefixNodes_subset_observed (n + 1)) = (fun ω : M.ObservedValues => (valuesProjection (M.prefixNodes_subset_observed n) ω, valuesProjection hY ω)) := by change (fun ω : M.ObservedValues => valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hk) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk)) (valuesProjection (M.prefixNodes_subset_observed (n + 1)) ω))) = (fun ω : M.ObservedValues => (valuesProjection (M.prefixNodes_subset_observed n) ω, valuesProjection hY ω)) exact M.prefixSucc_projection_pair hk rw [hleft_fun] have hright_fun : e ∘ M.extendObsPrefix hk = (fun p : ValuesOn (M.prefixNodes n) (swigΩ Ω) × swigΩ Ω (M.observedAt ⟨n, hk⟩).val => (p.1, singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hk⟩).val) p.2)) := by funext p exact M.valuesUnionEquiv_extendObsPrefix hk p rw [hright_fun] change map (fun ω : M.ObservedValues => (valuesProjection hCC ω, valuesProjection hY ω)) (M.obsKernel s) = map (map id (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hk⟩).val))) (((M.obsKernel s).map (valuesProjection hCC)) ⊗ₘ (M.obsStepCondKernel hk).sectR s) rw [← MeasureTheory.Measure.compProd_map (μ := (M.obsKernel s).map (valuesProjection hCC)) (κ := (M.obsStepCondKernel hk).sectR s) (f := singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hk⟩).val)) (measurable_singletonValues (α := swigΩ Ω))] rw [M.obsStepCondKernel_sectR_map_singletonValues hk s] rw [← M.obsCondPairKernel_apply_eq_compProd Y (M.prefixNodes n) hY hCC s] unfold obsCondPairKernel rw [ProbabilityTheory.Kernel.map_apply _ ((measurable_valuesProjection hCC).prodMk (measurable_valuesProjection hY))]

theorem parent_unobserved_of_not_fixed_not_observed (G : SWIGGraph N) {u v : SWIGNode N} (hedge : G.dag.edge u v) (hfix : u ∉ G.fixed) (hobs : u ∉ G.observed) : u ∈ G.unobserved := by have hclass : u ∈ G.fixed ∪ G.observed ∪ G.unobserved := (G.dag_edges_classified _ _ hedge).1 rcases Finset.mem_union.mp hclass with h | h · rcases Finset.mem_union.mp h with h | h · exact (hfix h).elim · exact (hobs h).elim · exact h