SCM.ID.Density
Density-based SCM identification tools: reference measures, observational chain-rule factorization, c-component density factors, and do-law marginal bridges.
ReferenceMeasure 6 core · 1 supporting A *reference measure family* assigns one σ-finite measure to every SWIG-node value space: the counting measure for a discrete node, Lebesgue measure for a continuous node, or any σ-finite choice. ★ ReferenceMeasures★ DominatedObs★ obsDensity★ withDensity_obsDensity_eq★ obsKernel_eq_of_obsDensity_ae_eq
Reference measure and joint observational density
A reference measure family assigns one σ-finite measure to every SWIG-node value space: the counting measure for a discrete node, Lebesgue measure for a continuous node, or any σ-finite choice. Its finite product over a node set is the joint reference measure, and a gSCM is dominated when its observational kernel is absolutely continuous with respect to that joint reference. In the dominated case the observational law has a joint density (Radon–Nikodym derivative), and the law is recovered from the density.
This is the foundation for the density-assisted c-component factorization: Tian's
assembly step P(v) = ∏_C Q[C] is a commutative regrouping of scalar density
factors, which has no kernel-composition analogue. The downstream ID theorems in
this slice specialize these reference-measure definitions to finite node value
spaces with measurable singleton sets and faithful finite-product references.
A reference measure family assigns a measure on every random or fixed node's value space, required to be σ-finite.
Definition (Lean source)
The joint reference measure is the finite product of the per-node reference measures over a node set.
A structural causal model is dominated when each observational law is absolutely continuous with respect to the joint reference measure.
Definition (Lean source)
The joint observational density is the Radon-Nikodym derivative of the observational law with respect to the observed-node reference product.
Definition (Lean source)
In a structural causal model whose observational law is absolutely continuous with respect to the joint reference measure on the observed nodes, weighting that joint reference measure by the observational density recovers the observational law exactly.
Formal statement
Proof (Lean source)
Within a model whose observational law is dominated by the joint reference measure, if the joint observational densities at two fixed-value slices agree almost everywhere with respect to that reference measure, then the two slices induce the same observational law.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
instSigmaFiniteJointRefinstance — Finite products of sigma-finite coordinate reference measures are sigma-finite.instance instSigmaFiniteJointRef (ref : ReferenceMeasures Ω) (I : Finset (SWIGNode N)) : SigmaFinite (jointRef ref I) := by unfold jointRef infer_instance
FiniteReference 3 core · 7 supporting When every node value space is finite with measurable singletons, the per-node reference measures in a σ-finite reference family are finite. ★ absolutelyContinuous_jointRef_of_faithful★ aemeasurable_fiber_rnDeriv_of_finite
Finite reference measures for discrete ID densities
When every node value space is finite with measurable singletons, the per-node
reference measures in a σ-finite reference family are finite. Consequently the
finite products jointRef ref I are finite as well. This file packages those
instances and the simple measurability fact used by the finite/discrete
chain-rule density proof.
A reference family is faithful when every single coordinate value has nonzero reference mass.
Definition (Lean source)
Faithful references dominate. On a finite coordinate product indexed by a node set I, if the reference family ref is faithful — every single coordinate value carries nonzero reference mass, then every measure μ on that product is absolutely continuous with respect to the joint reference measure.
Formal statement
Proof (Lean source)
For finite index types α and β, a joint measure μ on α × β, a measure ρ on β, and a Markov kernel κ from α to β, the fibre Radon-Nikodym derivative selector (κ p.1).rnDeriv ρ p.2 is almost-everywhere measurable with respect to μ.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
instFintypeSwigΩinstance — Every random or fixed SWIG-node value space is finite when every base-node value space is finite.instance instFintypeSwigΩ [∀ n, Fintype (Ω n)] : ∀ sn : SWIGNode N, Fintype (swigΩ Ω sn) | .random _ => inferInstance | .fixed _ => inferInstance -
instMeasurableSingletonClassSwigΩinstance — Every random or fixed SWIG-node value space has measurable singletons when every base-node value space has measurable singletons.instance instMeasurableSingletonClassSwigΩ [∀ n, MeasurableSingletonClass (Ω n)] : ∀ sn : SWIGNode N, MeasurableSingletonClass (swigΩ Ω sn) | .random _ => inferInstance | .fixed _ => inferInstance -
isFiniteMeasure_of_finite_measurableSingletonlemma — A σ-finite measure on a finite measurable-singleton space is finite.hypothesesα :μ :conclusionProof (Lean source)
lemma isFiniteMeasure_of_finite_measurableSingleton {α : Type*} [MeasurableSpace α] [Finite α] [MeasurableSingletonClass α] (μ : Measure α) [SigmaFinite μ] : IsFiniteMeasure μ := by refine ⟨?_⟩ have hcover : (Set.univ : Set α) = ⋃ x ∈ (Set.univ : Set α), ({x} : Set α) := by ext x simp rw [hcover] exact MeasureTheory.measure_biUnion_lt_top Set.finite_univ (fun x _ => MeasureTheory.measure_singleton_lt_top (μ := μ) (a := x)) -
instIsFiniteMeasure_refMuinstance — Each coordinate reference measure is finite on finite measurable-singleton node spaces.instance instIsFiniteMeasure_refMu [∀ n, Finite (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (ref : ReferenceMeasures Ω) (v : SWIGNode N) : IsFiniteMeasure (ref.μ v) := by haveI : Finite (swigΩ Ω v) := by cases v <;> infer_instance haveI : SigmaFinite (ref.μ v) := ref.sigmaFinite v exact isFiniteMeasure_of_finite_measurableSingleton (ref.μ v) -
instIsFiniteMeasure_jointRefinstance — The finite product reference measure is finite on finite measurable-singleton node spaces.instance instIsFiniteMeasure_jointRef [∀ n, Finite (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (ref : ReferenceMeasures Ω) (I : Finset (SWIGNode N)) : IsFiniteMeasure (jointRef ref I) := by unfold jointRef infer_instance -
absolutelyContinuous_of_singleton_ne_zerolemma — Any measure is absolutely continuous with respect to a measure that gives every singleton nonzero mass.hypothesesconclusionμ ≪ νProof (Lean source)
lemma absolutelyContinuous_of_singleton_ne_zero {α : Type*} [MeasurableSpace α] (μ ν : Measure α) (hν : ∀ x : α, ν ({x} : Set α) ≠ 0) : μ ≪ ν := by refine MeasureTheory.Measure.AbsolutelyContinuous.mk ?_ intro s _hs hνs have hs_empty : s = ∅ := by ext x constructor · intro hx exfalso have hsingle_subset : ({x} : Set α) ⊆ s := by intro y hy have hyx : y = x := by simpa using hy simpa [hyx] using hx have hle : ν ({x} : Set α) ≤ ν s := MeasureTheory.measure_mono hsingle_subset have hzero : ν ({x} : Set α) = 0 := le_antisymm (by simpa [hνs] using hle) zero_le exact hν x hzero · intro hx cases hx simp [hs_empty] -
jointRef_singleton_ne_zerolemma — A faithful reference family gives every point in a finite coordinate product nonzero joint reference mass.hypothesesProof (Lean source)
lemma jointRef_singleton_ne_zero [∀ n, MeasurableSingletonClass (Ω n)] (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (I : Finset (SWIGNode N)) (x : ValuesOn I (swigΩ Ω)) : jointRef ref I ({x} : Set (ValuesOn I (swigΩ Ω))) ≠ 0 := by classical unfold jointRef rw [MeasureTheory.Measure.pi_singleton] exact Finset.prod_ne_zero_iff.mpr (by intro i _hi exact href i.val (x i))
IdentifyMass 10 core · 5 supporting This file contains the finite, mass-level coordinate operations used by the recursive ID recovery. ★ identifyMassRec_base★ identifyMassRec_hedge★ identifyMassRec_step
Mass-level IDENTIFY functionals
This file contains the finite, mass-level coordinate operations used by the
recursive ID recovery. The graph helpers SWIGGraph.topoLinearOrder,
SWIGGraph.nodesAt, SWIGGraph.nodeIndex, and SWIGGraph.prefixIn enumerate
selected SWIG nodes in topological order. The mass operations
SCM.marginalizeOn and SCM.extractDistrict implement the coordinate
marginalization and district-ratio extraction steps. The recursion
SCM.identifyMassRec then combines induced ancestral restriction, hedge
detection, and district extraction, with simp equations for its base, hedge, and
recursive branches.
This order compares graph nodes by their topological position in the SWIG graph.
Definition (Lean source)
This selector returns the node at a given position in a finite node set sorted by graph topological order.
This selector returns a node's position inside a finite node set sorted by graph topological order.
This finite set contains the first selected nodes in graph topological order.
Marginalize a full-observed mass function by summing over the coordinates in W and overriding those coordinates in the evaluation point.
Extract the district factor for C' from a mass function on A by multiplying adjacent prefix marginal ratios along the topological order of G'.
Definition (Lean source)
The mass-level IDENTIFY recursion. Starting with a mass function for T, it recursively projects to the induced ancestral set of C, extracts the containing district there, and stops when the induced ancestral set is exactly C. The hedge branch A = T returns the current mass function; successful reachability proofs never use that branch.
Definition (Lean source)
For a target set T contained in the observed coordinates, if the graph-induced ancestral set of T relative to C already equals C, then the mass-level IDENTIFY recursion identifyMassRec on T stops immediately and returns the marginal of the input mass function q obtained by summing out the coordinates in T \ C.
Formal statement
Proof (Lean source)
For a target set T contained in the observed coordinates, if the graph-induced ancestral set of T relative to C does not equal C but it equals T itself — the hedge case, reached only after the base case has failed — then the recursion identifyMassRec on T returns the input mass function q unchanged.
Formal statement
Proof (Lean source)
For a target set T contained in the observed coordinates, if the graph-induced ancestral set of T relative to C does not equal C and does not equal T either — i.e. neither the base nor the hedge case applies — then the recursion identifyMassRec on T unfolds one step: it extracts, from the mass function q marginalized onto the induced ancestral set, the district factor of the c-component of C inside that induced ancestral graph, and recurses on that district.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
prefixIn_subsetlemma — Every node in a topological prefix of a selected node set belongs to the selected node set.Proof (Lean source)
lemma prefixIn_subset (G : SWIGGraph N) (D : Finset (SWIGNode N)) (n : ℕ) : G.prefixIn D n ⊆ D := by intro v hv exact (Finset.mem_filter.mp hv).1 -
inducedAncestral_subset_lefttheorem — The induced ancestral set lies inside the ambient observed node set.Proof (Lean source)
theorem inducedAncestral_subset_left (G : SWIGGraph N) (T C : Finset (SWIGNode N)) : inducedAncestral G T C ⊆ T := by intro v hv unfold inducedAncestral at hv have hvObs : v ∈ (G.induce T).observed := (Finset.mem_inter.mp hv).2 exact (Finset.mem_inter.mp (by simpa [SWIGGraph.induce] using hvObs)).1 -
subset_inducedAncestraltheorem — If C is observed and contained in T, then it is contained in its induced ancestral set inside T.hypothesesconclusionC ⊆ inducedAncestral G T CProof (Lean source)
theorem subset_inducedAncestral (G : SWIGGraph N) {T C : Finset (SWIGNode N)} (hCT : C ⊆ T) (hCobs : C ⊆ G.observed) : C ⊆ inducedAncestral G T C := by intro v hv unfold inducedAncestral refine Finset.mem_inter.mpr ⟨?_, ?_⟩ · exact (G.induce T).dag.subset_ancestralSet C hv · simp [SWIGGraph.induce, hCT hv, hCobs hv] -
containingCComponent_subset_observedtheorem — The containing c-component is always a set of observed nodes.Proof (Lean source)
theorem containingCComponent_subset_observed (G : SWIGGraph N) (S : Finset (SWIGNode N)) : containingCComponent G S ⊆ G.observed := by classical by_cases hS : S.Nonempty · simpa [containingCComponent, hS] using G.cComponentOf_subset_observed hS.choose · simp [containingCComponent, hS] -
containingCComponent_induce_subsettheorem — A containing c-component in an induced graph lies inside the inducing set.hypothesesconclusioncontainingCComponent (G.induce A) C ⊆ AProof (Lean source)
theorem containingCComponent_induce_subset (G : SWIGGraph N) (A C : Finset (SWIGNode N)) : containingCComponent (G.induce A) C ⊆ A := by intro v hv have hvObs := containingCComponent_subset_observed (G.induce A) C hv exact (Finset.mem_inter.mp (by simpa [SWIGGraph.induce] using hvObs)).1
LatentBlocks 7 core · 9 supporting This file provides the local-consistency predicate used by the ID density factorization and the latent-block decomposition facts that make q-masses split across c-components. ★ latentBlock_pairwise_disjoint★ localConsistent_fixSet_iff★ evalMap_agree_iff_localConsistent
Latent-block factorization and local consistency
This file provides the local-consistency predicate used by the ID density factorization and the latent-block decomposition facts that make q-masses split across c-components. Local consistency says that an observed assignment agrees with the structural function at a node when parents are read from fixed values, the observed assignment, and a latent realization.
The recursive evaluator can read all earlier observed coordinates from a full observed assignment.
Definition (Lean source)
The latent variables with an edge into a candidate observed c-component.
If C is a full c-component of the causal model's SWIG graph and C' is likewise a full c-component, and C and C' are distinct, then their latent-parent blocks — the unobserved nodes with an edge into the component — are disjoint.
Formal statement
Proof (Lean source)
v's mechanism, parents read locally from x/s/ℓ, reproduces x v.
Definition (Lean source)
Consider an intervention on a node set W whose random copies are all observed and whose fixed copies are not already fixed in the base model, giving the intervened model M.fixSet W. Fix a node v that is not itself one of the intervened random copies and that is observed both in the intervened model and in the base model. If the intervened model's observed assignment x' agrees with the base assignment x on every base-observed coordinate, the base assignment records, at each intervened node, the same value that the intervened model's fixed values assign to the corresponding fixed coordinate, and the intervened model's fixed values sW project, via fixSetProj, onto the base fixed values s, then local consistency of the structural evaluation at v in the intervened model, under sW, x', and a latent realization ℓ, is equivalent to local consistency at v in the base model, under s, x, and the same ℓ.
Formal statement
Proof (Lean source)
A finite set of observed nodes is closed under observed parents.
Definition (Lean source)
On a set P of observed nodes closed under taking observed parents (every observed parent of a member of P is itself in P), agreement of the structural evaluation evalMap with the recorded observed assignment x at every node of P is equivalent to pointwise local consistency of x against a fixed-value slice s and latent realization ℓ at every node of P.
Formal statement
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
latentBlock_pairwise_disjoint_induce_componentslemma — Distinct c-components of an induced SWIG have disjoint latent-parent blocks in the ambient SCM.hypothesesM :SCM N ΩhC :C ∈ (M.toSWIGGraph.induce R).cComponentSethC' :C' ∈ (M.toSWIGGraph.induce R).cComponentSethne :C ≠ C'conclusionDisjoint (M.latentBlock C) (M.latentBlock C')Proof (Lean source)
lemma latentBlock_pairwise_disjoint_induce_components (M : SCM N Ω) (R : Finset (SWIGNode N)) {C C' : Finset (SWIGNode N)} (hC : C ∈ (M.toSWIGGraph.induce R).cComponentSet) (hC' : C' ∈ (M.toSWIGGraph.induce R).cComponentSet) (hne : C ≠ C') : Disjoint (M.latentBlock C) (M.latentBlock C') := by classical rw [Finset.disjoint_left] intro u huC huC' obtain ⟨hu, v, hvC, huv⟩ := by simpa [latentBlock] using (Finset.mem_filter.mp huC) obtain ⟨_hu', w, hwC', huw⟩ := by simpa [latentBlock] using (Finset.mem_filter.mp huC') have hvIndObs : v ∈ (M.toSWIGGraph.induce R).observed := (M.toSWIGGraph.induce R).cComponentSet_subset_observed C hC hvC have hwIndObs : w ∈ (M.toSWIGGraph.induce R).observed := (M.toSWIGGraph.induce R).cComponentSet_subset_observed C' hC' hwC' have hvR : v ∈ R := by simpa [SWIGGraph.induce] using (Finset.mem_inter.mp hvIndObs).1 have hwR : w ∈ R := by simpa [SWIGGraph.induce] using (Finset.mem_inter.mp hwIndObs).1 have hsame := M.toSWIGGraph.induce_cComponentOf_eq_of_shared_unobserved_parent R hu hvR hwR huv huw have hvComp : (M.toSWIGGraph.induce R).cComponentOf v = C := (M.toSWIGGraph.induce R).cComponentOf_eq_of_mem_cComponentSet hC hvC have hwComp : (M.toSWIGGraph.induce R).cComponentOf w = C' := (M.toSWIGGraph.induce R).cComponentOf_eq_of_mem_cComponentSet hC' hwC' exact hne (hvComp ▸ hwComp ▸ hsame) -
latentBlock_pairwise_disjoint_fixSet_induce_componentslemma — Do-model specialization of induced-component latent-block disjointness.hypothesesM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedhC :C ∈ ((M.fixSet X hObs hFix).toSWIGGraph.induce R).cComponentSethC' :C' ∈ ((M.fixSet X hObs hFix).toSWIGGraph.induce R).cComponentSethne :C ≠ C'conclusionProof (Lean source)
lemma latentBlock_pairwise_disjoint_fixSet_induce_components (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (R : Finset (SWIGNode N)) {C C' : Finset (SWIGNode N)} (hC : C ∈ ((M.fixSet X hObs hFix).toSWIGGraph.induce R).cComponentSet) (hC' : C' ∈ ((M.fixSet X hObs hFix).toSWIGGraph.induce R).cComponentSet) (hne : C ≠ C') : Disjoint ((M.fixSet X hObs hFix).latentBlock C) ((M.fixSet X hObs hFix).latentBlock C') := latentBlock_pairwise_disjoint_induce_components (M.fixSet X hObs hFix) R hC hC' hne -
localConsistent_depends_only_on_blocklemma — Local consistency at v depends only on the latent block of v's c-component.hypothesesM :SCM N Ωs :M.FixedValuesv :SWIGNode Nhv :v ∈ M.observedℓ ℓ' :M.LatentValueshℓ :∀ u (hu : u ∈ M.latentBlock (M.toSWIGGraph.cComponentOf v)),ℓ ⟨u, (Finset.mem_filter.mp hu).1⟩ = ℓ' ⟨u, (Finset.mem_filter.mp hu).1⟩conclusionM.localConsistent s x v hv ℓ ↔ M.localConsistent s x v hv ℓ'Proof (Lean source)
lemma localConsistent_depends_only_on_block (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) (v : SWIGNode N) (hv : v ∈ M.observed) (ℓ ℓ' : M.LatentValues) (hℓ : ∀ u (hu : u ∈ M.latentBlock (M.toSWIGGraph.cComponentOf v)), ℓ ⟨u, (Finset.mem_filter.mp hu).1⟩ = ℓ' ⟨u, (Finset.mem_filter.mp hu).1⟩) : M.localConsistent s x v hv ℓ ↔ M.localConsistent s x v hv ℓ' := by unfold localConsistent set j : Fin M.observed.card := M.observedIndex ⟨v, hv⟩ with hj have hat : (M.observedAt j).val = v := by rw [hj] exact M.observedAt_observedIndex ⟨v, hv⟩ have hfun : M.structFun (M.observedAt j) (fun w => M.parentMap s ℓ j.isLt (prevFromObservedValues M x) w) = M.structFun (M.observedAt j) (fun w => M.parentMap s ℓ' j.isLt (prevFromObservedValues M x) w) := by congr 1 funext w by_cases huo : w.val ∈ M.unobserved · rw [parentMap_unobserved M s ℓ j.isLt _ w huo, parentMap_unobserved M s ℓ' j.isLt _ w huo] have hedge_v : M.dag.edge w.val v := by have hedge_at : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property simpa [hat] using hedge_at have hvComp : v ∈ M.toSWIGGraph.cComponentOf v := M.toSWIGGraph.mem_cComponentOf_self (by simpa using hv) have huBlock : w.val ∈ M.latentBlock (M.toSWIGGraph.cComponentOf v) := by rw [latentBlock, mem_filter] exact ⟨huo, ⟨v, hvComp, hedge_v⟩⟩ exact hℓ w.val huBlock · by_cases hfix : w.val ∈ M.fixed · rw [parentMap_fixed M s ℓ j.isLt _ w hfix, parentMap_fixed M s ℓ' j.isLt _ w hfix] · have hedge : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo rw [parentMap_observed M s ℓ j.isLt _ w hobs, parentMap_observed M s ℓ' j.isLt _ w hobs] subst j change ((M.observedAt_observedIndex ⟨v, hv⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v, hv⟩)) (fun w => M.parentMap s ℓ (M.observedIndex ⟨v, hv⟩).isLt (prevFromObservedValues M x) w) = x ⟨v, hv⟩) ↔ ((M.observedAt_observedIndex ⟨v, hv⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v, hv⟩)) (fun w => M.parentMap s ℓ' (M.observedIndex ⟨v, hv⟩).isLt (prevFromObservedValues M x) w) = x ⟨v, hv⟩) rw [hfun] -
observedAt_observedIndex_subtypelemma — Taking an observed node to its topological index and back recovers the same observed-node subtype value.hypothesesconclusionM.observedAt (M.observedIndex ⟨v, hv⟩) = ⟨v, hv⟩Proof (Lean source)
lemma observedAt_observedIndex_subtype (M : SCM N Ω) {v : SWIGNode N} (hv : v ∈ M.observed) : M.observedAt (M.observedIndex ⟨v, hv⟩) = ⟨v, hv⟩ := Subtype.ext (M.observedAt_observedIndex ⟨v, hv⟩) -
prevFromObservedValues_apply_observedlemmahypothesesM :SCM N Ωn :ℕn < M.observed.cardw :{w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}hobs :w.val ∈ M.observedhlt :(M.observedIndex ⟨w.val, hobs⟩).val < nconclusion(M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ prevFromObservedValues M x (M.observedIndex ⟨w.val, hobs⟩).val hlt (M.observedIndex ⟨w.val, hobs⟩).isLt= x ⟨w.val, hobs⟩Proof (Lean source)
lemma prevFromObservedValues_apply_observed (M : SCM N Ω) (x : ValuesOn M.observed (swigΩ Ω)) {n : ℕ} {hn : n < M.observed.card} {w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}} (hobs : w.val ∈ M.observed) (hlt : (M.observedIndex ⟨w.val, hobs⟩).val < n) : (M.observedAt_observedIndex ⟨w.val, hobs⟩) ▸ prevFromObservedValues M x (M.observedIndex ⟨w.val, hobs⟩).val hlt (M.observedIndex ⟨w.val, hobs⟩).isLt = x ⟨w.val, hobs⟩ := by unfold prevFromObservedValues set wobs : {v // v ∈ M.observed} := M.observedAt (M.observedIndex ⟨w.val, hobs⟩) have hsub : wobs = ⟨w.val, hobs⟩ := by change M.observedAt (M.observedIndex ⟨w.val, hobs⟩) = ⟨w.val, hobs⟩ exact observedAt_observedIndex_subtype M hobs change (Subtype.ext_iff.mp hsub) ▸ x wobs = x ⟨w.val, hobs⟩ clear_value wobs subst hsub rfl -
parentMap_prevFromObservedValues_eq_dispatchlemmahypothesesM :SCM N Ωs :M.FixedValuesℓ :M.LatentValuesj :Fin M.observed.cardw :{w // w ∈ M.dag.parents (M.observedAt j).val}conclusionM.parentMap s ℓ j.isLt (prevFromObservedValues M x) w= (if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo x ⟨w.val, hobs⟩)Proof (Lean source)
lemma parentMap_prevFromObservedValues_eq_dispatch (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) (ℓ : M.LatentValues) (j : Fin M.observed.card) (w : {w // w ∈ M.dag.parents (M.observedAt j).val}) : M.parentMap s ℓ j.isLt (prevFromObservedValues M x) w = (if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo x ⟨w.val, hobs⟩) := by by_cases huo : w.val ∈ M.unobserved · rw [parentMap_unobserved M s ℓ j.isLt _ w huo, dif_pos huo] · rw [dif_neg huo] by_cases hfix : w.val ∈ M.fixed · rw [parentMap_fixed M s ℓ j.isLt _ w hfix, dif_pos hfix] · rw [dif_neg hfix] have hedge : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo rw [parentMap_observed M s ℓ j.isLt _ w hobs] exact prevFromObservedValues_apply_observed M x hobs (M.observed_parent_index_lt j.isLt hedge hobs) -
localConsistent_iff_structFun_dispatchlemmahypothesesconclusionM.localConsistent s x v hv ℓ↔ M.structFun ⟨v, hv⟩ (fun w : {w // w ∈ M.dag.parents v} => if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val v := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo x ⟨w.val, hobs⟩) = x ⟨v, hv⟩Proof (Lean source)
lemma localConsistent_iff_structFun_dispatch (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) (v : SWIGNode N) (hv : v ∈ M.observed) (ℓ : M.LatentValues) : M.localConsistent s x v hv ℓ ↔ M.structFun ⟨v, hv⟩ (fun w : {w // w ∈ M.dag.parents v} => if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val v := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo x ⟨w.val, hobs⟩) = x ⟨v, hv⟩ := by set j : Fin M.observed.card := M.observedIndex ⟨v, hv⟩ with hj set vobs : {v // v ∈ M.observed} := M.observedAt j with hvobs have hsub : vobs = ⟨v, hv⟩ := by rw [hvobs] rw [hj] exact observedAt_observedIndex_subtype M hv have hiff := localConsistent_iff_structFun_dispatch_at_observedAt M s x ℓ j change M.localConsistent s x vobs.val vobs.property ℓ ↔ M.structFun vobs (fun w : {w // w ∈ M.dag.parents vobs.val} => if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val vobs.val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo x ⟨w.val, hobs⟩) = x vobs at hiff clear_value vobs subst hsub exact hiff -
evalMap_eq_iff_localConsistent_of_observed_parent_agreelemma — When all observed parents agree with their assigned values, evaluation at an observed node equals its assignment exactly when the latent values are locally consistent.hypothesesM :SCM N Ωs :M.FixedValuesℓ :M.LatentValuesv :SWIGNode Nhv :v ∈ M.observedhprev :∀ w (hw : w ∈ M.observed)ifM.dag.edge w vthenM.evalMap s ℓ ⟨w, mem_union_left _ hw⟩ = x ⟨w, hw⟩conclusionM.evalMap s ℓ ⟨v, mem_union_left _ hv⟩ = x ⟨v, hv⟩ ↔ M.localConsistent s x v hv ℓProof (Lean source)
lemma evalMap_eq_iff_localConsistent_of_observed_parent_agree (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) (ℓ : M.LatentValues) (v : SWIGNode N) (hv : v ∈ M.observed) (hprev : ∀ w (hw : w ∈ M.observed), M.dag.edge w v → M.evalMap s ℓ ⟨w, mem_union_left _ hw⟩ = x ⟨w, hw⟩) : M.evalMap s ℓ ⟨v, mem_union_left _ hv⟩ = x ⟨v, hv⟩ ↔ M.localConsistent s x v hv ℓ := by rw [evalMap_observed_unfold M s ℓ ⟨v, hv⟩, localConsistent_iff_structFun_dispatch M s x v hv ℓ] have hfun : M.structFun ⟨v, hv⟩ (fun w : {w // w ∈ M.dag.parents v} => if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val v := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo M.evalMap s ℓ ⟨w.val, mem_union_left _ hobs⟩) = M.structFun ⟨v, hv⟩ (fun w : {w // w ∈ M.dag.parents v} => if huo : w.val ∈ M.unobserved then ℓ ⟨w.val, huo⟩ else if hfix : w.val ∈ M.fixed then s ⟨w.val, hfix⟩ else have hedge : M.dag.edge w.val v := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo x ⟨w.val, hobs⟩) := by congr 1 funext w by_cases huo : w.val ∈ M.unobserved · rw [dif_pos huo, dif_pos huo] · rw [dif_neg huo, dif_neg huo] by_cases hfix : w.val ∈ M.fixed · rw [dif_pos hfix, dif_pos hfix] · rw [dif_neg hfix, dif_neg hfix] have hedge : M.dag.edge w.val v := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo exact hprev w.val hobs hedge rw [hfun] -
evalMap_eq_x_of_observedAt_eqlemma — If structural evaluation at an indexed observed node equals its recorded value, then the same equality holds after replacing that node by any equal observed node.hypothesesM :SCM N Ωs :M.FixedValuesℓ :M.LatentValuesj :Fin M.observed.cardv :SWIGNode Nhv :v ∈ M.observedhval :(M.observedAt j).val = vh :M.evalMap s ℓ ⟨(M.observedAt j).val, mem_union_left M.unobserved (M.observedAt j).property⟩= x (M.observedAt j)conclusionM.evalMap s ℓ ⟨v, mem_union_left _ hv⟩ = x ⟨v, hv⟩Proof (Lean source)
lemma evalMap_eq_x_of_observedAt_eq (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) (ℓ : M.LatentValues) (j : Fin M.observed.card) {v : SWIGNode N} (hv : v ∈ M.observed) (hval : (M.observedAt j).val = v) (h : M.evalMap s ℓ ⟨(M.observedAt j).val, mem_union_left M.unobserved (M.observedAt j).property⟩ = x (M.observedAt j)) : M.evalMap s ℓ ⟨v, mem_union_left _ hv⟩ = x ⟨v, hv⟩ := by set vobs : {v // v ∈ M.observed} := M.observedAt j with hvobs have hsub : vobs = ⟨v, hv⟩ := by rw [hvobs] exact Subtype.ext hval change M.evalMap s ℓ ⟨vobs.val, mem_union_left M.unobserved vobs.property⟩ = x vobs at h clear_value vobs subst hsub exact h
ChainRuleDensity 6 core · 20 supporting For a dominated structural causal model with σ-finite node reference measures, the joint observational density factors along the topological order of the observed nodes as a product of one-node conditional densities, ass ★ obsDensity_eq_qFactorDensityProduct
Observational chain-rule density
For a dominated structural causal model with σ-finite node reference measures, the
joint observational density factors along the topological order of the observed
nodes as a product of one-node conditional densities, assuming the stepwise fibre
Radon--Nikodym data (fibre domination and a jointly measurable fibre derivative) is
available. This is the density analogue of the kernel chain rule
obsKernel_eq_qFactorProduct; unlike the kernel version it holds for continuous
(Lebesgue-referenced) nodes, not just finite/discrete ones.
The right-hand side below is deliberately not a tautological copy of
obsDensity: each factor is the Radon--Nikodym derivative of the one-node
conditional kernel obsStepCondKernel against the corresponding one-node
reference measure, evaluated at the prefix and coordinate read from the full
observed assignment.
The one-node conditional density factor at an observed coordinate.
Definition (Lean source)
The chain-rule density product for the observational law.
Definition (Lean source)
The recursive prefix density product matching obsChainKernel.
Definition (Lean source)
Per-step analytic hypotheses needed to expose the fibre Radon--Nikodym derivative against a σ-finite one-node reference.
Definition (Lean source)
The i-th one-step density factor read from a k-prefix assignment.
Definition (Lean source)
Observational density chain rule. In a structural causal model whose observational law is absolutely continuous with respect to the joint reference measure on the observed nodes, if in addition the stepwise fibre Radon--Nikodym condition holds along the observed topological order, then the joint observational density agrees, almost everywhere with respect to that joint reference measure, with the product of the one-node conditional density factors taken in observed topological order.
Formal statement
Proof (Lean source)
20 supporting declarations (lemmas, instances)
-
prefixNodes_monolemma — Prefix node sets are monotone in the prefix length.Proof (Lean source)
lemma prefixNodes_mono (M : SCM N Ω) {m k : ℕ} (h : m ≤ k) : M.prefixNodes m ⊆ M.prefixNodes k := by intro v hv rcases (M.mem_prefixNodes_iff m v).mp hv with ⟨hobs, hlt⟩ exact (M.mem_prefixNodes_iff k v).mpr ⟨hobs, lt_of_lt_of_le hlt h⟩ -
map_pi_valuesEquivOfEqlemma — Measure.pi reindexes along valuesEquivOfEq, with no probability-measure hypothesis (the index equality reduces the equiv to the identity). This is the σ-finite-friendly companion of measurePreserving_valuesEquivOfEq.hypothesesconclusion= pi (fun j : {j // j ∈ J} => μ ⟨j.val, h ▸ j.property⟩)Proof (Lean source)
lemma map_pi_valuesEquivOfEq {M' : Type*} [DecidableEq M'] {I J : Finset M'} {Ω' : M' → Type*} [∀ n, MeasurableSpace (Ω' n)] (h : I = J) (μ : (i : {i // i ∈ I}) → Measure (Ω' i.val)) : (pi μ).map (valuesEquivOfEq (Ω := Ω') h) = pi (fun j : {j // j ∈ J} => μ ⟨j.val, h ▸ j.property⟩) := by subst h have hid : (⇑(valuesEquivOfEq (Ω := Ω') (rfl : I = I)) : ValuesOn I Ω' → ValuesOn I Ω') = id := by funext ξ; rfl rw [hid, MeasureTheory.Measure.map_id] -
singletonValues_map_ref_eq_jointReflemma — The scalar reference on one node maps to the singleton product reference.hypothesesref :v :SWIGNode NProof (Lean source)
lemma singletonValues_map_ref_eq_jointRef (ref : ReferenceMeasures Ω) (v : SWIGNode N) : (ref.μ v).map (singletonValues (α := swigΩ Ω) (v := v)) = jointRef ref ({v} : Finset (SWIGNode N)) := by classical rw [jointRef] let e := MeasurableEquiv.piUnique (fun i : {i // i ∈ ({v} : Finset (SWIGNode N))} => swigΩ Ω i.val) have hfun : (singletonValues (α := swigΩ Ω) (v := v)) = (fun x : swigΩ Ω v => (e.symm) (by simpa using x)) := by funext x ext i obtain ⟨w, hw⟩ := i have hwv : w = v := by simpa using hw subst w rfl calc map (singletonValues (α := swigΩ Ω) (v := v)) (ref.μ v) = map (fun x : swigΩ Ω v => (e.symm) (by simpa using x)) (ref.μ v) := by rw [hfun] _ = pi (fun i : {i // i ∈ ({v} : Finset (SWIGNode N))} => ref.μ i.val) := by have hmp := (MeasureTheory.measurePreserving_piUnique (fun i : {i // i ∈ ({v} : Finset (SWIGNode N))} => ref.μ i.val)).symm e simpa using hmp.map_eq -
jointRef_prefix_card_maplemma — Transport the full-prefix reference measure to the observed-value reference.hypothesesM :SCM N Ωref :Proof (Lean source)
lemma jointRef_prefix_card_map (M : SCM N Ω) (ref : ReferenceMeasures Ω) : (jointRef ref (M.prefixNodes M.observed.card)).map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) = jointRef ref M.observed := by rw [jointRef, jointRef, map_pi_valuesEquivOfEq (M.prefixNodes_card M.observed.card (le_refl _)) (fun i => ref.μ i.val)] -
jointRef_extendObsPrefixlemma — The successor prefix extension carries the product of the old-prefix reference and the next-node reference to the successor-prefix reference.hypothesesProof (Lean source)
lemma jointRef_extendObsPrefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) {k : ℕ} (hk : k < M.observed.card) : ((jointRef ref (M.prefixNodes k)).prod (ref.μ (M.observedAt ⟨k, hk⟩).val)).map (M.extendObsPrefix hk) = jointRef ref (M.prefixNodes (k + 1)) := by classical let v : SWIGNode N := (M.observedAt ⟨k, hk⟩).val let A : Finset (SWIGNode N) := M.prefixNodes k let B : Finset (SWIGNode N) := ({v} : Finset (SWIGNode N)) let hDisj : Disjoint A B := by simpa [A, B, v] using M.prefixNodes_disjoint_singleton_next hk have hsing : (ref.μ v).map (singletonValues (α := swigΩ Ω) (v := v)) = jointRef ref B := by simpa [B] using singletonValues_map_ref_eq_jointRef (Ω := Ω) ref v have hprod : ((jointRef ref A).prod (ref.μ v)).map (map id (singletonValues (α := swigΩ Ω) (v := v))) = (jointRef ref A).prod (jointRef ref B) := by rw [← MeasureTheory.Measure.map_prod_map (jointRef ref A) (ref.μ v) measurable_id (measurable_singletonValues (α := swigΩ Ω))] simp [hsing] 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 extendObsPrefix change (((jointRef ref A).prod (ref.μ v)).map ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk).symm) ∘ (fun p : ValuesOn A (swigΩ Ω) × swigΩ Ω v => valuesUnionMk p.1 (singletonValues (α := swigΩ Ω) (v := v) p.2)))) = jointRef ref (M.prefixNodes (k + 1)) rw [← MeasureTheory.Measure.map_map] · have hinner : (fun p : ValuesOn A (swigΩ Ω) × swigΩ Ω v => valuesUnionMk p.1 (singletonValues (α := swigΩ Ω) (v := v) p.2)) = ((fun q : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk q.1 q.2) ∘ (map id (singletonValues (α := swigΩ Ω) (v := v)))) := by rfl rw [hinner] rw [← MeasureTheory.Measure.map_map] · have hunion_fun : (fun q : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω) => valuesUnionMk q.1 q.2) = ((valuesUnionEquiv (Ω := Ω) hDisj).symm) := by rfl rw [hunion_fun, hprod, hunion] rw [jointRef, map_pi_valuesEquivOfEq] rfl · exact measurable_valuesUnionMk (Ω := swigΩ Ω) · exact measurable_id.prodMap (measurable_singletonValues (α := swigΩ Ω)) · exact (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk).symm).measurable · exact (measurable_valuesUnionMk (Ω := swigΩ Ω)).comp (measurable_id.prodMap (measurable_singletonValues (α := swigΩ Ω))) -
prefixDensityProduct_eq_range_productlemma — The recursive prefix density product is the range product of its one-step factors.hypothesesM :SCM N Ωref :s :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :k :ℕhk :k ≤ M.observed.cardconclusionM.prefixDensityProduct ref s k z= ∏ i ∈ range k, M.prefixStepDensityInPrefix ref s k z iProof (Lean source)
lemma prefixDensityProduct_eq_range_product (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) [∀ 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Ω Ω))] (k : ℕ) (hk : k ≤ M.observed.card) (z : ValuesOn (M.prefixNodes k) (swigΩ Ω)) : M.prefixDensityProduct ref s k z = ∏ i ∈ range k, M.prefixStepDensityInPrefix ref s k z i := by induction k with | zero => simp [prefixDensityProduct] | succ k ih => have hkcard : k < M.observed.card := Nat.lt_of_succ_le hk rw [prefixDensityProduct] rw [ih (le_of_succ_le hk) (valuesProjection (M.prefixNodes_mono (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 < M.observed.card := lt_of_lt_of_le hik (le_of_succ_le hk) have hproj : valuesProjection (M.prefixNodes_mono (le_of_lt hik)) (valuesProjection (M.prefixNodes_mono (Nat.le_succ k)) z) = valuesProjection (M.prefixNodes_mono (le_of_lt hisucc)) z := by funext a rfl simp [prefixStepDensityInPrefix, hik, hisucc, hicard, hproj, valuesProjection] · simp [prefixStepDensityInPrefix, hkcard] -
prefixDensityProduct_card_eq_qFactorDensityProductlemma — At the full observed prefix, the recursive prefix density product is the existing finite product over observed indices.hypothesesM :SCM N Ωref :s :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :conclusionM.prefixDensityProduct ref s M.observed.card y= M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y)Proof (Lean source)
lemma prefixDensityProduct_card_eq_qFactorDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) [∀ 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Ω Ω))] (y : ValuesOn (M.prefixNodes M.observed.card) (swigΩ Ω)) : M.prefixDensityProduct ref s M.observed.card y = M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y) := by rw [prefixDensityProduct_eq_range_product M ref s M.observed.card (le_refl _) y] rw [Finset.prod_range] simp only [qFactorDensityProduct, obsStepCondDensity, prefixStepDensityInPrefix, valuesEquivOfEq] refine Finset.prod_congr rfl ?_ intro i _hi have hproj : valuesProjection (M.prefixNodes_subset_observed i.val) (valuesProjection (le_of_eq (M.prefixNodes_card M.observed.card (le_refl _)).symm) y) = valuesProjection (M.prefixNodes_mono (le_of_lt i.isLt)) y := by funext a rfl simp only [i.isLt] rfl -
rnDeriv_compProd_same_leftlemma — Conditional factor of the composition-product Radon–Nikodym derivative.hypothesesconclusion(μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2Proof (Lean source)
lemma rnDeriv_compProd_same_left {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [CountableOrCountablyGenerated α β] (μ : Measure α) (κ η : Kernel α β) [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (h_ac : ∀ a, κ a ≪ η a) : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2 := by have hκeq : η.withDensity (rnDeriv κ η) = κ := ProbabilityTheory.Kernel.ext fun a => ProbabilityTheory.Kernel.withDensity_rnDeriv_eq (h_ac a) haveI : IsSFiniteKernel (η.withDensity (rnDeriv κ η)) := by rw [hκeq]; infer_instance have hcp : μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun p => rnDeriv κ η p.1 p.2) := by conv_lhs => rw [← hκeq] exact MeasureTheory.Measure.compProd_withDensity (ProbabilityTheory.Kernel.measurable_rnDeriv κ η) rw [hcp] exact MeasureTheory.Measure.rnDeriv_withDensity (μ ⊗ₘ η) (ProbabilityTheory.Kernel.measurable_rnDeriv κ η) -
absolutelyContinuous_of_map_measurableEmbeddinglemma — Pull absolute continuity back through a measurable embedding.Proof (Lean source)
lemma absolutelyContinuous_of_map_measurableEmbedding {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) {μ ν : Measure α} (h : μ.map f ≪ ν.map f) : μ ≪ ν := by intro A hνA have hν_image : ν.map f (f '' A) = 0 := by rw [hf.map_apply ν (f '' A), hf.injective.preimage_image] exact hνA have hμ_image : μ.map f (f '' A) = 0 := h hν_image rw [hf.map_apply μ (f '' A), hf.injective.preimage_image] at hμ_image exact hμ_image -
rnDeriv_compProd_same_left_aelemma — Same-left composition-product RN derivative under a.e. fibre absolute continuity. This is the a.e. variant needed after extracting fibre domination from product domination.hypothesesconclusion(μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2Proof (Lean source)
lemma rnDeriv_compProd_same_left_ae {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [CountableOrCountablyGenerated α β] (μ : Measure α) (κ η : Kernel α β) [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (h_ac : ∀ᵐ a ∂μ, κ a ≪ η a) : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p => rnDeriv κ η p.1 p.2 := by have hκeq : κ =ᵐ[μ] η.withDensity (rnDeriv κ η) := by filter_upwards [h_ac] with a ha exact (ProbabilityTheory.Kernel.withDensity_rnDeriv_eq ha).symm haveI : IsSFiniteKernel (η.withDensity (rnDeriv κ η)) := by infer_instance have hcp : μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun p => rnDeriv κ η p.1 p.2) := by calc μ ⊗ₘ κ = μ ⊗ₘ (η.withDensity (rnDeriv κ η)) := MeasureTheory.Measure.compProd_congr hκeq _ = (μ ⊗ₘ η).withDensity (fun p => rnDeriv κ η p.1 p.2) := by exact MeasureTheory.Measure.compProd_withDensity (ProbabilityTheory.Kernel.measurable_rnDeriv κ η) rw [hcp] exact MeasureTheory.Measure.rnDeriv_withDensity (μ ⊗ₘ η) (ProbabilityTheory.Kernel.measurable_rnDeriv κ η) -
rnDeriv_compProd_prod_sigmaFinite_of_fiber_aclemma — σ-finite product-reference RN derivative for a finite kernel, under explicit fibre domination and fibre-density measurability.hypothesesα β :μ ν :Measure αρ :Measure βκ :Kernel α βf :α → ENNRealhμν :μ ≪ νhfiber :∀ᵐ a ∂μ, κ a ≪ ρhfiber_meas :AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (ν.prod ρ)hf :μ.rnDeriv ν =ᵐ[ν] fconclusion(μ ⊗ₘ κ).rnDeriv (ν.prod ρ) =ᵐ[ν.prod ρ] fun p => f p.1 * (κ p.1).rnDeriv ρ p.2Proof (Lean source)
lemma rnDeriv_compProd_prod_sigmaFinite_of_fiber_ac {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ ν : Measure α) (ρ : Measure β) (κ : Kernel α β) (f : α → ENNReal) [IsFiniteMeasure μ] [SigmaFinite ν] [SigmaFinite ρ] [IsFiniteKernel κ] (hμν : μ ≪ ν) (hfiber : ∀ᵐ a ∂μ, κ a ≪ ρ) (hfiber_meas : AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (ν.prod ρ)) (hf : μ.rnDeriv ν =ᵐ[ν] f) : (μ ⊗ₘ κ).rnDeriv (ν.prod ρ) =ᵐ[ν.prod ρ] fun p => f p.1 * (κ p.1).rnDeriv ρ p.2 := by exact rnDeriv_compProd_prod_sigmaFinite μ ν ρ κ f hμν hfiber hfiber_meas hf -
obsChainKernel_absolutelyContinuous_jointRef_prefixlemma — Domination of the recursive observed-prefix chain by the prefix reference.hypothesesM :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :k :ℕhk :k ≤ M.observed.cardconclusionM.obsChainKernel k hk s ≪ jointRef ref (M.prefixNodes k)Proof (Lean source)
lemma obsChainKernel_absolutelyContinuous_jointRef_prefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ 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Ω Ω))] (k : ℕ) (hk : k ≤ M.observed.card) : M.obsChainKernel k hk s ≪ jointRef ref (M.prefixNodes k) := by classical -- The chain kernel is the prefix marginal of the (dominated) observational law. rw [← M.obsKernel_map_prefixNodes s k hk] have hsubset : M.prefixNodes k ⊆ M.observed := M.prefixNodes_subset_observed k have hDisj : Disjoint (M.prefixNodes k) (M.observed \ M.prefixNodes k) := disjoint_sdiff_self_right have hAB : M.prefixNodes k ∪ (M.observed \ M.prefixNodes k) = M.observed := Finset.union_sdiff_of_subset hsubset -- The prefix projection factors as `fst ∘ union-equiv ∘ reindex`. have hfun : (valuesProjection (Ω := swigΩ Ω) hsubset) = fst ∘ (valuesUnionEquiv (Ω := Ω) hDisj) ∘ (valuesEquivOfEq (Ω := swigΩ Ω) hAB.symm) := by funext ω i; rfl -- The reference marginal is a scalar multiple of the prefix reference. have hmarg : (jointRef ref M.observed).map (valuesProjection hsubset) = (jointRef ref (M.observed \ M.prefixNodes k) univ) • jointRef ref (M.prefixNodes 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 ∈ M.observed} => ref.μ i.val)] have hsplit : (pi (fun j : {j // j ∈ M.prefixNodes k ∪ (M.observed \ M.prefixNodes k)} => ref.μ j.val)).map (valuesUnionEquiv (Ω := Ω) hDisj) = (jointRef ref (M.prefixNodes k)).prod (jointRef ref (M.observed \ M.prefixNodes k)) := by have hmp := measurePreserving_valuesUnionEquiv (Ω := Ω) hDisj ref.μ simpa [jointRef] using hmp.map_eq rw [hsplit, MeasureTheory.Measure.map_fst_prod] -- Push the joint domination forward and absorb the scalar. refine ((hdom s).map (measurable_valuesProjection hsubset)).trans ?_ rw [hmarg] intro t ht simp [MeasureTheory.Measure.smul_apply, ht] -
obsChainKernel_rnDeriv_eq_prefixDensityProductlemma — General prefix-level RN derivative for the recursive observational chain.hypothesesM :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :hstep :ObsStepFiberRN M ref sProof (Lean source)
lemma obsChainKernel_rnDeriv_eq_prefixDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ 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Ω Ω))] (hstep : ObsStepFiberRN M ref s) : ∀ (k : ℕ) (hk : k ≤ M.observed.card), (M.obsChainKernel k hk s).rnDeriv (jointRef ref (M.prefixNodes k)) =ᵐ[jointRef ref (M.prefixNodes k)] M.prefixDensityProduct ref s k := by intro k induction k with | zero => intro hk -- `ValuesOn (prefixNodes 0)` is a one-point space; both measures are probability -- measures there, hence equal, and `rnDeriv_self =ᵐ 1 = prefixDensityProduct 0`. have hsub : Subsingleton (ValuesOn (M.prefixNodes 0) (swigΩ Ω)) := ⟨fun a b => funext fun i => absurd (M.prefixNodes_zero ▸ i.property) (notMem_empty i.val)⟩ have heq : M.obsChainKernel 0 hk s = jointRef ref (M.prefixNodes 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_univ, jointRef, MeasureTheory.Measure.pi_univ] symm apply Finset.prod_eq_one intro i _ obtain ⟨_, hlt⟩ := (M.mem_prefixNodes_iff 0 i.val).mp i.property exact absurd hlt (Nat.not_lt_zero _) rw [heq] have h1 : M.prefixDensityProduct ref s 0 = (fun _ => (1 : ENNReal)) := rfl rw [h1] exact MeasureTheory.Measure.rnDeriv_self _ | succ k ih => intro hk classical have hkc : k < M.observed.card := Nat.lt_of_succ_le hk have hkprev : k ≤ M.observed.card := Nat.le_of_succ_le hk let node : SWIGNode N := (M.observedAt ⟨k, hkc⟩).val let νk : Measure (ValuesOn (M.prefixNodes k) (swigΩ Ω)) := jointRef ref (M.prefixNodes k) let refnode : Measure (swigΩ Ω node) := ref.μ node let chain : Measure (ValuesOn (M.prefixNodes k) (swigΩ Ω)) := M.obsChainKernel k hkprev s let stepK : Kernel (ValuesOn (M.prefixNodes k) (swigΩ Ω)) (swigΩ Ω node) := (M.obsStepCondKernel hkc).sectR s let ext : ValuesOn (M.prefixNodes k) (swigΩ Ω) × swigΩ Ω node → ValuesOn (M.prefixNodes (k + 1)) (swigΩ Ω) := M.extendObsPrefix hkc have hchainSucc : M.obsChainKernel (k + 1) hk s = (chain ⊗ₘ stepK).map ext := by dsimp [chain, stepK, ext] change ((((M.obsChainKernel k hkprev) ⊗ₖ (M.obsStepCondKernel hkc)).map (M.extendObsPrefix hkc)) s) = (((M.obsChainKernel k hkprev) s) ⊗ₘ ((M.obsStepCondKernel hkc).sectR s)).map (M.extendObsPrefix hkc) rw [ProbabilityTheory.Kernel.map_apply _ (M.measurable_extendObsPrefix hkc)] rw [ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR] have hrefSucc : jointRef ref (M.prefixNodes (k + 1)) = (νk.prod refnode).map ext := by dsimp [νk, refnode, node, ext] exact (jointRef_extendObsPrefix M ref hkc).symm have hsingle_emb : MeasurableEmbedding (singletonValues (α := swigΩ Ω) (v := node)) := by refine ⟨?_, measurable_singletonValues (α := swigΩ Ω), ?_⟩ · intro x y hxy have := congrArg (singletonValue (α := swigΩ Ω) (v := node)) hxy simpa using this · intro A hA have hpre : singletonValues (α := swigΩ Ω) (v := node) '' A = (singletonValue (α := swigΩ Ω) (v := node)) ⁻¹' A := by ext x constructor · rintro ⟨a, ha, rfl⟩ simpa using ha · intro hx refine ⟨singletonValue (α := swigΩ Ω) (v := node) x, hx, ?_⟩ exact singletonValues_singletonValue (α := swigΩ Ω) x rw [hpre] exact hA.preimage (measurable_singletonValue (α := swigΩ Ω)) have hext_emb : MeasurableEmbedding ext := by dsimp [ext, node] unfold extendObsPrefix refine (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hkc).symm).measurableEmbedding.comp ?_ change MeasurableEmbedding ((fun q : ValuesOn (M.prefixNodes k) (swigΩ Ω) × ValuesOn ({(M.observedAt ⟨k, hkc⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) => valuesUnionMk q.1 q.2) ∘ map id (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨k, hkc⟩).val))) refine ((valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hkc)).symm.measurableEmbedding).comp ?_ exact MeasurableEmbedding.id.prodMap hsingle_emb have hcore : (chain ⊗ₘ stepK).rnDeriv (νk.prod refnode) =ᵐ[νk.prod refnode] fun p => M.prefixDensityProduct ref s k p.1 * (stepK p.1).rnDeriv refnode p.2 := by have hchain_ac : chain ≪ νk := by dsimp [chain, νk] exact M.obsChainKernel_absolutelyContinuous_jointRef_prefix ref hdom s k hkprev have hfiber := hstep k hkc have hfiber_meas : AEMeasurable (fun p : ValuesOn (M.prefixNodes k) (swigΩ Ω) × swigΩ Ω node => (stepK p.1).rnDeriv refnode p.2) (νk.prod refnode) := hfiber.2 exact rnDeriv_compProd_prod_sigmaFinite_of_fiber_ac chain νk refnode stepK (M.prefixDensityProduct ref s k) hchain_ac hfiber.1 hfiber_meas (ih hkprev) rw [hchainSucc, hrefSucc, EventuallyEq, hext_emb.ae_map_iff] filter_upwards [hext_emb.rnDeriv_map (chain ⊗ₘ stepK) (νk.prod refnode), hcore] with p hmap hp rw [hmap, hp] dsimp [ext, stepK, node] have hpair := M.valuesUnionEquiv_extendObsPrefix hkc p have hproj_ext : valuesProjection (M.prefixNodes_mono (Nat.le_succ k)) (M.extendObsPrefix hkc p) = p.1 := by funext i have hi := congrArg (fun q => q.1 i) hpair exact hi have hcoord_ext : M.extendObsPrefix hkc p ⟨(M.observedAt ⟨k, hkc⟩).val, by rw [M.prefixNodes_succ hkc] exact mem_union_right _ (mem_singleton_self _)⟩ = p.2 := by have hnext := congrArg (fun q => singletonValue (α := swigΩ Ω) (v := (M.observedAt ⟨k, hkc⟩).val) q.2) hpair exact hnext rw [prefixDensityProduct] simp [hkc, hproj_ext, hcoord_ext, refnode] rfl -
qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback_of_jointReflemma — RN-derivative transport for qFactorProduct, assuming the final reference transport has already been identified.hypothesesM :SCM N Ωref :s :M.FixedValueshref :∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :Proof (Lean source)
lemma qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback_of_jointRef (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) (href : (jointRef ref (M.prefixNodes M.observed.card)).map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) = jointRef ref M.observed) [∀ 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Ω Ω))] : (M.qFactorProduct s).rnDeriv (jointRef ref M.observed) =ᵐ[jointRef ref M.observed] fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x) := by classical set e := valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _)) with he have hf : MeasurableEmbedding (e : ValuesOn (M.prefixNodes M.observed.card) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) := e.measurableEmbedding have hq : M.qFactorProduct s = (M.obsChainKernel M.observed.card (le_refl _) s).map e := by rw [qFactorProduct, ProbabilityTheory.Kernel.map_apply _ e.measurable] rw [hq, ← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hf.rnDeriv_map (M.obsChainKernel M.observed.card (le_refl _) s) (jointRef ref (M.prefixNodes M.observed.card))] with y hy simpa using hy -
qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullbacklemma — Peel the final qFactorProduct map back to the full prefix chain kernel.hypothesesM :SCM N Ωref :s :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :Proof (Lean source)
lemma qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) [∀ 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Ω Ω))] : (M.qFactorProduct s).rnDeriv (jointRef ref M.observed) =ᵐ[jointRef ref M.observed] fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x) := by exact qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback_of_jointRef M ref s (jointRef_prefix_card_map M ref) -
obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefix_inductionlemma — The analytic prefix induction for the density chain rule.hypothesesM :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :hstep :ObsStepFiberRN M ref sProof (Lean source)
lemma obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefix_induction (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ 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Ω Ω))] (hstep : ObsStepFiberRN M ref s) : (M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card)) =ᵐ[jointRef ref (M.prefixNodes M.observed.card)] fun y => M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y) := by exact (obsChainKernel_rnDeriv_eq_prefixDensityProduct M ref hdom s hstep M.observed.card (le_refl _)).trans (Filter.EventuallyEq.of_eq (funext (prefixDensityProduct_card_eq_qFactorDensityProduct M ref s))) -
obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefixlemma — Prefix-level analytic chain rule at the full observed prefix.hypothesesM :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :hstep :ObsStepFiberRN M ref sProof (Lean source)
lemma obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ 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Ω Ω))] (hstep : ObsStepFiberRN M ref s) : (M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card)) =ᵐ[jointRef ref (M.prefixNodes M.observed.card)] fun y => M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y) := by exact obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefix_induction M ref hdom s hstep -
obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct_of_prefixlemma — Push the full-prefix a.e. density identity forward, assuming the reference transport and prefix-level chain rule.hypothesesM :SCM N Ωref :s :M.FixedValueshref :∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :Proof (Lean source)
lemma obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct_of_prefix (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) (href : (jointRef ref (M.prefixNodes M.observed.card)).map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) = jointRef ref M.observed) [∀ 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Ω Ω))] (hprefix : (M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card)) =ᵐ[jointRef ref (M.prefixNodes M.observed.card)] fun y => M.qFactorDensityProduct ref s ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) y)) : (fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x)) =ᵐ[jointRef ref M.observed] M.qFactorDensityProduct ref s := by classical set e := valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _)) with he have hf : MeasurableEmbedding (e : ValuesOn (M.prefixNodes M.observed.card) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) := e.measurableEmbedding rw [← href, EventuallyEq, hf.ae_map_iff] filter_upwards [hprefix] with y hy simpa using hy -
obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProductlemma — Push the full-prefix a.e. density identity forward to observed coordinates.hypothesesM :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :hstep :ObsStepFiberRN M ref sProof (Lean source)
lemma obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ 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Ω Ω))] (hstep : ObsStepFiberRN M ref s) : (fun x => ((M.obsChainKernel M.observed.card (le_refl _) s).rnDeriv (jointRef ref (M.prefixNodes M.observed.card))) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).symm x)) =ᵐ[jointRef ref M.observed] M.qFactorDensityProduct ref s := by exact obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct_of_prefix M ref s (jointRef_prefix_card_map M ref) (obsChainKernel_card_rnDeriv_eq_qFactorDensityProduct_prefix M ref hdom s hstep) -
qFactorProduct_rnDeriv_eq_qFactorDensityProducttheorem — Analytic chain rule for the mapped observational product kernel.hypothesesM :SCM N Ωref :hdom :DominatedObs M refs :M.FixedValues∀ s' :M.FixedValues, IsFiniteMeasure (M.obsKernel s')∀ (k : ℕ) (hk : k < M.observed.card),∀ (k : ℕ) (hk : k < M.observed.card),∀ k :hstep :ObsStepFiberRN M ref sProof (Lean source)
theorem qFactorProduct_rnDeriv_eq_qFactorDensityProduct (M : SCM N Ω) (ref : ReferenceMeasures Ω) (hdom : DominatedObs M ref) (s : M.FixedValues) [∀ 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Ω Ω))] (hstep : ObsStepFiberRN M ref s) : (M.qFactorProduct s).rnDeriv (jointRef ref M.observed) =ᵐ[jointRef ref M.observed] M.qFactorDensityProduct ref s := by exact (qFactorProduct_rnDeriv_eq_obsChainKernel_card_pullback M ref s).trans (obsChainKernel_card_rnDeriv_pullback_eq_qFactorDensityProduct M ref hdom s hstep)
CComponentDensity 2 core · 1 supporting The joint observational density is a *scalar* product of one-node conditional densities (qFactorDensityProduct). ★ qFactorDensityProduct_eq_prod_cComponentFactor
c-component regrouping of the chain-rule density
The joint observational density is a scalar product of one-node conditional
densities (qFactorDensityProduct). Because scalar multiplication is
commutative, that product can be regrouped by c-component: collect the factors
whose node lies in each c-component of the graph. This regrouping is exactly the
step that has no kernel-composition analogue — composed kernels cannot be
permuted to bring a non-contiguous c-component's factors together, but scalar
density factors can.
This file performs the regrouping (qFactorDensityProduct_eq_prod_cComponentFactor)
and isolates the per-component scalar factor cComponentDensityFactor, which the
next layer identifies with Tian's Q[C] density.
The per-c-component density factor: the product of the one-node conditional density factors over exactly the observed nodes lying in the c-component C. This is the density-side analogue of Tian's c-factor Q[C].
Definition (Lean source)
c-component regrouping of the chain-rule density product. For a structural causal model M, a reference measure family ref, a fixed assignment s, and a value assignment x to the observed coordinates, the product of all one-node conditional density factors equals the product, over the c-components of the graph, of the per-component density factors.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
cComponentDensityFactor_heq_of_obsKernel_heqlemma — Cross-model c-component density-factor transport. If two structural causal models share the same SWIG graph and have heterogeneously-equal observational kernels, then every c-component density factor recovered from the observational chain-rule density is heterogeneously equal across the two models.hypothesesM₁ M₂ :SCM N Ωref :hsg :M₁.toSWIGGraph = M₂.toSWIGGraphhobs :HEq M₁.obsKernel M₂.obsKernel∀ s' :M₁.FixedValues, IsFiniteMeasure (M₁.obsKernel s')∀ (k : ℕ) (hk : k < M₁.observed.card),∀ (k : ℕ) (hk : k < M₁.observed.card),∀ k :∀ s' :M₂.FixedValues, IsFiniteMeasure (M₂.obsKernel s')∀ (k : ℕ) (hk : k < M₂.observed.card),∀ (k : ℕ) (hk : k < M₂.observed.card),∀ k :conclusionHEq (fun s => M₁.cComponentDensityFactor ref s C) (fun s => M₂.cComponentDensityFactor ref s C)Proof (Lean source)
lemma cComponentDensityFactor_heq_of_obsKernel_heq (M₁ M₂ : SCM N Ω) (ref : ReferenceMeasures Ω) (C : Finset (SWIGNode N)) (hsg : M₁.toSWIGGraph = M₂.toSWIGGraph) (hobs : HEq M₁.obsKernel M₂.obsKernel) [∀ 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Ω Ω))] [∀ 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Ω Ω))] : HEq (fun s => M₁.cComponentDensityFactor ref s C) (fun s => M₂.cComponentDensityFactor ref s C) := by 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₂ have hk : _ = _ := eq_of_heq hobs apply heq_of_eq funext s x unfold cComponentDensityFactor congr 1 funext i unfold obsStepCondDensity obsStepCondKernel SCM.obsCondKernel SCM.obsCondPairKernel repeat' congr
PiUnion 3 core · 5 supporting For disjoint node sets A and B, the canonical measurable equivalence valuesUnionEquiv : ValuesOn (A ∪ B) ≃ᵐ ValuesOn A × ValuesOn B carries the finite product reference measure on A ∪ B to the product of the references o ★ measurePreserving_valuesUnionEquiv
Product measure over a disjoint union of value coordinates
For disjoint node sets A and B, the canonical measurable equivalence
valuesUnionEquiv : ValuesOn (A ∪ B) ≃ᵐ ValuesOn A × ValuesOn B carries the
finite product reference measure on A ∪ B to the product of the references on
A and on B. In other words Measure.pi over a disjoint union is the product
of the two Measure.pi's. This is the reference-splitting fact that lets the
density chain rule peel off one coordinate at a time.
The proof routes the project's union equivalence through Mathlib's
sumPiEquivProdPi (the value reindexing along the Sum decomposition of the
union index) and piCongrLeft (the index reindexing), both measure-preserving.
Override the coordinates in W of an assignment on I, leaving the other coordinates unchanged.
The index equivalence {a ∈ A} ⊕ {b ∈ B} ≃ {i ∈ A ∪ B} for disjoint A, B.
Definition (Lean source)
Measure.pi splits over a disjoint union. Given a family of σ-finite reference measures μ, one per coordinate, together with two finite index sets A and B assumed disjoint, the canonical equivalence carrying value assignments on A ∪ B to pairs of assignments on A and on B is measure-preserving from the product reference measure on A ∪ B to the product of the component reference measures on A and on B.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
instFintypeValuesOnSwigΩinstance — Value assignments on finite SWIG-node sets are finite when each base node value space is finite.instance instFintypeValuesOnSwigΩ [∀ n, Fintype (Ω n)] (I : Finset (SWIGNode N)) : Fintype (ValuesOn I (swigΩ Ω)) := by classical haveI : ∀ v : SWIGNode N, Fintype (swigΩ Ω v) | .random _ => inferInstance | .fixed _ => inferInstance infer_instance -
overrideOn_memlemma — On overridden coordinates, overrideOn reads from the replacement assignment.Proof (Lean source)
@[simp] lemma overrideOn_mem {I W : Finset (SWIGNode N)} (x : ValuesOn I (swigΩ Ω)) (y : ValuesOn W (swigΩ Ω)) (i : {i // i ∈ I}) (hiW : i.val ∈ W) : overrideOn x y i = y ⟨i.val, hiW⟩ := by simp [overrideOn, hiW] -
overrideOn_notMemlemma — Away from overridden coordinates, overrideOn keeps the original assignment.Proof (Lean source)
@[simp] lemma overrideOn_notMem {I W : Finset (SWIGNode N)} (x : ValuesOn I (swigΩ Ω)) (y : ValuesOn W (swigΩ Ω)) (i : {i // i ∈ I}) (hiW : i.val ∉ W) : overrideOn x y i = x i := by simp [overrideOn, hiW] -
overrideOn_overrideOnlemma — Re-overriding the same coordinate set keeps the last replacement assignment.hypothesesconclusionProof (Lean source)
@[simp] lemma overrideOn_overrideOn {I W : Finset (SWIGNode N)} (x : ValuesOn I (swigΩ Ω)) (y z : ValuesOn W (swigΩ Ω)) : overrideOn (overrideOn x y) z = overrideOn x z := by funext i by_cases hiW : i.val ∈ W · simp [overrideOn, hiW] · simp [overrideOn, hiW] -
valuesProjection_overrideOnlemma — Projecting an override back to the overridden coordinates returns the replacement assignment.hypothesesconclusionvaluesProjection hWI (overrideOn x y) = yProof (Lean source)
@[simp] lemma valuesProjection_overrideOn {I W : Finset (SWIGNode N)} (hWI : W ⊆ I) (x : ValuesOn I (swigΩ Ω)) (y : ValuesOn W (swigΩ Ω)) : valuesProjection hWI (overrideOn x y) = y := by funext i exact overrideOn_mem x y ⟨i.val, hWI i.property⟩ i.property
QMass 5 core · 12 supporting This file develops the finite mass identities behind the density route to ID. ★ qLocalMass_marginalize_ancestralClosed★ qLocalMass_prod_of_latentBlock_disjoint★ obsKernel_marginal_singleton_eq_prod_qLocalMass★ doObsKernelAncestralMarginal_positiveMass
Local q-masses for ID density factorization
This file develops the finite mass identities behind the density route to ID.
The central definition is qLocalMass, the latent-product mass of satisfying
local consistency on a chosen observed node set. The file proves elimination
and marginalization lemmas for local q-masses, factors local consistency events
over disjoint latent blocks, and derives the c-component factorization
obsKernel_marginal_singleton_eq_prod_qLocalMass for observed marginal atoms.
It also supplies the positivity bridge
doObsKernelAncestralMarginal_positiveMass for do-model ancestral marginals and
the pure ENNReal telescope prod_filter_div_telescope, both used by the Tian
district-density recovery in QFactor.
The latent-product mass of satisfying local consistency on an observed subset.
For a set of observed nodes T and a subset W of T such that every parent, within T, of a node in W also lies in W, marginalizing the local q-mass on T over the coordinates in T \ W yields the local q-mass on W.
Formal statement
Proof (Lean source)
For a finite family 𝒞 of observed node sets whose latent parent blocks are pairwise disjoint, the local q-mass on the union of the family equals the product, over the members U of 𝒞, of the local q-mass on U.
Formal statement
Proof (Lean source)
For a set of observed nodes P that is closed under observed parents, the singleton mass of the projection of the observational law onto P equals the product, over the full c-components C of the graph, of the local q-mass on C ∩ P.
Formal statement
Proof (Lean source)
For an intervention set X whose random copies are observed and whose fixed copies are not already frozen, a positive observational kernel at every fixed-value assignment, and an outcome set Y disjoint from the random copies of X, the do(X)-law ancestral marginal kernel used in the identification density assembly also has everywhere-positive point mass.
Formal statement
Proof (Lean source)
12 supporting declarations (lemmas, instances)
-
qLocalMass_emptylemma — The empty local q-mass is one.hypothesesconclusionM.qLocalMass s ∅ (by simp) x = 1Proof (Lean source)
@[simp] lemma qLocalMass_empty (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s ∅ (by simp) x = 1 := by simp [qLocalMass] -
qLocalMass_antilemma — Local q-mass is antitone in the constrained observed set.hypothesesconclusionM.qLocalMass s T' hT' x ≤ M.qLocalMass s T hT xProof (Lean source)
lemma qLocalMass_anti (M : SCM N Ω) (s : M.FixedValues) {T T' : Finset (SWIGNode N)} (hTT' : T ⊆ T') (hT : T ⊆ M.observed) (hT' : T' ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s T' hT' x ≤ M.qLocalMass s T hT x := by apply MeasureTheory.measure_mono intro ℓ hℓ v hv exact hℓ v (hTT' hv) -
marginalizeOn_emptylemma — Marginalizing a mass function over an empty set of observed coordinates leaves its value at every observed assignment unchanged.Proof (Lean source)
lemma marginalizeOn_empty [∀ n, Fintype (Ω n)] (M : SCM N Ω) (q : ValuesOn M.observed (swigΩ Ω) → ENNReal) (x : ValuesOn M.observed (swigΩ Ω)) : marginalizeOn M.observed ∅ (by simp) q x = q x := by classical unfold marginalizeOn let y0 : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω) := fun i => elim (notMem_empty i.val i.property) rw [Finset.sum_eq_single y0] · congr funext i simp · intro y _hy hy exact (hy (Subsingleton.elim y y0)).elim · intro hy exact (hy (Finset.mem_univ y0)).elim -
qLocalMass_sum_point_eliminatelemma — Summing a local q-mass over one childless observed coordinate removes that coordinate from the constrained set.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N Ωs :M.FixedValueshT :T ⊆ M.observedv :SWIGNode NhvT :v ∈ ThNoChild :∀ w ∈ T, ¬ M.dag.edge v wconclusion(∑ ω : swigΩ Ω v, M.qLocalMass s T hT (overrideOn x (singletonValuePt v ω)))= M.qLocalMass s (T.erase v) (fun _ hv => hT (mem_of_mem_erase hv)) xProof (Lean source)
lemma qLocalMass_sum_point_eliminate [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (T : Finset (SWIGNode N)) (hT : T ⊆ M.observed) {v : SWIGNode N} (hvT : v ∈ T) (hNoChild : ∀ w ∈ T, ¬ M.dag.edge v w) (x : ValuesOn M.observed (swigΩ Ω)) : (∑ ω : swigΩ Ω v, M.qLocalMass s T hT (overrideOn x (singletonValuePt v ω))) = M.qLocalMass s (T.erase v) (fun _ hv => hT (mem_of_mem_erase hv)) x := by classical let Erest : Set M.LatentValues := {ℓ | ∀ w (hw : w ∈ T.erase v), M.localConsistent s x w (hT (mem_of_mem_erase hw)) ℓ} let Fset : swigΩ Ω v → Set M.LatentValues := fun ω => {ℓ | localStructValue M s x v (hT hvT) ℓ = ω} have hevent : ∀ ω : swigΩ Ω v, {ℓ : M.LatentValues | ∀ w (hw : w ∈ T), M.localConsistent s (overrideOn x (singletonValuePt v ω)) w (hT hw) ℓ} = Erest ∩ Fset ω := by intro ω simpa [Erest, Fset] using qLocalEvent_override_singleton_eq_inter M s hT hvT hNoChild x ω have hdisj : PairwiseDisjoint (↑(Finset.univ : Finset (swigΩ Ω v))) (fun ω => Erest ∩ Fset ω) := by intro ω₁ _ ω₂ _ hne change Disjoint (Erest ∩ Fset ω₁) (Erest ∩ Fset ω₂) rw [Set.disjoint_left] intro ℓ hℓ₁ hℓ₂ exact hne (hℓ₁.2.symm.trans hℓ₂.2) have hmeas : ∀ ω ∈ (Finset.univ : Finset (swigΩ Ω v)), MeasurableSet (Erest ∩ Fset ω) := by intro ω _hω exact Set.Finite.measurableSet (Set.toFinite _) have hunion : (⋃ ω ∈ (Finset.univ : Finset (swigΩ Ω v)), Erest ∩ Fset ω) = Erest := by ext ℓ simp [Fset] simp only [qLocalMass] calc (∑ ω : swigΩ Ω v, M.latentProduct {ℓ : M.LatentValues | ∀ w (hw : w ∈ T), M.localConsistent s (overrideOn x (singletonValuePt v ω)) w (hT hw) ℓ}) = ∑ ω : swigΩ Ω v, M.latentProduct (Erest ∩ Fset ω) := by refine Finset.sum_congr rfl ?_ intro ω _hω rw [hevent ω] _ = M.latentProduct (⋃ ω ∈ (Finset.univ : Finset (swigΩ Ω v)), Erest ∩ Fset ω) := by symm simpa using (MeasureTheory.measure_biUnion_finset (μ := M.latentProduct) (s := (Finset.univ : Finset (swigΩ Ω v))) (f := fun ω => Erest ∩ Fset ω) hdisj hmeas) _ = M.latentProduct Erest := by rw [hunion] -
latentProduct_singleton_eq_prodlemma — The latent-product mass of a singleton latent assignment equals the product of the singleton masses assigned by the latent distributions at every unobserved node.hypothesesProof (Lean source)
lemma latentProduct_singleton_eq_prod [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (ℓ₀ : M.LatentValues) : M.latentProduct ({ℓ₀} : Set M.LatentValues) = ∏ u : {u // u ∈ M.unobserved}, M.latentDist u ({ℓ₀ u} : Set (swigΩ Ω u.val)) := by classical haveI : ∀ u : {u // u ∈ M.unobserved}, IsProbabilityMeasure (M.latentDist u) := M.isProbability_latent haveI : ∀ u : {u // u ∈ M.unobserved}, SigmaFinite (M.latentDist u) := fun _ => inferInstance unfold SCM.latentProduct have hsingleton : ({ℓ₀} : Set M.LatentValues) = Set.univ.pi (fun u => ({ℓ₀ u} : Set (swigΩ Ω u.val))) := by ext ℓ simp [Set.mem_pi, funext_iff] rw [hsingleton, MeasureTheory.Measure.pi_pi] -
measurableSet_comap_piFinset_of_dependslemma — A set of finite product outcomes whose membership depends only on a specified finite set of coordinates is measurable with respect to the σ-algebra on those coordinates.hypothesesι :∀ i, MeasurableSpace (α i)∀ i, Fintype (α i)∀ i, MeasurableSingletonClass (α i)S :Finset ιA :Set (∀ i, α i)hdep :∀ ξ ξ'if(∀ i (_hi : i ∈ S), ξ i = ξ' i)then(ξ ∈ A ↔ ξ' ∈ A)conclusionProof (Lean source)
lemma measurableSet_comap_piFinset_of_depends {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, MeasurableSpace (α i)] [∀ i, Fintype (α i)] [∀ i, MeasurableSingletonClass (α i)] (S : Finset ι) (A : Set (∀ i, α i)) (hdep : ∀ ξ ξ', (∀ i (_hi : i ∈ S), ξ i = ξ' i) → (ξ ∈ A ↔ ξ' ∈ A)) : MeasurableSet[ comap (fun ξ : (∀ i, α i) => fun i : S => ξ i) inferInstance] A := by let B : Set (∀ i : S, α i.val) := {η | ∃ ξ ∈ A, (fun i : S => ξ i) = η} refine ⟨B, Set.Finite.measurableSet B.toFinite, ?_⟩ ext ξ change ξ ∈ ((fun ξ : (∀ i, α i) => fun i : S => ξ i) ⁻¹' B) ↔ ξ ∈ A constructor · rintro ⟨ξ', hξ'A, hξ'⟩ exact (hdep ξ' ξ (by intro i hi exact congrFun hξ' ⟨i, hi⟩)).mp hξ'A · intro hξA exact ⟨ξ, hξA, rfl⟩ -
localConsistent_depends_only_on_latentBlock_of_memlemma — Local consistency at an observed node in a node set is unchanged when two latent assignments agree on every unobserved parent of a node in that set.hypothesesM :SCM N Ωs :M.FixedValuesv :SWIGNode NhvU :v ∈ Uhv :v ∈ M.observedℓ ℓ' :M.LatentValueshℓ :∀ u (hu : u ∈ M.latentBlock U),ℓ ⟨u, (Finset.mem_filter.mp hu).1⟩ = ℓ' ⟨u, (Finset.mem_filter.mp hu).1⟩conclusionM.localConsistent s x v hv ℓ ↔ M.localConsistent s x v hv ℓ'Proof (Lean source)
lemma localConsistent_depends_only_on_latentBlock_of_mem (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) {U : Finset (SWIGNode N)} {v : SWIGNode N} (hvU : v ∈ U) (hv : v ∈ M.observed) (ℓ ℓ' : M.LatentValues) (hℓ : ∀ u (hu : u ∈ M.latentBlock U), ℓ ⟨u, (Finset.mem_filter.mp hu).1⟩ = ℓ' ⟨u, (Finset.mem_filter.mp hu).1⟩) : M.localConsistent s x v hv ℓ ↔ M.localConsistent s x v hv ℓ' := by unfold localConsistent set j : Fin M.observed.card := M.observedIndex ⟨v, hv⟩ with hj have hat : (M.observedAt j).val = v := by rw [hj] exact M.observedAt_observedIndex ⟨v, hv⟩ have hfun : M.structFun (M.observedAt j) (fun w => M.parentMap s ℓ j.isLt (prevFromObservedValues M x) w) = M.structFun (M.observedAt j) (fun w => M.parentMap s ℓ' j.isLt (prevFromObservedValues M x) w) := by congr 1 funext w by_cases huo : w.val ∈ M.unobserved · rw [parentMap_unobserved M s ℓ j.isLt _ w huo, parentMap_unobserved M s ℓ' j.isLt _ w huo] have hedge_v : M.dag.edge w.val v := by have hedge_at : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property simpa [hat] using hedge_at have huBlock : w.val ∈ M.latentBlock U := by rw [latentBlock, mem_filter] exact ⟨huo, ⟨v, hvU, hedge_v⟩⟩ exact hℓ w.val huBlock · by_cases hfix : w.val ∈ M.fixed · rw [parentMap_fixed M s ℓ j.isLt _ w hfix, parentMap_fixed M s ℓ' j.isLt _ w hfix] · have hedge : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo rw [parentMap_observed M s ℓ j.isLt _ w hobs, parentMap_observed M s ℓ' j.isLt _ w hobs] subst j change ((M.observedAt_observedIndex ⟨v, hv⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v, hv⟩)) (fun w => M.parentMap s ℓ (M.observedIndex ⟨v, hv⟩).isLt (prevFromObservedValues M x) w) = x ⟨v, hv⟩) ↔ ((M.observedAt_observedIndex ⟨v, hv⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v, hv⟩)) (fun w => M.parentMap s ℓ' (M.observedIndex ⟨v, hv⟩).isLt (prevFromObservedValues M x) w) = x ⟨v, hv⟩) rw [hfun] -
localConsistent_event_eq_component_biInterlemma — For an observed-parent-closed node set, local consistency at all of its nodes is equivalent to local consistency within each of its confounded components.hypothesesconclusion{ℓ : M.LatentValues | ∀ v (hv : v ∈ P), M.localConsistent s x v (hP.1 hv) ℓ}= ⋂ C ∈ M.toSWIGGraph.cComponentSet, {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ}Proof (Lean source)
lemma localConsistent_event_eq_component_biInter (M : SCM N Ω) (s : M.FixedValues) (P : Finset (SWIGNode N)) (hP : M.ObsParentClosed P) (x : ValuesOn M.observed (swigΩ Ω)) : {ℓ : M.LatentValues | ∀ v (hv : v ∈ P), M.localConsistent s x v (hP.1 hv) ℓ} = ⋂ C ∈ M.toSWIGGraph.cComponentSet, {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ} := by classical ext ℓ constructor · intro hℓ rw [Set.mem_iInter] intro C rw [Set.mem_iInter] intro _hC v hv exact hℓ v (mem_of_mem_inter_right hv) · intro hℓ v hvP rw [Set.mem_iInter] at hℓ have hC : M.toSWIGGraph.cComponentOf v ∈ M.toSWIGGraph.cComponentSet := by rw [SWIGGraph.cComponentSet, mem_image] exact ⟨v, hP.1 hvP, rfl⟩ have hvC : v ∈ M.toSWIGGraph.cComponentOf v := M.toSWIGGraph.mem_cComponentOf_self (hP.1 hvP) have hℓC := hℓ (M.toSWIGGraph.cComponentOf v) rw [Set.mem_iInter] at hℓC exact hℓC hC v (Finset.mem_inter.mpr ⟨hvC, hvP⟩) -
localConsistent_event_eq_family_biInterlemma — For a finite family of observed node sets, local consistency over their union is equivalent to local consistency over every member of the family.hypothesesconclusion{ℓ : M.LatentValues | ∀ v (hv : v ∈ 𝒞.sup id), M.localConsistent s x v (hSup hv) ℓ}= ⋂ U ∈ 𝒞, if hU : U ∈ 𝒞 then {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U hU hv) ℓ} else univProof (Lean source)
lemma localConsistent_event_eq_family_biInter (M : SCM N Ω) (s : M.FixedValues) (𝒞 : Finset (Finset (SWIGNode N))) (h𝒞obs : ∀ U ∈ 𝒞, U ⊆ M.observed) (hSup : 𝒞.sup id ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : {ℓ : M.LatentValues | ∀ v (hv : v ∈ 𝒞.sup id), M.localConsistent s x v (hSup hv) ℓ} = ⋂ U ∈ 𝒞, if hU : U ∈ 𝒞 then {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U hU hv) ℓ} else univ := by classical ext ℓ constructor · intro hℓ rw [Set.mem_iInter] intro U rw [Set.mem_iInter] intro hU simp [hU] intro v hv have hvSup : v ∈ 𝒞.sup id := by rw [mem_sup] exact ⟨U, hU, hv⟩ convert hℓ v hvSup using 1 · intro hℓ v hvSup rw [Set.mem_iInter] at hℓ rw [mem_sup] at hvSup rcases hvSup with ⟨U, hU, hvU⟩ have hℓU := hℓ U rw [Set.mem_iInter] at hℓU have hUevent : ℓ ∈ {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U hU hv) ℓ} := by simpa [hU] using hℓU hU convert hUevent v hvU using 1 -
qLocalMass_prod_inter_of_latentBlock_disjointlemma — Local q-mass on a covered set factors over an abstract family after intersecting each family member with the covered set.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N Ωs :M.FixedValueshPobs :P ⊆ M.observedh𝒞obs :∀ U ∈ 𝒞, U ⊆ M.observedhcover :P ⊆ 𝒞.sup idhblock :conclusionM.qLocalMass s P hPobs x= ∏ U ∈ 𝒞, if hU : U ∈ 𝒞 then M.qLocalMass s (U ∩ P) (fun _ hv => h𝒞obs U hU (mem_of_mem_inter_left hv)) x else 1Proof (Lean source)
lemma qLocalMass_prod_inter_of_latentBlock_disjoint [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (P : Finset (SWIGNode N)) (hPobs : P ⊆ M.observed) (𝒞 : Finset (Finset (SWIGNode N))) (h𝒞obs : ∀ U ∈ 𝒞, U ⊆ M.observed) (hcover : P ⊆ 𝒞.sup id) (hblock : (↑𝒞 : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U'))) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s P hPobs x = ∏ U ∈ 𝒞, if hU : U ∈ 𝒞 then M.qLocalMass s (U ∩ P) (fun _ hv => h𝒞obs U hU (mem_of_mem_inter_left hv)) x else 1 := by classical let E : Finset (SWIGNode N) → Set M.LatentValues := fun U => if hU : U ∈ 𝒞 then {ℓ : M.LatentValues | ∀ v (hv : v ∈ U ∩ P), M.localConsistent s x v (h𝒞obs U hU (mem_of_mem_inter_left hv)) ℓ} else Set.univ have hevent : {ℓ : M.LatentValues | ∀ v (hv : v ∈ P), M.localConsistent s x v (hPobs hv) ℓ} = ⋂ U ∈ 𝒞, E U := by ext ℓ constructor · intro hℓ rw [Set.mem_iInter] intro U rw [Set.mem_iInter] intro hU simp [E, hU] intro v _hvU hvP exact hℓ v hvP · intro hℓ v hvP rw [Set.mem_iInter] at hℓ have hvSup : v ∈ 𝒞.sup id := hcover hvP rw [mem_sup] at hvSup rcases hvSup with ⟨U, hU, hvU⟩ have hℓU := hℓ U rw [Set.mem_iInter] at hℓU have hUevent : ℓ ∈ {ℓ : M.LatentValues | ∀ v (hv : v ∈ U ∩ P), M.localConsistent s x v (h𝒞obs U hU (mem_of_mem_inter_left hv)) ℓ} := by simpa [E, hU] using hℓU hU have hvUP : v ∈ U ∩ P := Finset.mem_inter.mpr ⟨hvU, hvP⟩ convert hUevent v hvUP using 1 have hcoord : iIndepFun (fun u : {u // u ∈ M.unobserved} => fun ℓ : M.LatentValues => ℓ u) M.latentProduct := by haveI : ∀ u : {u // u ∈ M.unobserved}, IsProbabilityMeasure (M.latentDist u) := M.isProbability_latent unfold SCM.latentProduct exact ProbabilityTheory.iIndepFun_pi (X := fun _ : {u // u ∈ M.unobserved} => id) (fun _ => aemeasurable_id) have hfactor : ∀ S : Finset (Finset (SWIGNode N)), S ⊆ 𝒞 → M.latentProduct (⋂ U ∈ S, E U) = ∏ U ∈ S, M.latentProduct (E U) := by intro S refine Finset.induction_on S ?base ?step · intro _hS simp [E] · intro U S hUnot ih hSinsert have hS : S ⊆ 𝒞 := by intro V hV exact hSinsert (mem_insert_of_mem hV) have hU : U ∈ 𝒞 := hSinsert (mem_insert_self U S) have hdisj : Disjoint (S.biUnion (latentBlockIndex M)) (latentBlockIndex M U) := latentBlockIndex_biUnion_disjoint_of_pairwise M hS hU hUnot hblock have hindep : IndepFun (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) M.latentProduct := hcoord.indepFun_finset (S.biUnion (latentBlockIndex M)) (latentBlockIndex M U) hdisj (fun u => measurable_pi_apply u) have hmeasS : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) inferInstance] (⋂ V ∈ S, E V) := by refine measurableSet_comap_piFinset_of_depends (S := S.biUnion (latentBlockIndex M)) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ rw [Set.mem_iInter] at hℓ rw [Set.mem_iInter] intro V have hℓV := hℓ V rw [Set.mem_iInter] at hℓV rw [Set.mem_iInter] intro hVS have hV𝒞 : V ∈ 𝒞 := hS hVS simp [E, hV𝒞] intro v hvV hvP have hlocal : M.localConsistent s x v (h𝒞obs V hV𝒞 hvV) ℓ := by have hEV : ℓ ∈ E V := hℓV hVS have hEV' : ∀ v (hv : v ∈ V ∩ P), M.localConsistent s x v (h𝒞obs V hV𝒞 (mem_of_mem_inter_left hv)) ℓ := by simpa [E, hV𝒞] using hEV exact hEV' v (Finset.mem_inter.mpr ⟨hvV, hvP⟩) exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvV (h𝒞obs V hV𝒞 hvV) ℓ ℓ' (by intro u hu have hmemBlock : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M V := (mem_latentBlockIndex_iff M V _).mpr hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨V, hVS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord)).mp hlocal · intro hℓ' rw [Set.mem_iInter] at hℓ' rw [Set.mem_iInter] intro V have hℓ'V := hℓ' V rw [Set.mem_iInter] at hℓ'V rw [Set.mem_iInter] intro hVS have hV𝒞 : V ∈ 𝒞 := hS hVS simp [E, hV𝒞] intro v hvV hvP have hlocal : M.localConsistent s x v (h𝒞obs V hV𝒞 hvV) ℓ' := by have hEV : ℓ' ∈ E V := hℓ'V hVS have hEV' : ∀ v (hv : v ∈ V ∩ P), M.localConsistent s x v (h𝒞obs V hV𝒞 (mem_of_mem_inter_left hv)) ℓ' := by simpa [E, hV𝒞] using hEV exact hEV' v (Finset.mem_inter.mpr ⟨hvV, hvP⟩) exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvV (h𝒞obs V hV𝒞 hvV) ℓ' ℓ (by intro u hu have hmemBlock : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M V := (mem_latentBlockIndex_iff M V _).mpr hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨V, hVS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord.symm)).mp hlocal have hmeasU : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) inferInstance] (E U) := by refine measurableSet_comap_piFinset_of_depends (S := latentBlockIndex M U) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ simp [E, hU] at hℓ ⊢ intro v hvU hvP have hlocal : M.localConsistent s x v (h𝒞obs U hU hvU) ℓ := hℓ v hvU hvP exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvU (h𝒞obs U hU hvU) ℓ ℓ' (by intro u hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord)).mp hlocal · intro hℓ' simp [E, hU] at hℓ' ⊢ intro v hvU hvP have hlocal : M.localConsistent s x v (h𝒞obs U hU hvU) ℓ' := hℓ' v hvU hvP exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvU (h𝒞obs U hU hvU) ℓ' ℓ (by intro u hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord.symm)).mp hlocal have hinter := hindep.meas_inter (μ := M.latentProduct) hmeasS hmeasU calc M.latentProduct (⋂ V ∈ insert U S, E V) = M.latentProduct ((⋂ V ∈ S, E V) ∩ E U) := by congr 1 ext ℓ simp [E, and_comm] _ = M.latentProduct (⋂ V ∈ S, E V) * M.latentProduct (E U) := by exact hinter _ = (∏ V ∈ S, M.latentProduct (E V)) * M.latentProduct (E U) := by rw [ih hS] _ = ∏ V ∈ insert U S, M.latentProduct (E V) := by rw [Finset.prod_insert hUnot] rw [mul_comm] have hfull := hfactor 𝒞 (fun _ h => h) unfold qLocalMass rw [hevent] rw [hfull] refine Finset.prod_congr rfl ?_ intro U hU simp [E, hU] -
qLocalMass_pos_of_positiveObslemma — Positive observational mass implies nonzero local q-mass.hypothesesconclusion∀ T hT x, M.qLocalMass s T hT x ≠ 0Proof (Lean source)
lemma qLocalMass_pos_of_positiveObs (M : SCM N Ω) (s : M.FixedValues) [MeasurableSingletonClass (ValuesOn M.observed (swigΩ Ω))] (hpos : ID.DiscreteID.PositiveMass (M.obsKernel s)) : ∀ T hT x, M.qLocalMass s T hT x ≠ 0 := by classical intro T hT x have hobs : M.observed ⊆ M.observed := fun ⦃_⦄ hv => hv have hclosed : M.ObsParentClosed M.observed := by refine ⟨hobs, ?_⟩ intro _v _hv _w hw _hedge exact hw have hmass := obsKernel_marginal_singleton_eq_latentProduct_agree M s (P := M.observed) hobs x have hset : {ℓ : M.LatentValues | ∀ v : {v // v ∈ M.observed}, M.evalMap s ℓ ⟨v.val, mem_union_left M.unobserved v.property⟩ = x ⟨v.val, v.property⟩} = {ℓ : M.LatentValues | ∀ v (hv : v ∈ M.observed), M.localConsistent s x v hv ℓ} := by ext ℓ constructor · intro hEval exact (M.evalMap_agree_iff_localConsistent s M.observed hclosed x ℓ).mp (fun v hv => hEval ⟨v, hv⟩) · intro hLocal v exact (M.evalMap_agree_iff_localConsistent s M.observed hclosed x ℓ).mpr hLocal v.val v.property rw [hset] at hmass have hproj_id : (valuesProjection (Ω := swigΩ Ω) hobs : ValuesOn M.observed (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) = id := by funext ξ rfl rw [hproj_id, Measure.map_id] at hmass have hfull : M.qLocalMass s M.observed hobs x ≠ 0 := by have hx : (M.obsKernel s) ({x} : Set (ValuesOn M.observed (swigΩ Ω))) ≠ 0 := by simpa [ID.DiscreteID.singletonMass_apply] using hpos x simpa [qLocalMass] using (hmass ▸ hx) have hle : M.qLocalMass s M.observed hobs x ≤ M.qLocalMass s T hT x := M.qLocalMass_anti s (T := T) (T' := M.observed) hT hT hobs x intro hzero exact hfull (le_antisymm (by simpa [hzero] using hle) zero_le) -
prod_filter_div_telescopelemma — Pure ENNReal telescope for products of selected adjacent ratios.hypothesesa :ℕ → ENNRealm :ℕT :Finset ℕhT :T ⊆ range mhne :∀ i ≤ m, a i ≠ 0hfin :∀ i ≤ m, a i ≠ ⊤hconst :∀ i < mifi ∉ Tthena (i + 1) = a iconclusion∏ i ∈ T, a (i + 1) / a i = a m / a 0Proof (Lean source)
lemma prod_filter_div_telescope (a : ℕ → ENNReal) (m : ℕ) (T : Finset ℕ) (hT : T ⊆ range m) (hne : ∀ i ≤ m, a i ≠ 0) (hfin : ∀ i ≤ m, a i ≠ ⊤) (hconst : ∀ i < m, i ∉ T → a (i + 1) = a i) : ∏ i ∈ T, a (i + 1) / a i = a m / a 0 := by classical have hrange_all : ∀ n : ℕ, (∀ i ≤ n, a i ≠ 0) → (∀ i ≤ n, a i ≠ ⊤) → ∏ i ∈ range n, a (i + 1) / a i = a n / a 0 := by intro n hnne hnfin induction n with | zero => simp [ENNReal.div_self (hnne 0 le_rfl) (hnfin 0 le_rfl)] | succ m ih => rw [Finset.prod_range_succ] have hih : ∏ i ∈ range m, a (i + 1) / a i = a m / a 0 := ih (fun i hi => hnne i (Nat.le_trans hi (Nat.le_succ m))) (fun i hi => hnfin i (Nat.le_trans hi (Nat.le_succ m))) rw [hih] rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv] rw [show a m * (a 0)⁻¹ * (a (m + 1) * (a m)⁻¹) = a (m + 1) * (a m * (a m)⁻¹) * (a 0)⁻¹ by ac_rfl] rw [ENNReal.mul_inv_cancel (hnne m (Nat.le_succ m)) (hnfin m (Nat.le_succ m))] simp have hrange : ∏ i ∈ range m, a (i + 1) / a i = a m / a 0 := hrange_all m hne hfin have hsubset : ∏ i ∈ T, a (i + 1) / a i = ∏ i ∈ range m, a (i + 1) / a i := by exact Finset.prod_subset hT (by intro i hiRange hiT have hi_lt : i < m := Finset.mem_range.mp hiRange rw [hconst i hi_lt hiT] exact ENNReal.div_self (hne i (le_of_lt hi_lt)) (hfin i (le_of_lt hi_lt))) rw [hsubset, hrange]
MechCFactor 6 core · 13 supporting The recovery tianDistrictDensity ν_M S =ᵐ cComponentDensityFactor M S used by the density route for ID soundness is, at bottom, the do(X)-invariance of the c-factor Q[S] for a full c-component S. ★ cComponentDensityFactor_eq_mechCFactor★ mechCFactor_fixSet_invariant
Mechanism c-factor Q[S] and its do(X)-invariance (Tian Lemma 4)
The recovery tianDistrictDensity ν_M S =ᵐ cComponentDensityFactor M S used by
the density route for ID soundness is, at bottom, the do(X)-invariance of the
c-factor Q[S] for a full c-component S. This file isolates the
mechanism-level object carrying that content.
mechCFactor M' S is Tian's Q[S] = P_{v∖s}(s) (Eq. 36): intervene on every
observed node outside S that is not already fixed in M' (its do-complement)
and read off the S-marginal density. The "not already fixed" clause makes the
definition apply to the non-standard do-model M.fixSet X (whose fixed set
is the fixed copies of X), which is what the invariance step compares against.
Decomposition of the recovery:
* cComponentDensityFactor M S = mechCFactor M S — Tian Lemma 1
(Eq. 37 = Eq. 36): the observational full-prefix product is the
do-complement marginal.
* mechCFactor (M.fixSet X) S = mechCFactor M S for c-components avoiding X:
the c-factor is invariant under interventions outside the component.
* tianDistrictDensity ν_M S = mechCFactor (M.fixSet X) S: the district density
in the do-law ancestral marginal is the corresponding mechanism c-factor.
Together these results identify the recovered district density with the observational c-component density used by the ID soundness argument.
Base-node names whose random copy lies in M.observed \ S and whose fixed copy is not already fixed in M — the variables intervened on in Tian's do-complement object Q[S] = P_{v∖s}(s). The "not already fixed" clause lets this apply to non-standard models such as M.fixSet X.
Definition (Lean source)
Fixed-value slice for the do-complement SCM, read from a full observed assignment: keep M's existing fixed slice s and extend it on the do-complement coordinates by projecting x to the random copies in V∖S.
Definition (Lean source)
Tian's Q[S] measure (Eq. 36 / Eq. 55): the do(observed∖S) marginal on S. Intervene on every not-already-fixed observed node outside S, then project the intervened observational law to the coordinates in S.
Definition (Lean source)
The mechanism c-factor density Q[S] as a function of a full observed assignment x: read the do-values for V∖S from x (keeping M's fixed slice s), form the do-complement marginal on S, and take its rnDeriv against the product reference on S, evaluated at the S-projection of x.
Definition (Lean source)
(A) Tian Lemma 1 (Eq. 37 = Eq. 36). For a standard causal model M, i.e. one with no fixed nodes, a reference family that is faithful — every coordinate value has nonzero reference mass, and an observational kernel at a fixed-value slice s with full point-mass support (every observed assignment has nonzero probability), fix a node set S contained in the observed coordinates that is a full c-component of the model's SWIG graph. Then the observational full-prefix c-component density cComponentDensityFactor on S equals the mechanism c-factor Q[S] (mechCFactor) — the do-complement marginal density of S.
Formal statement
Proof (Lean source)
Do(X)-invariance of the c-factor Q[S] (Tian Lemma 4). Let an intervention set X have random copies that are all observed and fixed copies that are not already fixed in the base model, giving the intervened model M.fixSet X. For a standard base model M, a reference family that is faithful, and a node set S contained in the observed coordinates whose random copies avoid every intervened node in X, if the base assignment x records, at each intervened node, the same value that the intervened model's fixed values sDo assign to the corresponding fixed coordinate, then the S-c-factor Q[S] of the intervened model M.fixSet X at sDo, x equals the S-c-factor of the base model M at the projected fixed values M.fixSetProj X sDo, x.
Formal statement
Proof (Lean source)
13 supporting declarations (lemmas, instances)
-
mechComplementNames_random_mem_observedlemma — Every mechanism-complement variable has its random copy among the observed nodes.hypothesesconclusion∀ n ∈ M.mechComplementNames S, SWIGNode.random n ∈ M.observedProof (Lean source)
lemma mechComplementNames_random_mem_observed (M : SCM N Ω) (S : Finset (SWIGNode N)) : ∀ n ∈ M.mechComplementNames S, SWIGNode.random n ∈ M.observed := by intro n hn exact (Finset.mem_sdiff.mp (Finset.mem_filter.mp hn).2.1).1 -
mechComplementNames_fixed_not_memlemma — Every mechanism-complement variable has a fixed copy that is not already fixed.hypothesesconclusion∀ n ∈ M.mechComplementNames S, SWIGNode.fixed n ∉ M.fixedProof (Lean source)
lemma mechComplementNames_fixed_not_mem (M : SCM N Ω) (S : Finset (SWIGNode N)) : ∀ n ∈ M.mechComplementNames S, SWIGNode.fixed n ∉ M.fixed := by intro n hn exact (Finset.mem_filter.mp hn).2.2 -
mechComplementNames_image_random_subset_observedlemma — The random copies of the mechanism-complement variables form a subset of the observed nodes.hypothesesconclusion(M.mechComplementNames S).image SWIGNode.random ⊆ M.observedProof (Lean source)
lemma mechComplementNames_image_random_subset_observed (M : SCM N Ω) (S : Finset (SWIGNode N)) : (M.mechComplementNames S).image SWIGNode.random ⊆ M.observed := by intro v hv rcases Finset.mem_image.mp hv with ⟨n, hn, rfl⟩ exact M.mechComplementNames_random_mem_observed S n hn -
QmechMeasure_singleton_eq_qLocalMasstheorem — The do-complement Q[S] atom equals the local q-mass on S.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N ΩhS :S ⊆ M.observedhfe :∀ n : NifSWIGNode.fixed n ∈ M.fixedthen∀ v : SWIGNode N, ¬ M.dag.edge (SWIGNode.random n) vs :M.FixedValuesconclusionQmechMeasure M S hS (M.mechDoValues S s x) {valuesProjection hS x} = M.qLocalMass s S hS xProof (Lean source)
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 -
standard_fixed_random_edgelesslemmahypothesesM :SCM N ΩhStd :M.isStandardconclusion∀ n : NifSWIGNode.fixed n ∈ M.fixedthen∀ v : SWIGNode N, ¬ M.dag.edge (SWIGNode.random n) vProof (Lean source)
lemma standard_fixed_random_edgeless (M : SCM N Ω) (hStd : M.isStandard) : ∀ n : N, SWIGNode.fixed n ∈ M.fixed → ∀ v : SWIGNode N, ¬ M.dag.edge (SWIGNode.random n) v := by intro n hn rw [SCM.isStandard] at hStd rw [hStd] at hn simp at hn -
prefixNodes_obsParentClosedlemma — The first k observed nodes in a structural causal model's topological order form a set closed under observed parents.Proof (Lean source)
lemma prefixNodes_obsParentClosed (M : SCM N Ω) (k : ℕ) : M.ObsParentClosed (M.prefixNodes k) := by classical refine ⟨M.prefixNodes_subset_observed k, ?_⟩ intro v hv w hwObs hEdge rcases (M.mem_prefixNodes_iff k v).mp hv with ⟨hvObs, hvlt⟩ let i : Fin M.observed.card := M.observedIndex ⟨v, hvObs⟩ have hi_eq : (M.observedAt i).val = v := by exact M.observedAt_observedIndex ⟨v, hvObs⟩ have hwPred : w ∈ M.toSWIGGraph.observedPredecessors (M.observedAt i).val := by rw [hi_eq] exact Finset.mem_filter.mpr ⟨hwObs, M.dag.topoOrder_lt w v hEdge⟩ have hwPrefixI : w ∈ M.prefixNodes i.val := by simpa using ((M.observedPredecessors_observedAt i.isLt).symm ▸ hwPred) exact M.prefixNodes_mono (show i.val ≤ k from le_of_lt hvlt) hwPrefixI -
qLocalMass_ne_toplemma — Every local q-mass associated with fixed values, an observed node set, and an observed assignment is finite. -
div_mul_commonlemma — Cancelling a common nonzero finite factor preserves a quotient of extended nonnegative reals.Proof (Lean source)
lemma ENNReal.div_mul_common {a b r : ENNReal} (hr0 : r ≠ 0) (hrtop : r ≠ ∞) : (a * r) / (b * r) = a / b := by rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul] rw [ENNReal.mul_inv] · rw [show b⁻¹ * r⁻¹ * (a * r) = (r⁻¹ * r) * (b⁻¹ * a) by ac_rfl] rw [ENNReal.inv_mul_cancel hr0 hrtop] simp [mul_comm] · exact inr hrtop · exact inr hr0 -
prod_ne_top_of_ne_toplemma — A finite product of finite extended nonnegative reals is finite.hypothesesconclusion(∏ i ∈ s, f i) ≠ ∞Proof (Lean source)
lemma Finset.prod_ne_top_of_ne_top {ι : Type*} [DecidableEq ι] (s : Finset ι) (f : ι → ENNReal) (hf : ∀ i ∈ s, f i ≠ ∞) : (∏ i ∈ s, f i) ≠ ∞ := by classical induction s using Finset.induction_on with | empty => simp | insert a s ha ih => rw [Finset.prod_insert ha] exact ENNReal.mul_ne_top (hf a (mem_insert_self a s)) (ih (by intro i hi; exact hf i (mem_insert_of_mem hi))) -
prod_div_prodlemma — A finite product of quotients is the quotient of the finite products when denominators are nonzero and finite.hypothesesconclusion(∏ i ∈ t, f i / g i) = (∏ i ∈ t, f i) / (∏ i ∈ t, g i)Proof (Lean source)
lemma ENNReal.prod_div_prod {ι : Type*} [DecidableEq ι] (t : Finset ι) (f g : ι → ENNReal) (hg0 : ∀ i ∈ t, g i ≠ 0) (hgtop : ∀ i ∈ t, g i ≠ ∞) : (∏ i ∈ t, f i / g i) = (∏ i ∈ t, f i) / (∏ i ∈ t, g i) := by classical induction t using Finset.induction_on with | empty => simp | insert a t ha ih => have ih' : (∏ i ∈ t, f i / g i) = (∏ i ∈ t, f i) / (∏ i ∈ t, g i) := ih (by intro i hi; exact hg0 i (mem_insert_of_mem hi)) (by intro i hi; exact hgtop i (mem_insert_of_mem hi)) have hprod0 : (∏ i ∈ t, g i) ≠ 0 := by exact Finset.prod_ne_zero_iff.mpr (by intro i hi exact hg0 i (mem_insert_of_mem hi)) have hprodtop : (∏ i ∈ t, g i) ≠ ∞ := by exact Finset.prod_ne_top_of_ne_top _ g (by intro i hi exact hgtop i (mem_insert_of_mem hi)) rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.prod_insert ha, ih'] rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv] rw [ENNReal.mul_inv] · ac_rfl · exact inr hprodtop · exact inr hprod0 -
mechCFactor_eq_qLocalMass_div_jointReflemmahypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N Ωref :s :M.FixedValueshS :S ⊆ M.observedhref :hfe :∀ n : NifSWIGNode.fixed n ∈ M.fixedthen∀ v : SWIGNode N, ¬ M.dag.edge (SWIGNode.random n) vconclusionM.mechCFactor ref S hS s xProof (Lean source)
lemma mechCFactor_eq_qLocalMass_div_jointRef [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (ref : ReferenceMeasures Ω) (s : M.FixedValues) (S : Finset (SWIGNode N)) (hS : S ⊆ M.observed) (href : ReferenceFaithful ref) (hfe : ∀ n : N, SWIGNode.fixed n ∈ M.fixed → ∀ v : SWIGNode N, ¬ M.dag.edge (SWIGNode.random n) v) (x : ValuesOn M.observed (swigΩ Ω)) : M.mechCFactor ref S hS s x = M.qLocalMass s S hS x / jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) := by have hnum : QmechMeasure M S hS (M.mechDoValues S s x) {valuesProjection hS x} = M.qLocalMass s S hS x := QmechMeasure_singleton_eq_qLocalMass M S hS hfe s x have hden0 : jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) ≠ 0 := jointRef_singleton_ne_zero ref href S (valuesProjection hS x) have hdenTop : 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 M S hS (M.mechDoValues S s x))) (valuesProjection hS x) hden0 hdenTop] rw [hnum] -
component_ref_atom_product_eq_jointReflemma — Multiplying the singleton reference masses for all observed variables in one c-component equals the singleton mass of their joint reference measure.hypotheses∀ n, MeasurableSingletonClass (Ω n)M :SCM N Ωref :hS :S ⊆ M.observedhScomp :S ∈ M.toSWIGGraph.cComponentSetProof (Lean source)
lemma component_ref_atom_product_eq_jointRef [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (ref : ReferenceMeasures Ω) (S : Finset (SWIGNode N)) (hS : S ⊆ M.observed) (hScomp : S ∈ M.toSWIGGraph.cComponentSet) (x : ValuesOn M.observed (swigΩ Ω)) : (∏ i ∈ Finset.univ.filter (fun i : Fin M.observed.card => M.toSWIGGraph.cComponentOf (M.observedAt i).val = S), ref.μ (M.observedAt i).val ({x (M.observedAt i)} : Set (swigΩ Ω (M.observedAt i).val))) = jointRef ref S ({valuesProjection hS x} : Set (ValuesOn S (swigΩ Ω))) := by classical have hprod : (∏ i ∈ Finset.univ.filter (fun i : Fin M.observed.card => M.toSWIGGraph.cComponentOf (M.observedAt i).val = S), ref.μ (M.observedAt i).val ({x (M.observedAt i)} : Set (swigΩ Ω (M.observedAt i).val))) = ∏ v : {v // v ∈ S}, ref.μ v.val ({(valuesProjection hS x) v} : Set (swigΩ Ω v.val)) := by refine Finset.prod_bij (fun i hi => ⟨(M.observedAt i).val, (mem_cComponent_iff_cComponentOf_eq M.toSWIGGraph (M.observedAt i).property hScomp).mpr (Finset.mem_filter.mp hi).2⟩) ?_ ?_ ?_ ?_ · intro i hi exact Finset.mem_univ _ · intro i _hi j _hj hij have hval : (M.observedAt i).val = (M.observedAt j).val := congrArg (fun v : {v // v ∈ S} => v.val) hij have hsub : M.observedAt i = M.observedAt j := Subtype.ext hval calc i = M.observedIndex (M.observedAt i) := (M.observedIndex_observedAt i).symm _ = M.observedIndex (M.observedAt j) := by rw [hsub] _ = j := M.observedIndex_observedAt j · intro v _hv let i : Fin M.observed.card := M.observedIndex ⟨v.val, hS v.property⟩ have hnode : (M.observedAt i).val = v.val := M.observedAt_observedIndex ⟨v.val, hS v.property⟩ refine ⟨i, ?_, ?_⟩ · rw [mem_filter] refine ⟨Finset.mem_univ _, ?_⟩ have hvcomp : M.toSWIGGraph.cComponentOf v.val = S := (mem_cComponent_iff_cComponentOf_eq M.toSWIGGraph (hS v.property) hScomp).mp v.property simpa [hnode] using hvcomp · exact Subtype.ext hnode · intro i hi simp [valuesProjection] rw [jointRef_singleton_eq_prod] exact hprod -
qLocalMass_fixSet_invariantlemma — Local q-mass is invariant under a fixSet intervention when no coordinate in S is one of the intervened random nodes and the full assignment pins each intervened random node to the corresponding fixed value.hypothesesM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedsDo :(M.fixSet X hObs hFix).FixedValueshS :S ⊆ M.observedhSX :∀ n ∈ X, SWIGNode.random n ∉ Shpin :∀ 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⟩)⟩conclusion(M.fixSet X hObs hFix).qLocalMass sDo S (by simpa [fixSet_observed] using hS) x= M.qLocalMass (M.fixSetProj X hObs hFix sDo) S hS xProof (Lean source)
lemma qLocalMass_fixSet_invariant (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (sDo : (M.fixSet X hObs hFix).FixedValues) (S : Finset (SWIGNode N)) (hS : S ⊆ M.observed) (hSX : ∀ n ∈ X, SWIGNode.random n ∉ S) (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).qLocalMass sDo S (by simpa [fixSet_observed] using hS) x = M.qLocalMass (M.fixSetProj X hObs hFix sDo) S hS x := by classical let MX := M.fixSet X hObs hFix let hSXobs : S ⊆ MX.observed := by simpa [MX, fixSet_observed] using hS have hobsAgree : ∀ w (hw : w ∈ M.observed), x ⟨w, by simpa [MX, fixSet_observed] using hw⟩ = x ⟨w, hw⟩ := by intro w hw rfl have hproj : M.fixSetProj X hObs hFix sDo = M.fixSetProj X hObs hFix sDo := rfl unfold qLocalMass congr 1 ext ℓ constructor · intro hLocal v hv have hnot : v ∉ X.image SWIGNode.random := by intro hvX rcases Finset.mem_image.mp hvX with ⟨D, hD, rfl⟩ exact hSX D hD hv exact (localConsistent_fixSet_iff M X hObs hFix sDo (M.fixSetProj X hObs hFix sDo) x x v (hSXobs hv) (hS hv) hnot hobsAgree hpin hproj ℓ).mp (hLocal v hv) · intro hLocal v hv have hnot : v ∉ X.image SWIGNode.random := by intro hvX rcases Finset.mem_image.mp hvX with ⟨D, hD, rfl⟩ exact hSX D hD hv exact (localConsistent_fixSet_iff M X hObs hFix sDo (M.fixSetProj X hObs hFix sDo) x x v (hSXobs hv) (hS hv) hnot hobsAgree hpin hproj ℓ).mpr (hLocal v hv)
CountingReference 3 core · 0 supporting On finite node value spaces the canonical reference family is the per-node counting measure. ★ referenceFaithful_countingRef★ dominatedObs_countingRef
The counting reference measure for finite discrete models
On finite node value spaces the canonical reference family is the per-node
counting measure. It is faithful — every singleton has counting mass one — so,
via absolutelyContinuous_jointRef_of_faithful, every structural causal model
is dominated by it. This supplies the domination half of the general
density-route identification theorem id_sound, whose model class is
DominatedObs · ref ∧ DiscretePositive; the positivity half is supplied by the
standard discrete positive model class.
The counting reference family: each SWIG-node coordinate carries the counting measure. On countable value spaces this is a σ-finite measure.
Definition (Lean source)
The counting reference family is faithful: every singleton coordinate value has counting mass one, in particular nonzero.
Formal statement
Proof (Lean source)
For every structural causal model M, each of its observational laws is absolutely continuous with respect to the counting reference family's product measure, because a faithful reference dominates every measure on a countable coordinate product. Note this holds for all M, with no positivity or graph hypothesis.
Formal statement
Proof (Lean source)
DoLawMarginal 2 core · 0 supporting This file collects foundational facts used to identify the Y-marginal of the do-law from observational densities. ★ obsDensity_heq_of_obsKernel_heq★ obsKernel_heq_of_obsDensity_heq
Foundational helpers for the do-law Y-marginal
This file collects foundational facts used to identify the Y-marginal of the
do-law from observational densities. It currently provides cross-model density
transport: two structural causal models sharing the same SWIG graph and the same
observational kernel also share the same observational density, so densities
transport across models that agree on those data. This is the step that turns the
hypothesis "the two models have the same observational law" into "the two models
have the same observational density", from which the recovered c-factors — and
hence the identifiable do-law Y-marginal — are read off.
Cross-model density transport. If two structural causal models M₁ and M₂ share the same SWIG graph and have heterogeneously-equal observational kernels, then their observational densities are heterogeneously equal. After unifying the SWIG-graph data the observed-value types coincide, the observational kernels become literally equal, and the density is the Radon–Nikodym derivative of that kernel against a fixed reference measure.
Formal statement
Proof (Lean source)
Cross-model law transport (converse). If two structural causal models M₁ and M₂ are each dominated by the same reference measure, share the same SWIG graph, and have heterogeneously-equal observational densities, then their observational kernels are heterogeneously equal. After unifying the SWIG-graph data the observed-value types coincide and the densities become literally equal; weighting the common joint reference by that density recovers each observational law (withDensity_obsDensity_eq), so the two laws agree. This is the converse of obsDensity_heq_of_obsKernel_heq: under dominance, equal density and equal law are interchangeable, letting the kernel-level identification tools be driven from a density hypothesis.
Formal statement
Proof (Lean source)
MassBridge 3 core · 7 supporting This file exposes the measure-level identities that turn Radon--Nikodym derivatives and conditional kernels into singleton-mass ratios on finite measurable-singleton spaces. ★ condDistrib_singleton_mass_eq_conditionalMass★ obsCondKernel_singleton_mass_of_ne_zero★ obsStepCondDensity_eq_mass_ratio
Point-mass bridges for finite discrete densities
This file exposes the measure-level identities that turn Radon--Nikodym derivatives and conditional kernels into singleton-mass ratios on finite measurable-singleton spaces. The statements are reference-measure agnostic: they apply to any faithful finite reference family, not only counting measure.
For a measurable map Y and a measurable map Z out of a finite measure space, at a conditioning value z with nonzero pushforward mass under Z, the singleton mass that Mathlib's conditional distribution condDistrib Y Z μ assigns to a value y at z equals the discrete conditional-mass ratio conditionalMass, computed from the joint pushforward law of (Y, Z), evaluated at (y, z).
Formal statement
Proof (Lean source)
For a query coordinate set Y contained in the observed nodes and a conditioning coordinate set CC contained in the observed nodes, at a conditioning value c with nonzero pushforward mass of the observational kernel under projection onto CC, the observational conditional kernel's singleton mass at a value y equals the observational kernel's joint singleton mass at the pair (c, y) divided by its singleton mass at c.
Formal statement
Proof (Lean source)
At the i-th observed coordinate, if the one-step observational conditional kernel is absolutely continuous with respect to the reference measure on that coordinate, and the reference measure's singleton mass at the recorded value is nonzero and finite, then the one-node observational step density obsStepCondDensity equals the conditional kernel's singleton mass at the recorded value divided by the reference measure's singleton mass there.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
rnDeriv_mul_measure_singletontheorem — On a measurable singleton, the RN derivative multiplied by the base mass recovers the numerator singleton mass.hypothesesα :hμν :μ ≪ νx :αProof (Lean source)
theorem rnDeriv_mul_measure_singleton {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ ν : Measure α) [SFinite ν] [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) (x : α) : ν ({x} : Set α) * μ.rnDeriv ν x = μ ({x} : Set α) := by have h1 : μ ({x} : Set α) = ∫⁻ y in ({x} : Set α), μ.rnDeriv ν y ∂ν := (Measure.setLIntegral_rnDeriv hμν ({x} : Set α)).symm have h2 : (∫⁻ y in ({x} : Set α), μ.rnDeriv ν y ∂ν) = μ.rnDeriv ν x * ν ({x} : Set α) := by rw [lintegral_singleton] rw [h1, h2, mul_comm] -
rnDeriv_singleton_eq_divtheorem — On a positive finite singleton of the reference measure, the RN derivative is the ratio of numerator mass to reference mass.Proof (Lean source)
theorem rnDeriv_singleton_eq_div {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ ν : Measure α) [SFinite ν] [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) (x : α) (hν0 : ν ({x} : Set α) ≠ 0) (hνtop : ν ({x} : Set α) ≠ ∞) : μ.rnDeriv ν x = μ ({x} : Set α) / ν ({x} : Set α) := by rw [ENNReal.eq_div_iff hν0 hνtop] exact rnDeriv_mul_measure_singleton μ ν hμν x -
jointRef_singleton_eq_prodtheorem — The singleton mass of a finite product reference is the product of the coordinate singleton masses.hypothesesProof (Lean source)
-
obsKernel_marginal_singleton_eq_latentProduct_agreetheorem — Mapping an observational kernel to a subcollection of observed coordinates turns a singleton mass into the latent-product mass of the corresponding agreement event.hypothesesconclusion= M.latentProduct {ℓ | ∀ v : {v // v ∈ P}, M.evalMap s ℓ ⟨v.val, mem_union_left M.unobserved (hP v.property)⟩ = x ⟨v.val, hP v.property⟩}Proof (Lean source)
theorem obsKernel_marginal_singleton_eq_latentProduct_agree (M : SCM N Ω) (s : M.FixedValues) {P : Finset (SWIGNode N)} (hP : P ⊆ M.observed) [MeasurableSingletonClass (ValuesOn P (swigΩ Ω))] (x : M.ObservedValues) : ((M.obsKernel s).map (valuesProjection hP)) ({valuesProjection hP x} : Set (ValuesOn P (swigΩ Ω))) = M.latentProduct {ℓ | ∀ v : {v // v ∈ P}, M.evalMap s ℓ ⟨v.val, mem_union_left M.unobserved (hP v.property)⟩ = x ⟨v.val, hP v.property⟩} := by classical have hproj : Measurable (valuesProjection (Ω := swigΩ Ω) hP) := measurable_valuesProjection hP have hcomp : Measurable ((valuesProjection (Ω := swigΩ Ω) hP) ∘ M.randomToObserved) := hproj.comp M.measurable_randomToObserved have heval : Measurable (fun ℓ : M.LatentValues => M.evalMap s ℓ) := M.evalMap_measurable.comp (prodMk measurable_const measurable_id) rw [SCM.obsKernel, Kernel.map_apply _ M.measurable_randomToObserved, Measure.map_map hproj M.measurable_randomToObserved] rw [M.jointKernel_apply_eq s, Measure.map_map hcomp heval] rw [Measure.map_apply] · congr 1 ext ℓ constructor · intro h v have hv := congrFun h v simpa [Function.comp_def, valuesProjection, SCM.randomToObserved] using hv · intro h ext v exact h v · exact hcomp.comp heval · exact MeasurableSet.singleton _ -
compProd_singleton_masstheorem — The singleton mass of a measure-kernel composition product factors as the conditioning singleton mass times the fibre singleton mass.hypothesesProof (Lean source)
theorem compProd_singleton_mass {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsSFiniteKernel κ] (b : α) (y : β) : (μ ⊗ₘ κ) ({(b, y)} : Set (α × β)) = μ ({b} : Set α) * κ b ({y} : Set β) := by have hset : ({b} : Set α) ×ˢ ({y} : Set β) = ({(b, y)} : Set (α × β)) := by ext p rcases p with ⟨b', y'⟩ simp calc (μ ⊗ₘ κ) ({(b, y)} : Set (α × β)) = (μ ⊗ₘ κ) (({b} : Set α) ×ˢ ({y} : Set β)) := by rw [hset] _ = ∫⁻ a in ({b} : Set α), κ a ({y} : Set β) ∂μ := by rw [Measure.compProd_apply_prod (MeasurableSet.singleton b) (MeasurableSet.singleton y)] _ = κ b ({y} : Set β) * μ ({b} : Set α) := by rw [lintegral_singleton] _ = μ ({b} : Set α) * κ b ({y} : Set β) := by rw [mul_comm] -
condKernel_singleton_mass_of_ne_zerotheorem — A disintegration conditional kernel at a positive conditioning atom is the joint singleton mass divided by the conditioning singleton mass.Proof (Lean source)
theorem condKernel_singleton_mass_of_ne_zero {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace β] [Nonempty β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (ρ : Measure (α × β)) [IsFiniteMeasure ρ] (b : α) (y : β) (hb : ρ.fst ({b} : Set α) ≠ 0) : ρ.condKernel b ({y} : Set β) = ρ ({(b, y)} : Set (α × β)) / ρ.fst ({b} : Set α) := by have hset : ({b} : Set α) ×ˢ ({y} : Set β) = ({(b, y)} : Set (α × β)) := by ext p rcases p with ⟨b', y'⟩ simp rw [Measure.condKernel_apply_of_ne_zero (ρ := ρ) hb ({y} : Set β)] rw [hset, ENNReal.div_eq_inv_mul] -
condDistrib_singleton_mass_of_ne_zerotheorem — Mathlib's measure-level conditional distribution has singleton mass equal to the corresponding joint singleton mass divided by the conditioning mass.hypothesesconclusion(condDistrib Y Z μ z) ({y} : Set γ)Proof (Lean source)
theorem condDistrib_singleton_mass_of_ne_zero {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [StandardBorelSpace γ] [Nonempty γ] [MeasurableSingletonClass β] [MeasurableSingletonClass γ] {μ : Measure α} [IsFiniteMeasure μ] {Y : α → γ} {Z : α → β} (hY : Measurable Y) (z : β) (y : γ) (hz : (μ.map Z) ({z} : Set β) ≠ 0) : (condDistrib Y Z μ z) ({y} : Set γ) = (μ.map (fun ω => (Z ω, Y ω))) ({(z, y)} : Set (β × γ)) / (μ.map Z) ({z} : Set β) := by have hset : ({z} : Set β) ×ˢ ({y} : Set γ) = ({(z, y)} : Set (β × γ)) := by ext p rcases p with ⟨z', y'⟩ simp rw [condDistrib_apply_of_ne_zero hY z hz ({y} : Set γ)] rw [hset, ENNReal.div_eq_inv_mul]
QFactor 8 core · 14 supporting This file provides the density-level Tian district objects used by the ID do-law assembly: the topological prefix helpers on a SWIG node set (nodesAt, nodeIndex, prefixIn), tianPrefixStepDensity, tianDistrictDensity (the ★ tianDistrictDensity_eq_mechCFactor_doModel★ tianDistrictDensity_eq_qLocalMass_div_jointRef_district★ tian_full_cComponent_density_recovery_core_direct
Tian district densities and the c-component recovery core
This file provides the density-level Tian district objects used by the ID
do-law assembly: the topological prefix helpers on a SWIG node set
(nodesAt, nodeIndex, prefixIn), tianPrefixStepDensity,
tianDistrictDensity (the S-district prefix-conditional product of a measure
on D), and tianDensityProduct, around Tian and Pearl (2002) Eqs. 37 and
70-72.
The keystone is tian_full_cComponent_density_recovery_core_direct: for a
district S of the post-intervention ancestral graph that is also a full
c-component of M, the S-district factor of the do-law ancestral marginal
equals a.e. the full observational c-component factor Q_M[S]. The proof
chains the do-model district-density identity, do(X)-invariance of mechanism
c-factors, and the observational c-component/mechanism equivalence.
This predicate says that two coordinate blocks are conditionally independent given a third block under a finite-coordinate measure.
Definition (Lean source)
This predicate says that every graphical separation in a graph gives the corresponding coordinate conditional independence under a finite-coordinate measure.
Definition (Lean source)
This density is Tian's one-node conditional factor along the topological prefix of a finite node set.
Definition (Lean source)
Tian's district density multiplies the prefix conditional factors whose nodes lie in one district.
Definition (Lean source)
Tian's full prefix-chain density multiplies all one-node prefix conditional factors for a finite node set.
Definition (Lean source)
(B) Tian Lemma 1 for the do-model ancestral marginal. Consider a structural causal model M with an intervention set X whose random copies are observed and whose fixed copies are not already frozen, an outcome set Y disjoint from the random copies of X, under a faithful reference-measure family, a positive observational kernel at every fixed-value assignment, and the standing assumption that M is a standard model. For a set S that is simultaneously a district of the post-intervention ancestral graph and a full c-component of M, and an extension map that inverts the projection onto the ancestral observed coordinates, the Tian district density read off the do(X)-law ancestral marginal at S agrees with the mechanism c-factor of the post-intervention model at the extended point.
Formal statement
Proof (Lean source)
Consider an intervention set X whose random copies are observed and whose fixed copies are not already frozen together with an outcome set Y disjoint from the random copies of X, under a faithful reference-measure family and a positive observational kernel at every fixed-value assignment. For any district S of the post-intervention ancestral graph and an extension map inverting the projection onto the ancestral observed coordinates, the Tian district density read off the do(X)-law ancestral marginal at S equals the do-model local q-mass on S divided by the reference atom mass of S.
Formal statement
Proof (Lean source)
District recovery (Tian Lemma 4 projection consistency). Consider a standard structural causal model M with an intervention set X whose random copies are observed and whose fixed copies are not already frozen, under a faithful reference-measure family and a positive observational kernel at every fixed-value assignment, for an outcome set Y disjoint from the random copies of X. For a set S that is simultaneously a district of the post-intervention ancestral graph and a full c-component of M, and an extension map that inverts the projection onto the ancestral observed coordinates and reproduces the intervention values sDo on the intervened coordinates, the Tian district density read off the do(X)-law ancestral marginal at S agrees, almost everywhere with respect to the product reference measure on the ancestral observed coordinates, with the observational c-component density factor at S pulled back through the extension.
Formal statement
Proof (Lean source)
14 supporting declarations (lemmas, instances)
-
prefixIn_obsParentClosedlemma — Topological prefixes of an observed-parent-closed set remain observed-parent-closed.hypothesesM :SCM N ΩX :Finset NhObs :∀ D ∈ X, SWIGNode.random D ∈ M.observedhFix :∀ D ∈ X, SWIGNode.fixed D ∉ M.fixedk :ℕconclusion(M.fixSet X hObs hFix).ObsParentClosed (((M.fixSet X hObs hFix).toSWIGGraph.induce (SCM.ID.fixAncestralSet M X hObs hFix Y)).prefixIn (SCM.ID.fixObservedAncestralSet M X hObs hFix Y) k)Proof (Lean source)
lemma prefixIn_obsParentClosed (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)) (k : ℕ) : (M.fixSet X hObs hFix).ObsParentClosed (((M.fixSet X hObs hFix).toSWIGGraph.induce (SCM.ID.fixAncestralSet M X hObs hFix Y)).prefixIn (SCM.ID.fixObservedAncestralSet M X hObs hFix Y) k) := by classical let M' := M.fixSet X hObs hFix let A := SCM.ID.fixAncestralSet M X hObs hFix Y let D := SCM.ID.fixObservedAncestralSet M X hObs hFix Y let H := M'.toSWIGGraph.induce A have hDclosed : M'.ObsParentClosed D := by simpa [M', D] using (SCM.ID.fixObservedAncestralSet_obsParent_closed M X hObs hFix Y) refine ⟨?_, ?_⟩ · intro v hv exact hDclosed.1 (H.prefixIn_subset D k hv) · intro v hv w hwObs hEdge have hvD : v ∈ D := H.prefixIn_subset D k hv have hwD : w ∈ D := hDclosed.2 v hvD w hwObs hEdge rcases Finset.mem_filter.mp hv with ⟨hvD₀, hvIdxLt₀⟩ have hvIdxLt : (H.nodeIndex D ⟨v, hvD⟩).val < k := by have hsub : (⟨v, hvD⟩ : {v // v ∈ D}) = ⟨v, hvD₀⟩ := Subtype.ext rfl simpa [SWIGGraph.prefixIn, hsub, hvD₀] using hvIdxLt₀ have hEdgeH : H.dag.edge w v := by have hwA : w ∈ A := (Finset.mem_inter.mp hwD).1 have hvA : v ∈ A := (Finset.mem_inter.mp hvD).1 have hvObs : v ∈ M'.observed := hDclosed.1 hvD dsimp [H, M', A, SWIGGraph.induce, SWIGGraph.inducedDag, SWIGGraph.inducedEdge] refine ⟨hEdge, ?_, ?_⟩ · exact mem_union_left _ (mem_union_right _ (Finset.mem_inter.mpr ⟨hwA, hwObs⟩)) · exact mem_union_left _ (mem_union_right _ (Finset.mem_inter.mpr ⟨hvA, hvObs⟩)) have hTopo : H.dag.topoOrder w < H.dag.topoOrder v := H.dag.topoOrder_lt w v hEdgeH letI := H.topoLinearOrder have hSubtypeLt : (⟨w, hwD⟩ : {v // v ∈ D}) < ⟨v, hvD⟩ := by change H.dag.topoOrder w < H.dag.topoOrder v exact hTopo have hIndexLt : (H.nodeIndex D ⟨w, hwD⟩).val < (H.nodeIndex D ⟨v, hvD⟩).val := by have hIndexLtFin : H.nodeIndex D ⟨w, hwD⟩ < H.nodeIndex D ⟨v, hvD⟩ := by simpa [SWIGGraph.nodeIndex] using ((D.orderIsoOfFin rfl).symm.strictMono hSubtypeLt) simpa [SWIGGraph.nodeIndex] using hIndexLtFin change w ∈ D.filter (fun v => if h : v ∈ D then (H.nodeIndex D ⟨v, h⟩).val < k else False) exact Finset.mem_filter.mpr ⟨hwD, by simpa [hwD] using lt_trans hIndexLt hvIdxLt⟩ -
mem_cComponent_iff_cComponentOf_eqlemma — For an observed node and a c-component listed in cComponentSet, membership in that component is the same as saying that the node's computed c-component is that listed component. This converts Tian's district factor, which filters by membership in a district, into the fiber form needed for finite-product regrouping.hypothesesconclusionv ∈ S ↔ G.cComponentOf v = SProof (Lean source)
lemma mem_cComponent_iff_cComponentOf_eq (G : SWIGGraph N) {v : SWIGNode N} {S : Finset (SWIGNode N)} (hv : v ∈ G.observed) (hS : S ∈ G.cComponentSet) : v ∈ S ↔ G.cComponentOf v = S := by constructor · intro hvS rw [SWIGGraph.cComponentSet, mem_image] at hS obtain ⟨w, hw, rfl⟩ := hS have hwv : G.bidirectedReachable w v := (G.mem_cComponentOf_iff_reachable hw).mp hvS exact (G.cComponentOf_eq_of_reachable hwv).symm · intro hcomp exact hcomp ▸ G.mem_cComponentOf_self hv -
prod_tianDistrictDensity_eq_tianDensityProducttheorem — Tian's full prefix-chain density regroups exactly as the product of the Tian district factors over the graph c-components. This is pure finite-product algebra: each prefix index maps to the c-component of its node, and the district factor is precisely the product over the corresponding fiber.hypothesesH :hD :H.observed = Dref :∀ (k : ℕ) (hk : k < D.card),conclusion(fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D μ ref S x)= fun x => tianDensityProduct H D μ ref xProof (Lean source)
theorem prod_tianDistrictDensity_eq_tianDensityProduct (H : SWIGGraph N) (D : Finset (SWIGNode N)) (hD : H.observed = D) (μ : 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Ω Ω))] : (fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D μ ref S x) = fun x => tianDensityProduct H D μ ref x := by classical funext x have hmaps : ∀ i ∈ (Finset.univ : Finset (Fin D.card)), H.cComponentOf (H.nodesAt D i).val ∈ H.cComponentSet := by intro i _ exact Finset.mem_image.mpr ⟨(H.nodesAt D i).val, hD.symm ▸ (H.nodesAt D i).property, rfl⟩ unfold tianDensityProduct tianDistrictDensity rw [← Finset.prod_fiberwise_of_maps_to hmaps (fun i => tianPrefixStepDensity H D μ ref i x)] refine Finset.prod_congr rfl ?_ intro S hS refine Finset.prod_congr ?_ (fun i _ => rfl) ext i simp only [mem_filter, Finset.mem_univ, true_and] exact mem_cComponent_iff_cComponentOf_eq H (hD.symm ▸ (H.nodesAt D i).property) hS -
prefixIn_parent_closed_induce_observedlemma — In an induced set of observed variables, every topological prefix contains all parents within that set of each variable it contains.hypothesesProof (Lean source)
lemma prefixIn_parent_closed_induce_observed (M : SCM N Ω) (A : Finset (SWIGNode N)) (hA : A ⊆ M.observed) (k : ℕ) : ∀ v ∈ A, ∀ w ∈ (M.toSWIGGraph.induce A).prefixIn A k, M.dag.edge v w → v ∈ (M.toSWIGGraph.induce A).prefixIn A k := by classical intro v hvA w hwPre hEdge let H := M.toSWIGGraph.induce A have hwA : w ∈ A := H.prefixIn_subset A k hwPre have hEdgeH : H.dag.edge v w := by dsimp [H, SWIGGraph.induce] rw [SWIGGraph.inducedDag_edge_iff] refine ⟨hEdge, ?_, ?_⟩ · simp [hvA, hA hvA] · simp [hwA, hA hwA] have hTopo : H.dag.topoOrder v < H.dag.topoOrder w := H.dag.topoOrder_lt v w hEdgeH rcases (mem_prefixIn_iff_qfactor H A k w).mp hwPre with ⟨hwA', hwIdxLt⟩ letI := H.topoLinearOrder have hSubtypeLt : (⟨v, hvA⟩ : {v // v ∈ A}) < ⟨w, hwA'⟩ := by change H.dag.topoOrder v < H.dag.topoOrder w exact hTopo have hIndexLt : (H.nodeIndex A ⟨v, hvA⟩).val < (H.nodeIndex A ⟨w, hwA'⟩).val := by have hIndexLtFin : H.nodeIndex A ⟨v, hvA⟩ < H.nodeIndex A ⟨w, hwA'⟩ := by simpa [SWIGGraph.nodeIndex] using ((A.orderIsoOfFin rfl).symm.strictMono hSubtypeLt) simpa [SWIGGraph.nodeIndex] using hIndexLtFin exact (mem_prefixIn_iff_qfactor H A k v).mpr ⟨hvA, lt_trans hIndexLt hwIdxLt⟩ -
prefixIn_qProduct_ratio_eq_component_ratio_of_familylemma — In a product over an abstract pairwise-disjoint family, the prefix-ratio step at a node of S cancels every factor except the S factor.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N ΩH :s :M.FixedValueshS𝒞 :S ∈ 𝒞hdisj :∀ C ∈ 𝒞ifC ≠ SthenDisjoint C Si :Fin D.cardhDobs :D ⊆ M.observedhiS :(H.nodesAt D i).val ∈ Shpos :DiscreteID.PositiveMass (M.obsKernel s)conclusion(∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)= M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) xProof (Lean source)
lemma prefixIn_qProduct_ratio_eq_component_ratio_of_family [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (H : SWIGGraph N) (D : Finset (SWIGNode N)) (s : M.FixedValues) (𝒞 : Finset (Finset (SWIGNode N))) (S : Finset (SWIGNode N)) (hS𝒞 : S ∈ 𝒞) (hdisj : ∀ C ∈ 𝒞, C ≠ S → Disjoint C S) (i : Fin D.card) (hDobs : D ⊆ M.observed) (hiS : (H.nodesAt D i).val ∈ S) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) (x : ValuesOn M.observed (swigΩ Ω)) : (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) = M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x := by classical let f₁ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x let f₀ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x have hrest : ∏ C ∈ 𝒞 \ {S}, f₁ C = ∏ C ∈ 𝒞 \ {S}, f₀ C := by refine Finset.prod_congr rfl ?_ intro C hC have hC𝒞 : C ∈ 𝒞 := (Finset.mem_sdiff.mp hC).1 have hCne : C ≠ S := by intro h exact (Finset.mem_sdiff.mp hC).2 (by simp [h]) simp [f₁, f₀, family_inter_prefixIn_succ_eq_of_ne H D hiS (hdisj C hC𝒞 hCne)] have hsplit₁ : (∏ C ∈ 𝒞, f₁ C) = f₁ S * ∏ C ∈ 𝒞 \ {S}, f₁ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₁ (by intro h; exact elim (h hS𝒞)) have hsplit₀ : (∏ C ∈ 𝒞, f₀ C) = f₀ S * ∏ C ∈ 𝒞 \ {S}, f₀ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₀ (by intro h; exact elim (h hS𝒞)) have hr0 : (∏ C ∈ 𝒞 \ {S}, f₀ C) ≠ 0 := by exact Finset.prod_ne_zero_iff.mpr (by intro C _hC exact M.qLocalMass_pos_of_positiveObs s hpos (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) have hrtop : (∏ C ∈ 𝒞 \ {S}, f₀ C) ≠ ∞ := by exact Finset.prod_ne_top_of_ne_top _ f₀ (by intro C _hC exact qLocalMass_ne_top M s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) change (∏ C ∈ 𝒞, f₁ C) / (∏ C ∈ 𝒞, f₀ C) = f₁ S / f₀ S rw [hsplit₁, hsplit₀, hrest] exact ENNReal.div_mul_common hr0 hrtop -
prefixIn_qProduct_ratio_eq_component_ratio_of_family_of_ne_zerolemma — Nonzero-denominator variant of prefixIn_qProduct_ratio_eq_component_ratio_of_family.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N ΩH :s :M.FixedValueshS𝒞 :S ∈ 𝒞hdisj :∀ C ∈ 𝒞ifC ≠ SthenDisjoint C Si :Fin D.cardhDobs :D ⊆ M.observedhiS :(H.nodesAt D i).val ∈ Shrest0 :(∏ C ∈ 𝒞 \ {S}, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)≠ 0conclusion(∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)= M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) xProof (Lean source)
lemma prefixIn_qProduct_ratio_eq_component_ratio_of_family_of_ne_zero [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (H : SWIGGraph N) (D : Finset (SWIGNode N)) (s : M.FixedValues) (𝒞 : Finset (Finset (SWIGNode N))) (S : Finset (SWIGNode N)) (hS𝒞 : S ∈ 𝒞) (hdisj : ∀ C ∈ 𝒞, C ≠ S → Disjoint C S) (i : Fin D.card) (hDobs : D ⊆ M.observed) (hiS : (H.nodesAt D i).val ∈ S) (x : ValuesOn M.observed (swigΩ Ω)) (hrest0 : (∏ C ∈ 𝒞 \ {S}, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) ≠ 0) : (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) = M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x := by classical let f₁ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x let f₀ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x have hrest : ∏ C ∈ 𝒞 \ {S}, f₁ C = ∏ C ∈ 𝒞 \ {S}, f₀ C := by refine Finset.prod_congr rfl ?_ intro C hC have hC𝒞 : C ∈ 𝒞 := (Finset.mem_sdiff.mp hC).1 have hCne : C ≠ S := by intro h exact (Finset.mem_sdiff.mp hC).2 (by simp [h]) simp [f₁, f₀, family_inter_prefixIn_succ_eq_of_ne H D hiS (hdisj C hC𝒞 hCne)] have hsplit₁ : (∏ C ∈ 𝒞, f₁ C) = f₁ S * ∏ C ∈ 𝒞 \ {S}, f₁ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₁ (by intro h; exact elim (h hS𝒞)) have hsplit₀ : (∏ C ∈ 𝒞, f₀ C) = f₀ S * ∏ C ∈ 𝒞 \ {S}, f₀ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₀ (by intro h; exact elim (h hS𝒞)) have hrtop : (∏ C ∈ 𝒞 \ {S}, f₀ C) ≠ ∞ := by exact Finset.prod_ne_top_of_ne_top _ f₀ (by intro C _hC exact qLocalMass_ne_top M s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) change (∏ C ∈ 𝒞, f₁ C) / (∏ C ∈ 𝒞, f₀ C) = f₁ S / f₀ S rw [hsplit₁, hsplit₀, hrest] exact ENNReal.div_mul_common hrest0 hrtop -
extractDistrict_qLocalMasslemma — Extracting an induced district from the local mass on an ancestral set recovers that district's local q-mass.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N Ωs :M.FixedValueshA :A ⊆ M.observedhC' :C' ∈ (M.toSWIGGraph.induce A).cComponentSethpos :DiscreteID.PositiveMass (M.obsKernel s)conclusionextractDistrict M.observed (M.toSWIGGraph.induce A) A C' hA (M.qLocalMass s A hA) x= M.qLocalMass s C' (fun _ hv => hA (by have hHobs : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C' hC' hv)) xProof (Lean source)
lemma extractDistrict_qLocalMass [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (A C' : Finset (SWIGNode N)) (hA : A ⊆ M.observed) (hC' : C' ∈ (M.toSWIGGraph.induce A).cComponentSet) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) (x : ValuesOn M.observed (swigΩ Ω)) : extractDistrict M.observed (M.toSWIGGraph.induce A) A C' hA (M.qLocalMass s A hA) x = M.qLocalMass s C' (fun _ hv => hA (by have hHobs : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C' hC' hv)) x := by classical let H := M.toSWIGGraph.induce A have hHobs : H.observed = A := by simp [H, SWIGGraph.induce, Finset.inter_eq_left.mpr hA] have hCobs : C' ⊆ M.observed := by intro v hv exact hA (hHobs ▸ H.cComponentSet_subset_observed C' hC' hv) have hCA : C' ⊆ A := by intro v hv exact hHobs ▸ H.cComponentSet_subset_observed C' hC' hv have hdisj : (↑H.cComponentSet : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint U U') := by intro U hU V hV hne exact H.cComponentSet_pairwise_disjoint hU hV hne have hmarg : ∀ k, marginalizeOn M.observed (A \ H.prefixIn A k) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s A hA) x = M.qLocalMass s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) x := by intro k simpa [H] using M.qLocalMass_marginalize_ancestralClosed s A (H.prefixIn A k) hA (H.prefixIn_subset A k) (prefixIn_parent_closed_induce_observed M A hA k) x have hprod : ∀ k, M.qLocalMass s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) x = ∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k (mem_of_mem_inter_right hv))) x := by intro k simpa [H] using qLocalMass_prefixIn_eq_prod_induce_components M s A hA k x unfold SCM.extractDistrict calc (∏ i ∈ Finset.univ.filter (fun i : Fin A.card => (H.nodesAt A i).val ∈ C'), marginalizeOn M.observed (A \ H.prefixIn A (i.val + 1)) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s A hA) x / marginalizeOn M.observed (A \ H.prefixIn A i.val) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s A hA) x) = ∏ i ∈ Finset.univ.filter (fun i : Fin A.card => (H.nodesAt A i).val ∈ C'), (∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A (i.val + 1)) (fun _ hv => hA (H.prefixIn_subset A (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A i.val) (fun _ hv => hA (H.prefixIn_subset A i.val (mem_of_mem_inter_right hv))) x) := by refine Finset.prod_congr rfl ?_ intro i _hi rw [hmarg (i.val + 1), hmarg i.val, hprod (i.val + 1), hprod i.val] _ = ∏ i ∈ Finset.univ.filter (fun i : Fin A.card => (H.nodesAt A i).val ∈ C'), M.qLocalMass s (C' ∩ H.prefixIn A (i.val + 1)) (fun _ hv => hA (H.prefixIn_subset A (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (C' ∩ H.prefixIn A i.val) (fun _ hv => hA (H.prefixIn_subset A i.val (mem_of_mem_inter_right hv))) x := by refine Finset.prod_congr rfl ?_ intro i hi have hiC : (H.nodesAt A i).val ∈ C' := (Finset.mem_filter.mp hi).2 exact prefixIn_qProduct_ratio_eq_component_ratio_of_family M H A s H.cComponentSet C' hC' (fun C hC hne => hdisj hC hC' hne) i hA hiC hpos x _ = M.qLocalMass s C' hCobs x := by simpa using component_qLocalMass_ratio_product_prefixIn M H A s C' hCobs hCA hpos x _ = M.qLocalMass s C' (fun _ hv => hA (by have hHobs' : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs' ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C' hC' hv)) x := by rfl -
target_subsettheorem — The target set of a recursive c-factor reachability certificate is contained in the source set.Proof (Lean source)
theorem CFactorReachableRec.target_subset {G : SWIGGraph N} {T C : Finset (SWIGNode N)} (h : CFactorReachableRec G T C) : C ⊆ T := by cases h with | base _ hCT _ => exact hCT | step _ hCT _ _ _ => exact hCT -
qLocalMass_obsProof_irrellemma — The local q-mass of an observed variable set does not depend on which proof establishes that the set is observed.hypothesesconclusionM.qLocalMass s T hT x = M.qLocalMass s T hT' x -
identifyMassRec_qLocalMasstheorem — The obs-side IDENTIFY recursion recovers the local q-mass of the target district from the local q-mass of any recursively reachable source district.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)M :SCM N Ωs :M.FixedValueshpos :DiscreteID.PositiveMass (M.obsKernel s)hT :T ⊆ M.observedhReach :CFactorReachableRec M.toSWIGGraph T CconclusionidentifyMassRec M.observed M.toSWIGGraph T C hT (M.qLocalMass s T hT) x= M.qLocalMass s C (fun _ hv => hT (hReach.target_subset hv)) xProof (Lean source)
theorem identifyMassRec_qLocalMass [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) (T C : Finset (SWIGNode N)) (hT : T ⊆ M.observed) (hReach : CFactorReachableRec M.toSWIGGraph T C) (x : ValuesOn M.observed (swigΩ Ω)) : identifyMassRec M.observed M.toSWIGGraph T C hT (M.qLocalMass s T hT) x = M.qLocalMass s C (fun _ hv => hT (hReach.target_subset hv)) x := by classical induction hReach generalizing x with | base hne hCT hproject => rename_i T₀ C₀ rw [SCM.identifyMassRec_base M M.toSWIGGraph T₀ C₀ hT (M.qLocalMass s T₀ hT) hproject] have hclosed : ∀ v ∈ T₀, ∀ w ∈ C₀, M.dag.edge v w → v ∈ C₀ := by have hclosedA := inducedAncestral_parent_closed M.toSWIGGraph (T := T₀) (C := C₀) (by simpa using hT) intro v hvT w hwC hEdge have hwA : w ∈ inducedAncestral M.toSWIGGraph T₀ C₀ := by simpa [hproject] using hwC have hvA := hclosedA v hvT w hwA hEdge simpa [hproject] using hvA exact M.qLocalMass_marginalize_ancestralClosed s T₀ C₀ hT hCT hclosed x | step hne hCT hnotC hnotT hrec ih => rename_i T₀ C₀ let A := inducedAncestral M.toSWIGGraph T₀ C₀ let C₁ := containingCComponent (M.toSWIGGraph.induce A) C₀ let hA : A ⊆ M.observed := fun _ hv => hT (inducedAncestral_subset_left M.toSWIGGraph T₀ C₀ hv) let hC₁obs : C₁ ⊆ M.observed := fun _ hv => hT (inducedAncestral_subset_left M.toSWIGGraph T₀ C₀ (containingCComponent_induce_subset M.toSWIGGraph A C₀ hv)) have hCobs : C₀ ⊆ M.toSWIGGraph.observed := by intro v hv simpa using hT (hCT hv) have hCA : C₀ ⊆ A := subset_inducedAncestral M.toSWIGGraph hCT hCobs have hC₁mem : C₁ ∈ (M.toSWIGGraph.induce A).cComponentSet := by simp only [C₁, containingCComponent, dif_pos hne, SWIGGraph.cComponentSet] have hchooseA : hne.choose ∈ A := hCA hne.choose_spec have hchooseObs : hne.choose ∈ M.toSWIGGraph.observed := hCobs hne.choose_spec have hchooseInd : hne.choose ∈ (M.toSWIGGraph.induce A).observed := by simp [SWIGGraph.induce, hchooseA, hchooseObs] exact Finset.mem_image.mpr ⟨hne.choose, hchooseInd, rfl⟩ have hmarg : marginalizeOn M.observed (T₀ \ A) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T₀ hT) = M.qLocalMass s A hA := by funext y have hclosedA : ∀ v ∈ T₀, ∀ w ∈ A, M.dag.edge v w → v ∈ A := by simpa [A] using inducedAncestral_parent_closed M.toSWIGGraph (T := T₀) (C := C₀) (by simpa using hT) exact M.qLocalMass_marginalize_ancestralClosed s T₀ A hT (inducedAncestral_subset_left M.toSWIGGraph T₀ C₀) hclosedA y have hextract : extractDistrict M.observed (M.toSWIGGraph.induce A) A C₁ hA (M.qLocalMass s A hA) = M.qLocalMass s C₁ hC₁obs := by funext y calc extractDistrict M.observed (M.toSWIGGraph.induce A) A C₁ hA (M.qLocalMass s A hA) y = M.qLocalMass s C₁ (fun _ hv => hA (by have hHobs : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C₁ hC₁mem hv)) y := by exact extractDistrict_qLocalMass M s A C₁ hA hC₁mem hpos y _ = M.qLocalMass s C₁ hC₁obs y := by exact qLocalMass_obsProof_irrel M s C₁ _ _ y rw [SCM.identifyMassRec_step M M.toSWIGGraph T₀ C₀ hT (M.qLocalMass s T₀ hT) hnotC hnotT] change identifyMassRec M.observed M.toSWIGGraph C₁ C₀ hC₁obs (extractDistrict M.observed (M.toSWIGGraph.induce A) A C₁ hA (marginalizeOn M.observed (T₀ \ A) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T₀ hT))) x = _ rw [hmarg, hextract] calc identifyMassRec M.observed M.toSWIGGraph C₁ C₀ hC₁obs (M.qLocalMass s C₁ hC₁obs) x = M.qLocalMass s C₀ (fun _ hv => hC₁obs (hrec.target_subset hv)) x := by exact ih hC₁obs x _ = M.qLocalMass s C₀ (fun _ hv => hT ((CFactorReachableRec.step hne hCT hnotC hnotT hrec).target_subset hv)) x := by exact qLocalMass_obsProof_irrel M s C₀ _ _ x -
component_ref_atom_product_eq_jointRef_prefixInlemma — For a subset of an ordered finite graph set, the product of coordinate reference-measure masses at selected values equals the reference measure's mass at their joint singleton outcome.hypothesesProof (Lean source)
lemma component_ref_atom_product_eq_jointRef_prefixIn [∀ n, MeasurableSingletonClass (Ω n)] (H : SWIGGraph N) (D : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (S : Finset (SWIGNode N)) (hSD : S ⊆ D) (xD : ValuesOn D (swigΩ Ω)) : (∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), ref.μ (H.nodesAt D i).val ({xD (H.nodesAt D i)} : Set (swigΩ Ω (H.nodesAt D i).val))) = jointRef ref S ({valuesProjection hSD xD} : Set (ValuesOn S (swigΩ Ω))) := by classical have hprod : (∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), ref.μ (H.nodesAt D i).val ({xD (H.nodesAt D i)} : Set (swigΩ Ω (H.nodesAt D i).val))) = ∏ v : {v // v ∈ S}, ref.μ v.val ({(valuesProjection hSD xD) v} : Set (swigΩ Ω v.val)) := by refine Finset.prod_bij (fun i hi => ⟨(H.nodesAt D i).val, (Finset.mem_filter.mp hi).2⟩) ?_ ?_ ?_ ?_ · intro i hi exact Finset.mem_univ _ · intro i _hi j _hj hij have hval : (H.nodesAt D i).val = (H.nodesAt D j).val := congrArg (fun v : {v // v ∈ S} => v.val) hij have hsub : H.nodesAt D i = H.nodesAt D j := Subtype.ext hval calc i = H.nodeIndex D (H.nodesAt D i) := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] _ = H.nodeIndex D (H.nodesAt D j) := by rw [hsub] _ = j := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] · intro v _hv let i : Fin D.card := H.nodeIndex D ⟨v.val, hSD v.property⟩ have hnode : (H.nodesAt D i).val = v.val := by have hround : H.nodesAt D (H.nodeIndex D ⟨v.val, hSD v.property⟩) = ⟨v.val, hSD v.property⟩ := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] exact congrArg val hround refine ⟨i, ?_, ?_⟩ · rw [mem_filter] exact ⟨Finset.mem_univ _, by simp [hnode, v.property]⟩ · exact Subtype.ext hnode · intro i hi simp [valuesProjection] rw [jointRef_singleton_eq_prod] exact hprod -
prefix_pair_singleton_mass_eq_succ_prefix_masslemma — The mass of a realized prefix together with its next coordinate equals the mass of the same realization of the successor prefix under any measure on the ordered graph values.hypothesesconclusion(μ.map (fun ω : ValuesOn D (swigΩ Ω) => (valuesProjection (H.prefixIn_subset D i.val) ω, 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 (H.prefixIn_subset D i.val) x, 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) x)} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω) × ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω)))= (μ.map (valuesProjection (H.prefixIn_subset D (i.val + 1)))) ({valuesProjection (H.prefixIn_subset D (i.val + 1)) x} : Set (ValuesOn (H.prefixIn D (i.val + 1)) (swigΩ Ω)))Proof (Lean source)
lemma prefix_pair_singleton_mass_eq_succ_prefix_mass [∀ n, MeasurableSingletonClass (Ω n)] (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (i : Fin D.card) (x : ValuesOn D (swigΩ Ω)) : (μ.map (fun ω : ValuesOn D (swigΩ Ω) => (valuesProjection (H.prefixIn_subset D i.val) ω, 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 (H.prefixIn_subset D i.val) x, 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) x)} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω) × ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) = (μ.map (valuesProjection (H.prefixIn_subset D (i.val + 1)))) ({valuesProjection (H.prefixIn_subset D (i.val + 1)) x} : Set (ValuesOn (H.prefixIn D (i.val + 1)) (swigΩ Ω))) := by classical let hNodeD : ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D := by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property let pairMap : ValuesOn D (swigΩ Ω) → ValuesOn (H.prefixIn D i.val) (swigΩ Ω) × ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω) := fun ω => (valuesProjection (H.prefixIn_subset D i.val) ω, valuesProjection hNodeD ω) let succMap : ValuesOn D (swigΩ Ω) → ValuesOn (H.prefixIn D (i.val + 1)) (swigΩ Ω) := valuesProjection (H.prefixIn_subset D (i.val + 1)) have hsets : pairMap ⁻¹' ({(valuesProjection (H.prefixIn_subset D i.val) x, valuesProjection hNodeD x)} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω) × ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) = succMap ⁻¹' ({valuesProjection (H.prefixIn_subset D (i.val + 1)) x} : Set (ValuesOn (H.prefixIn D (i.val + 1)) (swigΩ Ω))) := by ext ω constructor · intro hω have hpre : valuesProjection (H.prefixIn_subset D i.val) ω = valuesProjection (H.prefixIn_subset D i.val) x := congrArg Prod.fst hω have hnode : valuesProjection hNodeD ω = valuesProjection hNodeD x := congrArg Prod.snd hω ext v by_cases hvpre : v.val ∈ H.prefixIn D i.val · have h := congrFun hpre ⟨v.val, hvpre⟩ simpa [succMap, valuesProjection] using h · have hvnode : v.val = (H.nodesAt D i).val := by have hvsucc : v.val ∈ H.prefixIn D (i.val + 1) := v.property have hvsucc' : v.val ∈ H.prefixIn D i.val ∪ {(H.nodesAt D i).val} := by simpa [prefixIn_succ_qfactor H D i.isLt] using hvsucc rcases Finset.mem_union.mp hvsucc' with hvold | hvnew · exact elim (hvpre hvold) · simpa using hvnew have h := congrFun hnode ⟨v.val, by simpa [hvnode] using mem_singleton_self (H.nodesAt D i).val⟩ simpa [succMap, valuesProjection, hvnode] using h · intro hω have hsucc : valuesProjection (H.prefixIn_subset D (i.val + 1)) ω = valuesProjection (H.prefixIn_subset D (i.val + 1)) x := hω apply Prod.ext · ext v have hvsucc : v.val ∈ H.prefixIn D (i.val + 1) := prefixIn_mono_qfactor H D (Nat.le_succ i.val) v.property have h := congrFun hsucc ⟨v.val, hvsucc⟩ simpa [pairMap, valuesProjection] using h · ext v have hvnode : v.val = (H.nodesAt D i).val := by exact Finset.mem_singleton.mp v.property have hvsucc : v.val ∈ H.prefixIn D (i.val + 1) := by rw [hvnode, nodesAt_mem_prefixIn_iff_qfactor H D (i.val + 1) i] exact Nat.lt_succ_self i.val have h := congrFun hsucc ⟨v.val, hvsucc⟩ simpa [pairMap, valuesProjection] using h rw [MeasureTheory.Measure.map_apply ((measurable_valuesProjection (H.prefixIn_subset D i.val)).prod (measurable_valuesProjection hNodeD)) (MeasurableSet.singleton _), MeasureTheory.Measure.map_apply (measurable_valuesProjection (H.prefixIn_subset D (i.val + 1))) (MeasurableSet.singleton _), hsets] -
tianPrefixStepDensity_eq_prefix_mass_ratiolemma — When the preceding prefix has nonzero singleton mass, the one-step Tian density is the ratio of the successive prefix singleton masses, divided by the singleton reference mass of the added variable.hypotheses∀ n, Fintype (Ω n)∀ n, MeasurableSingletonClass (Ω n)H :ref :href :∀ (k : ℕ) (hk : k < D.card),i :Fin D.cardhprefix0 :(μ.map (valuesProjection (H.prefixIn_subset D i.val))) ({valuesProjection (H.prefixIn_subset D i.val) x} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω)))≠ 0conclusiontianPrefixStepDensity H D μ ref i x= ((μ.map (valuesProjection (H.prefixIn_subset D (i.val + 1)))) ({valuesProjection (H.prefixIn_subset D (i.val + 1)) x} : Set (ValuesOn (H.prefixIn D (i.val + 1)) (swigΩ Ω))) / (μ.map (valuesProjection (H.prefixIn_subset D i.val))) ({valuesProjection (H.prefixIn_subset D i.val) x} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω)))) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({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) x} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω)))Proof (Lean source)
lemma tianPrefixStepDensity_eq_prefix_mass_ratio [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (H : SWIGGraph N) (D : Finset (SWIGNode N)) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) [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Ω Ω))] (i : Fin D.card) (x : ValuesOn D (swigΩ Ω)) (hprefix0 : (μ.map (valuesProjection (H.prefixIn_subset D i.val))) ({valuesProjection (H.prefixIn_subset D i.val) x} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω))) ≠ 0) : tianPrefixStepDensity H D μ ref i x = ((μ.map (valuesProjection (H.prefixIn_subset D (i.val + 1)))) ({valuesProjection (H.prefixIn_subset D (i.val + 1)) x} : Set (ValuesOn (H.prefixIn D (i.val + 1)) (swigΩ Ω))) / (μ.map (valuesProjection (H.prefixIn_subset D i.val))) ({valuesProjection (H.prefixIn_subset D i.val) x} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω)))) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({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) x} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) := by classical let hNodeD : ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D := by intro v hv rw [mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property let nodeMap : ValuesOn D (swigΩ Ω) → ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω) := valuesProjection hNodeD let prefixMap : ValuesOn D (swigΩ Ω) → ValuesOn (H.prefixIn D i.val) (swigΩ Ω) := valuesProjection (H.prefixIn_subset D i.val) have hden0 : jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({nodeMap x} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) ≠ 0 := jointRef_singleton_ne_zero ref href _ (nodeMap x) have hdentop : jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({nodeMap x} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) ≠ ∞ := by exact ne_of_lt (MeasureTheory.measure_lt_top (jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N))) _) have hcond : (condDistrib nodeMap prefixMap μ (prefixMap x)) ({nodeMap x} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) = (μ.map (valuesProjection (H.prefixIn_subset D (i.val + 1)))) ({valuesProjection (H.prefixIn_subset D (i.val + 1)) x} : Set (ValuesOn (H.prefixIn D (i.val + 1)) (swigΩ Ω))) / (μ.map prefixMap) ({prefixMap x} : Set (ValuesOn (H.prefixIn D i.val) (swigΩ Ω))) := by rw [condDistrib_singleton_mass_of_ne_zero (μ := μ) (Y := nodeMap) (Z := prefixMap) (measurable_valuesProjection hNodeD) (prefixMap x) (nodeMap x) hprefix0] rw [prefix_pair_singleton_mass_eq_succ_prefix_mass H D μ i x] unfold tianPrefixStepDensity rw [rnDeriv_singleton_eq_div _ _ (absolutelyContinuous_jointRef_of_faithful ref href ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (condDistrib nodeMap prefixMap μ (prefixMap x))) (nodeMap x) hden0 hdentop] simpa [nodeMap, prefixMap, hNodeD] using congrArg (fun a => a / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({nodeMap x} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω)))) hcond -
valuesProjection_extend_eq_of_subsetlemma — If an extension preserves all values on a larger observed set, then restricting the extension to any subset gives the same values as restricting the original assignment directly.hypothesesM :SCM N ΩhDobs :D ⊆ M.observedhSD :S ⊆ DhSobs :S ⊆ M.observedhExtend :∀ xD, valuesProjection hDobs (extend xD) = xDconclusionvaluesProjection hSobs (extend xD) = valuesProjection hSD xDProof (Lean source)
lemma valuesProjection_extend_eq_of_subset (M : SCM N Ω) {D S : Finset (SWIGNode N)} (hDobs : D ⊆ M.observed) (hSD : S ⊆ D) (hSobs : S ⊆ M.observed) (extend : ValuesOn D (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection hDobs (extend xD) = xD) (xD : ValuesOn D (swigΩ Ω)) : valuesProjection hSobs (extend xD) = valuesProjection hSD xD := by ext v have h := congrFun (hExtend xD) ⟨v.val, hSD v.property⟩ simpa [valuesProjection] using h
TianMassBridge 1 core · 0 supporting This file connects the Tian prefix-density construction to finite point-mass ratios. ★ tianPrefixStepDensityInPrefix_eq_mass_ratio
Tian density point-mass bridges
This file connects the Tian prefix-density construction to finite point-mass
ratios. Its public bridge theorem
tianPrefixStepDensityInPrefix_eq_mass_ratio says that, on a measurable
singleton with nonzero finite reference mass, a Tian one-step Radon--Nikodym
density is exactly the conditional singleton mass divided by the corresponding
singleton mass of the product reference.
The result is used by the discrete ID soundness lane to translate the measure-theoretic density factorization into the point-mass formulas consumed by finite conditional-mass proofs.
Fix a step index i earlier than the prefix length k that also lies within the node domain D. Provided the conditional distribution of the i-th coordinate given the shorter prefix is absolutely continuous with respect to the reference measure on that coordinate, and the reference-measure mass of the singleton value at that coordinate is nonzero and finite, then the Tian prefix-step density at index i equals the prefix conditional singleton mass divided by the corresponding singleton mass of the product reference measure.