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★ 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)
For a node population with measurable value spaces, a reference-measure family, and a finite node set, the joint reference measure is the finite product of the reference measures assigned to the nodes in that set.
For a finite node population with measurable value spaces, a structural causal model, and a reference-measure family, observational domination holds exactly when, for every assignment of fixed-node values, the model's observational law is absolutely continuous with respect to the joint reference measure on its observed nodes.
Definition (Lean source)
For a finite node population with measurable value spaces, a structural causal model, a reference-measure family, and fixed-node values, the joint observational density is the Radon--Nikodym derivative of the model's observational law at those fixed-node values with respect to the joint reference measure on the observed nodes.
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 — For a node population with measurable value spaces, a reference-measure family, and a finite set of nodes, the σ-finiteness structure for their joint reference measure asserts that the finite product of the selected coordinate reference measures is σ-finite.
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.
For any node set with measurable node-value spaces and a family of reference measures, reference faithfulness means that every value at every random or fixed node has nonzero mass under that node's reference measure.
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 — For a collection of node labels, a family of finite base-node value spaces, and a random or fixed SWIG node, the finite enumeration of that node's value space is inherited from the finite enumeration of its corresponding base-node value space by the random-node case or by the fixed-node case.parameters -
instMeasurableSingletonClassSwigΩinstance — For a collection of node labels, a family of base-node value spaces with measurable singletons, and a random or fixed SWIG node, the measurable-singleton structure on that node's value space is inherited from its corresponding base-node value space in the random-node case or in the fixed-node case.parametersinstance -
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 — For a collection of node labels, finite measurable base-node value spaces with measurable singletons, a family of reference measures, and a random or fixed SWIG node, the reference measure at that node has finite total mass.parametersN :sharedType u_1N → Type u_2∀ n, Finite (Ω n)∀ n, MeasurableSingletonClass (Ω n)ref :v :SWIGNode Ninstancegiven byby 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 — For a collection of node labels, finite measurable base-node value spaces with measurable singletons, a family of reference measures, and a finite set of random or fixed SWIG nodes, the corresponding product reference measure has finite total mass.parametersinstancegiven byby 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.
For a finite collection of distinguishable base-variable labels and a SWIG graph, the topological linear order orders its nodes by their positions in the graph's topological ordering.
Definition (Lean source)
For a finite collection of distinguishable base-variable labels, a SWIG graph, a finite set of graph nodes, and a position from zero through one less than the set's size, the node-at-position selector returns the node occupying that position when the set is sorted in graph topological order.
For a finite collection of distinguishable base-variable labels, a SWIG graph, a finite set of graph nodes, and a node belonging to that set, the node-position selector returns that node's position when the set is sorted in graph topological order.
For a finite collection of distinguishable base-variable labels, a SWIG graph, a finite set of graph nodes, and a nonnegative integer, the topological prefix consists of the nodes in that set whose topological positions are strictly less than .
For an ambient set of graph nodes, a subset of coordinates to eliminate that is contained in the ambient set, and a nonnegative extended-real mass function on assignments to the ambient set, the marginalized mass function maps each ambient assignment to the sum of the mass function over all assignments on the eliminated coordinates, replacing those coordinates in the evaluation point.
For an ambient node set, a SWIG graph, a node set, a district node set, the condition that the node set is contained in the ambient set, and a nonnegative extended-real mass function on ambient assignments, the district factor maps each ambient assignment to the product, over the nodes of the district in graph topological order, of the ratio of the two adjacent prefix marginals obtained by summing out the remaining nodes of .
Definition (Lean source)
For an ambient node set and a SWIG graph, the mass-level IDENTIFY recursion maps every target node set, district node set, proof that the target set is contained in the ambient set, and nonnegative extended-real mass function on ambient assignments to a mass function on ambient assignments. It first forms the induced ancestral set and its containment proof, then returns the marginal eliminating the target coordinates outside the district when that ancestral set equals the district, returns the original mass function when it equals the target set, and otherwise recurses after extracting the containing district factor from the appropriate marginal.
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.hypothesesconclusionG.prefixIn D n ⊆ DProof (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.hypothesesconclusioninducedAncestral G T C ⊆ TProof (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.hypothesesconclusioncontainingCComponent G S ⊆ G.observedProof (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.
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a full assignment of its observed node values, a natural-number bound , an index , and evidence that this index is within the observed topological order, the previous-value reader returns from the assignment the value of the -th observed node in that order.
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model and a candidate node set, the latent block is the set of all unobserved nodes having a directed edge into at least one member of that set.
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)
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a fixed-node assignment, an observed-node assignment, an observed node with evidence that it is observed, and a latent-node assignment, local consistency at that node holds exactly when its structural function, is indexed by that node's canonical observed-order position and, fed the corresponding fixed, latent, and earlier observed parent values, equals its assigned observed value.
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)
For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model and a finite node set, the observed-parent-closure condition holds exactly when every member of the set is observed and every observed parent of each member also belongs to the set.
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.hypothesesN :sharedType u_1N → Type u_2M :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.hypothesesN :sharedType u_1N → Type u_2M :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.hypothesesN :sharedType u_1N → Type u_2M :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_observedlemma — For a structural causal model and observed assignment, an observed parent that precedes the current node in topological order is read by the previous-value function as its value in the assignment.hypothesesN :sharedType u_1N → Type u_2M :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_dispatchlemma — Given a finite structural causal model, fixed, observed, and latent assignments, an observed-node index, and one of that node's parents, the parent map built from preceding observed values returns the latent value for an unobserved parent, the fixed value for a fixed parent, and the observed value otherwise.hypothesesN :sharedType u_1N → Type u_2M :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_dispatchlemma — Given a finite structural causal model, fixed, observed, and latent assignments, and an observed node, local consistency at that node holds exactly when its structural function, supplied latent, fixed, or observed parent values as appropriate, equals its observed value.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs :M.FixedValuesv :SWIGNode Nhv :v ∈ M.observedℓ :M.LatentValuesconclusionM.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.hypothesesN :sharedType u_1N → Type u_2M :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.hypothesesN :sharedType u_1N → Type u_2M :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
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.
For a finite node set with measurable node-value spaces, a structural causal model, a family of reference measures, an assignment to the model's fixed nodes, and a set of SWIG nodes, assuming every observational law is finite, every singleton observed-node value space is standard Borel and nonempty, and every fixed-node space together with every observed-node prefix space satisfies the stated countability condition, the per-c-component density factor maps a full observed-node assignment to the product of its one-node conditional density factors over precisely those observed nodes whose c-component is the given set.
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.hypothesesN :sharedType u_1N → Type u_2M₁ 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 : ℕ,∀ s' : M₂.FixedValues, IsFiniteMeasure (M₂.obsKernel s')∀ (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.
For a collection of nodes with a measurable outcome space for each node, a finite set of target coordinates, a finite set of replacement coordinates, an assignment on the target coordinates, and an assignment on the replacement coordinates, the overridden target-coordinate assignment uses the replacement assignment at every target coordinate that is also a replacement coordinate, and otherwise uses the original target-coordinate assignment.
For a collection of nodes, two finite sets of nodes, and their disjointness, the index equivalence between their tagged sum and their union maps each tagged node to that same node regarded as a member of the union.
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 — For a distinguishable node population with measurable, finite-valued node spaces and a finite set of SWIG nodes, the finite enumeration structure on assignments of values to those nodes exists. -
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.Proof (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
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.
For any node set with measurable node-value spaces, provided every random or fixed node has a countable value space and every base-node singleton is measurable, the counting reference family assigns counting measure to every random and fixed node coordinate and records that each such measure is σ-finite.
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.hypothesesN :sharedType u_1N → Type u_2ref :Proof (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.hypothesesN :sharedType u_1N → Type u_2M :SCM N Ωs :M.FixedValueshP :P ⊆ M.observedx :M.ObservedValuesconclusion= 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) := by fun_prop have heval : Measurable (fun ℓ : M.LatentValues => M.evalMap s ℓ) := by fun_prop 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]
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.