SCM.ID.Density.Mech­CFactor

theorem QmechMeasure_singleton_eq_qLocalMass [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (S : Finset (SWIGNode N)) (hS : S ⊆ M.observed) (hfe : ∀ n : N, SWIGNode.fixed n ∈ M.fixed → ∀ v : SWIGNode N, ¬ M.dag.edge (SWIGNode.random n) v) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) : QmechMeasure M S hS (M.mechDoValues S s x) {valuesProjection hS x} = M.qLocalMass s S hS x := by classical let W := M.mechComplementNames S let hWobs := M.mechComplementNames_random_mem_observed S let hWfix := M.mechComplementNames_fixed_not_mem S let M' := M.fixSet W hWobs hWfix let s' : M'.FixedValues := M.mechDoValues S s x have hclosed : M'.ObsParentClosed S := by simpa [M', W, hWobs, hWfix] using mechComplement_fixSet_obsParentClosed M S hS hfe let hS' : S ⊆ M'.observed := hclosed.1 have hbridge := obsKernel_marginal_singleton_eq_latentProduct_agree M' s' hS' x have heval_local : {ℓ | ∀ v : {v // v ∈ S}, M'.evalMap s' ℓ ⟨v.val, mem_union_left M'.unobserved (hS' v.property)⟩ = x ⟨v.val, hS' v.property⟩} = {ℓ | ∀ v (hv : v ∈ S), M'.localConsistent s' x v (hS' hv) ℓ} := by ext ℓ constructor · intro hEval exact (M'.evalMap_agree_iff_localConsistent s' S hclosed x ℓ).mp (fun v hv => hEval ⟨v, hv⟩) · intro hLocal v exact (M'.evalMap_agree_iff_localConsistent s' S hclosed x ℓ).mpr hLocal v.val v.property have hobsAgree : ∀ w (hw : w ∈ M.observed), x ⟨w, by simpa [M', W, hWobs, hWfix, fixSet_observed] using hw⟩ = x ⟨w, hw⟩ := by intro w hw rfl have hpin : ∀ D (hD : D ∈ W), x ⟨SWIGNode.random D, hWobs D hD⟩ = s' ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩ := by intro D hD have hnew := M.fixSetExtend_apply_new_fixed W hWobs hWfix s (valuesProjection (M.mechComplementNames_image_random_subset_observed S) x) hD simp only [s', mechDoValues] exact hnew.symm have hproj : M.fixSetProj W hWobs hWfix s' = s := by simpa [s', W, hWobs, hWfix, mechDoValues] using (M.fixSetProj_fixSetExtend W hWobs hWfix s (valuesProjection (M.mechComplementNames_image_random_subset_observed S) x)) have hset_do : {ℓ | ∀ v (hv : v ∈ S), M'.localConsistent s' x v (hS' hv) ℓ} = {ℓ | ∀ v (hv : v ∈ S), M.localConsistent s x v (hS hv) ℓ} := by ext ℓ constructor · intro hLocal v hv have hnot : v ∉ W.image SWIGNode.random := by intro hvW rcases Finset.mem_image.mp hvW with ⟨D, hD, rfl⟩ exact (Finset.mem_sdiff.mp (Finset.mem_filter.mp hD).2.1).2 hv exact (localConsistent_fixSet_iff M W hWobs hWfix s' s x x v (hS' hv) (hS hv) hnot hobsAgree hpin hproj ℓ).mp (hLocal v hv) · intro hLocal v hv have hnot : v ∉ W.image SWIGNode.random := by intro hvW rcases Finset.mem_image.mp hvW with ⟨D, hD, rfl⟩ exact (Finset.mem_sdiff.mp (Finset.mem_filter.mp hD).2.1).2 hv exact (localConsistent_fixSet_iff M W hWobs hWfix s' s x x v (hS' hv) (hS hv) hnot hobsAgree hpin hproj ℓ).mpr (hLocal v hv) calc QmechMeasure M S hS (M.mechDoValues S s x) {valuesProjection hS x} = ((M'.obsKernel s').map (valuesProjection hS')) {valuesProjection hS' x} := by rfl _ = M'.latentProduct {ℓ | ∀ v : {v // v ∈ S}, M'.evalMap s' ℓ ⟨v.val, mem_union_left M'.unobserved (hS' v.property)⟩ = x ⟨v.val, hS' v.property⟩} := hbridge _ = M'.latentProduct {ℓ | ∀ v (hv : v ∈ S), M'.localConsistent s' x v (hS' hv) ℓ} := by rw [heval_local] _ = M.latentProduct {ℓ | ∀ v (hv : v ∈ S), M.localConsistent s x v (hS hv) ℓ} := by rw [hset_do] rfl _ = M.qLocalMass s S hS x := by rfl

lemma cComponentDensityFactor_eq_mechCFactor [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) (hStd : M.isStandard) (S : Finset (SWIGNode N)) (hS : S ⊆ M.observed) (hScomp : S ∈ M.toSWIGGraph.cComponentSet) (href : ReferenceFaithful ref) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (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Ω Ω))] (x : ValuesOn M.observed (swigΩ Ω)) : M.cComponentDensityFactor ref s S x = M.mechCFactor ref S hS s x := by classical let I : Finset (Fin M.observed.card) := Finset.univ.filter (fun i : Fin M.observed.card => M.toSWIGGraph.cComponentOf (M.observedAt i).val = S) let num : Fin M.observed.card → ENNReal := fun i => M.qLocalMass s (S ∩ M.prefixNodes (i.val + 1)) (fun _ hv => M.prefixNodes_subset_observed (i.val + 1) (mem_of_mem_inter_right hv)) x let den : Fin M.observed.card → ENNReal := fun i => M.qLocalMass s (S ∩ M.prefixNodes i.val) (fun _ hv => M.prefixNodes_subset_observed i.val (mem_of_mem_inter_right hv)) x let atom : Fin M.observed.card → ENNReal := fun i => ref.μ (M.observedAt i).val ({x (M.observedAt i)} : Set (swigΩ Ω (M.observedAt i).val)) have hsteps : M.cComponentDensityFactor ref s S x = ∏ i ∈ I, (num i / den i) / atom i := by unfold cComponentDensityFactor refine Finset.prod_congr rfl ?_ intro i hi have hiS : M.toSWIGGraph.cComponentOf (M.observedAt i).val = S := (Finset.mem_filter.mp hi).2 exact obsStepCondDensity_eq_component_ratio_div_ref M ref s S hScomp i hiS href hpos x have hatom0 : ∀ i ∈ I, atom i ≠ 0 := by intro i _hi exact href (M.observedAt i).val (x (M.observedAt i)) have hatomtop : ∀ i ∈ I, atom i ≠ ∞ := by intro i _hi exact ne_of_lt (MeasureTheory.measure_lt_top (ref.μ (M.observedAt i).val) ({x (M.observedAt i)} : Set (swigΩ Ω (M.observedAt i).val))) have hsplit : (∏ i ∈ I, (num i / den i) / atom i) = (∏ i ∈ I, num i / den i) / (∏ i ∈ I, atom i) := ENNReal.prod_div_prod₂ I num den atom hatom0 hatomtop have hnum : (∏ i ∈ I, num i / den i) = M.qLocalMass s S hS x := by simpa [I, num, den] using component_qLocalMass_ratio_product M s S hS hScomp hpos x have hrefprod : (∏ i ∈ I, atom i) = jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) := by simpa [I, atom] using component_ref_atom_product_eq_jointRef M ref S hS hScomp x have hanchor : M.mechCFactor ref S hS s x = M.qLocalMass s S hS x / jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) := mechCFactor_eq_qLocalMass_div_jointRef M ref s S hS href (standard_fixed_random_edgeless M hStd) x calc M.cComponentDensityFactor ref s S x = ∏ i ∈ I, (num i / den i) / atom i := hsteps _ = (∏ i ∈ I, num i / den i) / (∏ i ∈ I, atom i) := hsplit _ = M.qLocalMass s S hS x / jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) := by rw [hnum, hrefprod] _ = M.mechCFactor ref S hS s x := hanchor.symm

lemma mechCFactor_fixSet_invariant [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (ref : ReferenceMeasures Ω) (X : Finset N) (href : ReferenceFaithful ref) (hStd : M.isStandard) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (S : Finset (SWIGNode N)) (hS : S ⊆ M.observed) (hSX : ∀ n ∈ X, SWIGNode.random n ∉ S) (sDo : (M.fixSet X hObs hFix).FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) (hpin : ∀ D (hD : D ∈ X), x ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : (M.fixSet X hObs hFix).mechCFactor ref S (by simpa [fixSet_observed] using hS) sDo x = M.mechCFactor ref S hS (M.fixSetProj X hObs hFix sDo) x := by classical let MX := M.fixSet X hObs hFix let hSXobs : S ⊆ MX.observed := by simpa [MX, fixSet_observed] using hS have hfeX : ∀ n : N, SWIGNode.fixed n ∈ MX.fixed → ∀ v : SWIGNode N, ¬ MX.dag.edge (SWIGNode.random n) v := by simpa [MX] using fixSet_fixed_random_edgeless M X hObs hFix hStd have hfeM : ∀ n : N, SWIGNode.fixed n ∈ M.fixed → ∀ v : SWIGNode N, ¬ M.dag.edge (SWIGNode.random n) v := standard_fixed_random_edgeless M hStd have hq : MX.qLocalMass sDo S hSXobs x = M.qLocalMass (M.fixSetProj X hObs hFix sDo) S hS x := qLocalMass_fixSet_invariant M X hObs hFix sDo S hS hSX x hpin have hnumX : QmechMeasure MX S hSXobs (MX.mechDoValues S sDo x) {valuesProjection hSXobs x} = MX.qLocalMass sDo S hSXobs x := QmechMeasure_singleton_eq_qLocalMass MX S hSXobs hfeX sDo x have hnumM : QmechMeasure M S hS (M.mechDoValues S (M.fixSetProj X hObs hFix sDo) x) {valuesProjection hS x} = M.qLocalMass (M.fixSetProj X hObs hFix sDo) S hS x := QmechMeasure_singleton_eq_qLocalMass M S hS hfeM (M.fixSetProj X hObs hFix sDo) x have hprojPoint : valuesProjection hSXobs x = valuesProjection hS x := by ext v rfl have hden0X : jointRef ref S ({valuesProjection hSXobs x} : Set (ValuesOn S (swigΩ Ω))) ≠ 0 := jointRef_singleton_ne_zero ref href S (valuesProjection hSXobs x) have hdenTopX : jointRef ref S ({valuesProjection hSXobs x} : Set (ValuesOn S (swigΩ Ω))) ≠ ∞ := by exact ne_of_lt (MeasureTheory.measure_lt_top (jointRef ref S) ({valuesProjection hSXobs x} : Set (ValuesOn S (swigΩ Ω)))) have hden0M : jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) ≠ 0 := jointRef_singleton_ne_zero ref href S (valuesProjection hS x) have hdenTopM : jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) ≠ ∞ := by exact ne_of_lt (MeasureTheory.measure_lt_top (jointRef ref S) ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω)))) unfold mechCFactor rw [rnDeriv_singleton_eq_div _ _ (absolutelyContinuous_jointRef_of_faithful ref href S (QmechMeasure MX S hSXobs (MX.mechDoValues S sDo x))) (valuesProjection hSXobs x) hden0X hdenTopX] rw [rnDeriv_singleton_eq_div _ _ (absolutelyContinuous_jointRef_of_faithful ref href S (QmechMeasure M S hS (M.mechDoValues S (M.fixSetProj X hObs hFix sDo) x))) (valuesProjection hS x) hden0M hdenTopM] rw [hnumX, hnumM, hq, hprojPoint]

lemma obsStepCondDensity_eq_component_ratio_div_ref [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) (S : Finset (SWIGNode N)) (hScomp : S ∈ M.toSWIGGraph.cComponentSet) (i : Fin M.observed.card) (hiS : M.toSWIGGraph.cComponentOf (M.observedAt i).val = S) (href : ReferenceFaithful ref) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [StandardBorelSpace (ValuesOn ({(M.observedAt i).val} : Finset (SWIGNode N)) (swigΩ Ω))] [Nonempty (ValuesOn ({(M.observedAt i).val} : Finset (SWIGNode N)) (swigΩ Ω))] [CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes i.val) (swigΩ Ω))] (x : ValuesOn M.observed (swigΩ Ω)) : M.obsStepCondDensity ref s i x = (M.qLocalMass s (S ∩ M.prefixNodes (i.val + 1)) (fun _ hv => M.prefixNodes_subset_observed (i.val + 1) (mem_of_mem_inter_right hv)) x / M.qLocalMass s (S ∩ M.prefixNodes i.val) (fun _ hv => M.prefixNodes_subset_observed i.val (mem_of_mem_inter_right hv)) x) / ref.μ (M.observedAt i).val ({x (M.observedAt i)} : Set (swigΩ Ω (M.observedAt i).val)) := by have hac : (M.obsStepCondKernel i.isLt) (s, valuesProjection (M.prefixNodes_subset_observed i.val) x) ≪ ref.μ (M.observedAt i).val := by exact absolutelyContinuous_of_singleton_ne_zero _ _ (href (M.observedAt i).val) have href0 : ref.μ (M.observedAt i).val ({x (M.observedAt i)} : Set (swigΩ Ω (M.observedAt i).val)) ≠ 0 := href (M.observedAt i).val (x (M.observedAt i)) have hreftop : ref.μ (M.observedAt i).val ({x (M.observedAt i)} : Set (swigΩ Ω (M.observedAt i).val)) ≠ ∞ := by exact ne_of_lt (MeasureTheory.measure_lt_top (ref.μ (M.observedAt i).val) _) rw [obsStepCondDensity_eq_mass_ratio M ref s i x hac href0 hreftop] rw [obsStepCondKernel_singleton_eq_prefix_ratio M s i hpos x] rw [obsKernel_prefix_singleton_eq_prod_qLocalMass] rw [obsKernel_prefix_singleton_eq_prod_qLocalMass] rw [prefix_qProduct_ratio_eq_component_ratio M s S hScomp i hiS hpos x]