Discovery.Invariant­Prediction.Helpers

theorem condDistrib_eq_mechanismKernel_of_indep {α β γ δ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] [StandardBorelSpace δ] [Nonempty δ] (μ : Measure α) [IsProbabilityMeasure μ] {X : α → β} {L : α → γ} {Y : α → δ} {Φ : β × γ → δ} (hX : Measurable X) (hL : Measurable L) (hY : Measurable Y) (hΦ : Measurable Φ) (hind : IndepFun L X μ) (hYeq : Y =ᵐ[μ] fun ω => Φ (X ω, L ω)) : (fun x => condDistrib Y X μ x) =ᵐ[μ.map X] mechanismKernel (μ.map L) Φ := by classical haveI : IsFiniteMeasure μ := inferInstance haveI : IsProbabilityMeasure (μ.map L) := Measure.isProbabilityMeasure_map hL.aemeasurable haveI : IsMarkovKernel (mechanismKernel (μ.map L) Φ) := instIsMarkovKernelMechanismKernel (μ.map L) hΦ have hXL : Measurable (fun ω => (X ω, L ω)) := hX.prodMk hL have hgraph : Measurable (fun p : β × γ => (p.1, Φ p)) := measurable_fst.prodMk hΦ have hprod : μ.map (fun ω => (X ω, L ω)) = (μ.map X).prod (μ.map L) := (indepFun_iff_map_prod_eq_prod_map_map hX.aemeasurable hL.aemeasurable).mp hind.symm have hpair_congr : (fun ω => (X ω, Y ω)) =ᵐ[μ] fun ω => (X ω, Φ (X ω, L ω)) := by filter_upwards [hYeq] with ω hω rw [hω] refine condDistrib_ae_eq_of_measure_eq_compProd X hY.aemeasurable ?_ calc μ.map (fun ω => (X ω, Y ω)) = μ.map (fun ω => (X ω, Φ (X ω, L ω))) := Measure.map_congr hpair_congr _ = Measure.map (fun p : β × γ => (p.1, Φ p)) (μ.map (fun ω => (X ω, L ω))) := by rw [Measure.map_map hgraph hXL] rfl _ = Measure.map (fun p : β × γ => (p.1, Φ p)) ((μ.map X).prod (μ.map L)) := by rw [hprod] _ = (μ.map X).compProd (mechanismKernel (μ.map L) Φ) := map_graph_prod_eq_compProd (μ.map X) (μ.map L) hΦ

theorem condDistrib_target_eq_mechanismKernel (F : EnvFamily N Ω ι) (i₀ i : ι) : (by classical haveI : StandardBorelSpace (ValuesOn ({F.yNode} : Finset (SWIGNode N)) (swigΩ Ω)) := F.borelTarget haveI : Nonempty (ValuesOn ({F.yNode} : Finset (SWIGNode N)) (swigΩ Ω)) := F.neTarget let hYrv : ({F.yNode} : Finset (SWIGNode N)) ⊆ (F.M i).randomVars := by intro w hw rw [mem_singleton] at hw subst hw exact mem_union_left _ (F.hYobs i) let hPrv : F.paObs i₀ ⊆ (F.M i).randomVars := by rw [F.paObs_eq i₀ i] exact (inter_subset_right).trans (by change (F.M i).observed ⊆ (F.M i).observed ∪ (F.M i).unobserved exact subset_union_left) let hLrv : F.paLat i ⊆ (F.M i).randomVars := by exact (inter_subset_right).trans (by change (F.M i).unobserved ⊆ (F.M i).observed ∪ (F.M i).unobserved exact subset_union_right) exact (fun c => condDistrib (valuesProjection hYrv) (valuesProjection hPrv) ((F.M i).jointKernel (F.s i)) c) =ᵐ[((F.M i).jointKernel (F.s i)).map (valuesProjection hPrv)] mechanismKernel (((F.M i).jointKernel (F.s i)).map (valuesProjection hLrv)) (F.mechanismFun i₀ i)) := by classical dsimp only haveI : StandardBorelSpace (ValuesOn ({F.yNode} : Finset (SWIGNode N)) (swigΩ Ω)) := F.borelTarget haveI : Nonempty (ValuesOn ({F.yNode} : Finset (SWIGNode N)) (swigΩ Ω)) := F.neTarget have hYrv : ({F.yNode} : Finset (SWIGNode N)) ⊆ (F.M i).randomVars := by intro w hw rw [mem_singleton] at hw subst hw exact mem_union_left _ (F.hYobs i) have hPrv : F.paObs i₀ ⊆ (F.M i).randomVars := by rw [F.paObs_eq i₀ i] exact (inter_subset_right).trans (by change (F.M i).observed ⊆ (F.M i).observed ∪ (F.M i).unobserved exact subset_union_left) have hLrv : F.paLat i ⊆ (F.M i).randomVars := by exact (inter_subset_right).trans (by show (F.M i).unobserved ⊆ (F.M i).observed ∪ (F.M i).unobserved exact subset_union_right) have hObsExo : (F.M i).dag.parents F.yNode ∩ (F.M i).observed ⊆ (F.M i).randomVars := (inter_subset_right).trans (by show (F.M i).observed ⊆ (F.M i).observed ∪ (F.M i).unobserved exact subset_union_left) have hLatExo : (F.M i).dag.parents F.yNode ∩ (F.M i).unobserved ⊆ (F.M i).randomVars := (inter_subset_right).trans (by show (F.M i).unobserved ⊆ (F.M i).observed ∪ (F.M i).unobserved exact subset_union_right) let e := valuesEquivOfEq (Ω := swigΩ Ω) (F.paObs_eq i i₀) have hOcomp : e ∘ (valuesProjection hObsExo : (F.M i).RandomValues → ValuesOn (F.paObs i) (swigΩ Ω)) = (valuesProjection hPrv : (F.M i).RandomValues → ValuesOn (F.paObs i₀) (swigΩ Ω)) := by funext ξ x rfl have hind : IndepFun (valuesProjection hLrv) (valuesProjection hPrv) ((F.M i).jointKernel (F.s i)) := by have h0 := (F.hExo i).comp (φ := id) (ψ := e) measurable_id e.measurable change IndepFun (id ∘ valuesProjection hLatExo) (e ∘ valuesProjection hObsExo) ((F.M i).jointKernel (F.s i)) at h0 rw [hOcomp] at h0 exact h0 have hEvalMeas : Measurable (fun ℓ : (F.M i).LatentValues => (F.M i).evalMap (F.s i) ℓ) := by have : (fun ℓ : (F.M i).LatentValues => (F.M i).evalMap (F.s i) ℓ) = fun ℓ => uncurry (F.M i).evalMap (F.s i, ℓ) := rfl rw [this] exact (F.M i).evalMap_measurable.comp (prodMk measurable_const measurable_id) have hpair : ((F.M i).jointKernel (F.s i)).map (fun ω => (valuesProjection hPrv ω, valuesProjection hYrv ω)) = ((F.M i).jointKernel (F.s i)).map (fun ω => (valuesProjection hPrv ω, F.mechanismFun i₀ i (valuesProjection hPrv ω, valuesProjection hLrv ω))) := by rw [SCM.jointKernel_apply_eq] rw [Measure.map_map ((measurable_valuesProjection hPrv).prodMk (measurable_valuesProjection hYrv)) hEvalMeas] have hRightMeas : Measurable (fun ω => (valuesProjection hPrv ω, F.mechanismFun i₀ i (valuesProjection hPrv ω, valuesProjection hLrv ω))) := (measurable_valuesProjection hPrv).prodMk ((F.measurable_mechanismFun i₀ i).comp ((measurable_valuesProjection hPrv).prodMk (measurable_valuesProjection hLrv))) rw [Measure.map_map hRightMeas hEvalMeas] congr 1 funext ℓ dsimp rw [F.target_projection_evalMap_eq_mechanismFun i₀ i ℓ] exact condDistrib_eq_mechanismKernel_of_indep_of_pair_map ((F.M i).jointKernel (F.s i)) (measurable_valuesProjection hPrv) (measurable_valuesProjection hLrv) (measurable_valuesProjection hYrv) (F.measurable_mechanismFun i₀ i) hind hpair

theorem mechanismKernel_cf_env_eq (F : EnvFamily N Ω ι) (i₀ i j : ι) (cf : ValuesOn (F.paFix i) (swigΩ Ω)) (hLrv : F.paLat i ⊆ (F.M i).randomVars) (hLrv' : F.paLat j ⊆ (F.M j).randomVars) : mechanismKernel (((F.M i).jointKernel (F.s i)).map (valuesProjection hLrv)) (F.mechanismFunCf i₀ i cf) = mechanismKernel (((F.M j).jointKernel (F.s j)).map (valuesProjection hLrv')) (F.mechanismFunCf i₀ j (valuesProjection (le_of_eq (F.paFix_eq j i)) cf)) := by classical apply ProbabilityTheory.Kernel.ext intro o rw [mechanismKernel_apply _ (F.measurable_mechanismFunCf i₀ i cf) o, mechanismKernel_apply _ (F.measurable_mechanismFunCf i₀ j _) o] let hLun : F.paLat i ⊆ (F.M i).unobserved := Finset.inter_subset_right let hLun' : F.paLat j ⊆ (F.M j).unobserved := Finset.inter_subset_right rw [F.jointKernel_map_paLat_eq_latentProduct_map i hLrv hLun, F.jointKernel_map_paLat_eq_latentProduct_map j hLrv' hLun'] have hSliceMeas : Measurable (fun l : ValuesOn (F.paLat i) (swigΩ Ω) => F.mechanismFunCf i₀ i cf (o, l)) := (F.measurable_mechanismFunCf i₀ i cf).comp (prodMk measurable_const measurable_id) have hSliceMeas' : Measurable (fun l : ValuesOn (F.paLat j) (swigΩ Ω) => F.mechanismFunCf i₀ j (valuesProjection (le_of_eq (F.paFix_eq j i)) cf) (o, l)) := (F.measurable_mechanismFunCf i₀ j _).comp (prodMk measurable_const measurable_id) rw [Measure.map_map hSliceMeas (measurable_valuesProjection hLun), Measure.map_map hSliceMeas' (measurable_valuesProjection hLun')] exact map_heq_transport (congrArg (fun S => ValuesOn S (swigΩ Ω)) (F.hUnobs i j)) (F.latentValues_measurableSpace_heq i j) (F.latentProduct_heq i j) <| by apply Function.hfunext (congrArg (fun S => ValuesOn S (swigΩ Ω)) (F.hUnobs i j)) intro l l' hl apply heq_of_eq funext w rcases w with ⟨w, hw⟩ have hwy : w = F.yNode := Finset.mem_singleton.mp hw subst hwy simp only [Function.comp_apply] unfold mechanismFunCf simp only apply F.structFun_yNode_apply_eq i j intro d hdi hdj by_cases hlat : d ∈ (F.M i).unobserved · have hlat' : d ∈ (F.M j).unobserved := by rw [← F.hUnobs i j] exact hlat simp only [hlat, hlat', dif_pos, valuesProjection] have hidx : (⟨d, hlat⟩ : {d // d ∈ (F.M i).unobserved}) ≍ (⟨d, hlat'⟩ : {d // d ∈ (F.M j).unobserved}) := by apply (Subtype.heq_iff_coe_eq (by intro x; rw [F.hUnobs i j])).mpr rfl have hval : HEq (l ⟨d, hlat⟩) (l' ⟨d, hlat'⟩) := by apply dcongr_heq hidx · intro u u' hu have huv : u.val = u'.val := by exact (Subtype.heq_iff_coe_eq (by intro x; rw [F.hUnobs i j])).mp hu rw [huv] · intro _ _ exact hl exact eq_of_heq hval · have hlat' : d ∉ (F.M j).unobserved := by intro h apply hlat rw [F.hUnobs i j] exact h simp only [hlat, hlat'] by_cases hfix : d ∈ (F.M i).fixed · have hfix' : d ∈ (F.M j).fixed := F.fixed_parent_mem_fixed_of_mem (Finset.mem_inter.mpr ⟨hdi, hfix⟩) simp only [dif_neg (not_false), dif_pos hfix, dif_pos hfix', valuesProjection] · have hfix' : d ∉ (F.M j).fixed := by intro h apply hfix exact F.fixed_parent_mem_fixed_of_mem (i := j) (j := i) (d := d) (Finset.mem_inter.mpr ⟨hdj, h⟩) simp only [hfix, hfix'] rfl