Graph.Finite­Density.Ordered­Local­Markov

Ordered local-Markov consequences of finite-DAG density factorizations: topological predecessor blocks, the parent-conditioned core, arbitrary parent-superset conditioning, and the unit-cube specialization.

Coordinates 4 core · 5 supporting This module packages an arbitrary numeric topological ranking, its predecessor set, and the measurability facts for the coordinate maps used by the ordered local Markov theorem. ★ parents_subset_predecessors

Coordinate blocks for ordered finite-DAG arguments

This module packages an arbitrary numeric topological ranking, its predecessor set, and the measurability facts for the coordinate maps used by the ordered local Markov theorem.

structure TopologicalRanking reviewed
Causalean.Graph.FiniteDensity

A finite DAG is equipped with a numeric position for each vertex, distinct positions for distinct vertices, and strictly increasing positions along every directed edge.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
fields
The numeric position of a vertex.
rank :
V → ℕ
Distinct vertices have distinct positions.
injective_rank :
Injective rank
Every directed edge points from a smaller position to a larger position.
edge_lt :
∀ {u v : V}
if
G.edge u v
then
rank u < rank v
Causalean.Graph.FiniteDensity.TopologicalRanking · Causalean/Graph/FiniteDensity/OrderedLocalMarkov/Coordinates.lean:21 · uses DAG
def canonicalTopologicalRanking reviewed
Causalean.Graph.FiniteDensity

A finite DAG has the canonical topological ranking supplied by its DAG API.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
def
canonicalTopologicalRanking G :
TopologicalRanking G
given by
clause 1
rank := G.topoOrder
clause 2
injective_rank := G.topoOrder_injective
clause 3
edge_lt := G.topoOrder_lt _ _
Causalean.Graph.FiniteDensity.canonicalTopologicalRanking · Causalean/Graph/FiniteDensity/OrderedLocalMarkov/Coordinates.lean:32 · uses DAG , TopologicalRanking
def predecessors reviewed
Causalean.Graph.FiniteDensity

A topological ranking and vertex determine the finite set of vertices strictly preceding that vertex.

Definition (Lean source)
parameters
V :
Type u_1
DAG V
shared
τ :
TopologicalRanking G
i :
V
def
predecessors τ i :
Finset V
given by
Finset.univ.filter (fun j ↦ τ.rank j < τ.rank i)
Causalean.Graph.FiniteDensity.predecessors · Causalean/Graph/FiniteDensity/OrderedLocalMarkov/Coordinates.lean:38 · uses DAG , TopologicalRanking
theorem parents_subset_predecessors reviewed
Causalean.Graph.FiniteDensity

A topological ranking places every parent of a vertex among its predecessors.

Formal statement
hypotheses
V :
Type u_1
DAG V
shared
τ :
TopologicalRanking G
i :
V
conclusion
G.parents i ⊆ predecessors τ i
Proof (Lean source)
theorem parents_subset_predecessors {G : DAG V} (τ : TopologicalRanking G) (i : V) : G.parents i ⊆ predecessors τ i := by intro j hj rw [predecessors, mem_filter] exact ⟨Finset.mem_univ j, τ.edge_lt (G.mem_parents.mp hj)⟩
Causalean.Graph.FiniteDensity.parents_subset_predecessors · Causalean/Graph/FiniteDensity/OrderedLocalMarkov/Coordinates.lean:43 · uses DAG , parents , TopologicalRanking , predecessors
5 supporting declarations (lemmas, instances)
Local 1 core · 0 supporting This module isolates the analytic core: under a finite DAG density factorization, a coordinate is conditionally independent of any parent-closed block omitting it after its parents are removed, given its parents. ★ localMarkovParents_of_parentClosed

Density-factorization local Markov core

This module isolates the analytic core: under a finite DAG density factorization, a coordinate is conditionally independent of any parent-closed block omitting it after its parents are removed, given its parents. The proof is intended to combine reverse-topological marginalization with a three-block density factorization and Mathlib's conditional-independence characterization.

theorem localMarkovParents_of_parentClosed reviewed
Causalean.Graph.FiniteDensity.Factorization

For a finite DAG density factorization, a parent-closed coordinate block, and a vertex omitted from that block, the vertex coordinate is conditionally independent of the block's non-parent coordinates given its parent coordinates.

Formal statement
hypotheses
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
i :
V
P :
Finset V
hP :
ParentClosed G P
hi :
i ∉ P
conclusion
CondIndepFun (comap (coordinateProjection (X := X) (G.parents i)) inferInstance) (coordinateConditioning_comap_le (X := X) (G.parents i)) (fun x : ∀ j, X j ↦ x i) (coordinateProjection (X := X) (P \ G.parents i)) B.observationalMeasure
Proof (Lean source)
theorem Factorization.localMarkovParents_of_parentClosed (B : Factorization G X μ) {i : V} {P : Finset V} (hP : ParentClosed G P) (hi : i ∉ P) : CondIndepFun (comap (coordinateProjection (X := X) (G.parents i)) inferInstance) (coordinateConditioning_comap_le (X := X) (G.parents i)) (fun x : ∀ j, X j ↦ x i) (coordinateProjection (X := X) (P \ G.parents i)) B.observationalMeasure := by classical by_cases hfull : Nonempty (∀ j, X j) · let x₀ : ∀ j, X j := Classical.choice hfull let R : Finset V := P ∪ nodeAncestralClosure G i let C : Finset V := G.parents i let Z : Finset V := R \ insert i C let I : Finset V := {i} let S : Finset V := I ∪ (Z ∪ C) have hiR : i ∈ R := by simp [R, nodeAncestralClosure] have hCR : C ⊆ R := by intro j hj exact Finset.mem_union_right P (selfParents_subset_nodeAncestralClosure i (mem_insert_of_mem (by simpa [C] using hj))) have hiC : i ∉ C := by simpa [C, mem_parents] using G.irrefl i have hSR : S = R := by ext j simp only [S, I, Z, mem_union, mem_singleton, mem_sdiff, Finset.mem_insert] constructor · rintro (rfl | (⟨hjR, _⟩ | hjC)) · exact hiR · exact hjR · exact hCR hjC · intro hjR by_cases hji : j = i · exact Or.inl hji · by_cases hjC : j ∈ C · exact inr (inr hjC) · exact inr (Or.inl ⟨hjR, by simp [hji, hjC]⟩) have hRclosed : ParentClosed G R := by intro j hj k hk rcases Finset.mem_union.mp hj with hjP | hjA · exact Finset.mem_union_left _ (hP hjP hk) · exact Finset.mem_union_right _ (parentClosed_nodeAncestralClosure i hjA hk) have hSclosed : ParentClosed G S := hSR ▸ hRclosed have hnochild : ∀ j ∈ R, j ≠ i → i ∉ G.parents j := by intro j hjR hji hij rcases Finset.mem_union.mp hjR with hjP | hjA · exact hi (hP hjP hij) · have hjiA : G.isAncestor j i := (mem_nodeAncestralClosure_iff.mp hjA).resolve_left hji exact G.isAncestor_irrefl i (G.isAncestor_trans (Causalean.DAG.isAncestor.edge (G.mem_parents.mp hij)) hjiA) have hZC : Disjoint Z C := by apply Finset.disjoint_left.mpr intro j hjZ hjC simp only [Z, mem_sdiff] at hjZ exact hjZ.2 (mem_insert_of_mem hjC) have hIZC : Disjoint I (Z ∪ C) := by apply Finset.disjoint_left.mpr intro j hjI hj have hji : j = i := by simpa [I] using hjI subst j rcases Finset.mem_union.mp hj with hjZ | hjC · simp only [Z, mem_sdiff] at hjZ exact hjZ.2 (mem_insert_self i C) · exact hiC hjC let eZC : ((∀ j : Z, X j) × (∀ j : C, X j)) ≃ᵐ (∀ j : ↥(Z ∪ C), X j) := MeasurableEquiv.piFinsetUnion X hZC let e : ((∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j))) ≃ᵐ (∀ j : S, X j) := (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) eZC).trans (MeasurableEquiv.piFinsetUnion X hIZC) let refI : Measure (∀ j : I, X j) := Measure.pi fun j : I ↦ μ j let refZ : Measure (∀ j : Z, X j) := Measure.pi fun j : Z ↦ μ j let refC : Measure (∀ j : C, X j) := Measure.pi fun j : C ↦ μ j let refS : Measure (∀ j : S, X j) := Measure.pi fun j : S ↦ μ j have he : MeasurePreserving e (refI.prod (refZ.prod refC)) refS := by have heZC := measurePreserving_piFinsetUnion hZC μ have heProd := (MeasurePreserving.id refI).prod heZC have heOuter := measurePreserving_piFinsetUnion hIZC μ refine ⟨e.measurable, ?_⟩ have hm := (heOuter.comp heProd).map_eq change Measure.map e (refI.prod (refZ.prod refC)) = refS have hefun : (e : ((∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j))) → (∀ j : S, X j)) = fun q ↦ (MeasurableEquiv.piFinsetUnion X hIZC) (q.1, eZC q.2) := by funext q rfl rw [hefun] simpa [S, eZC, refI, refZ, refC, refS, map, Function.comp_def] using hm let ext (q : (∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j))) : ∀ j, X j := coordinateExtension S x₀ (e q) have ext_I (q : (∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j))) (j : I) : ext q j = q.1 j := by have hjS : (j : V) ∈ S := Finset.mem_union_left _ j.property unfold ext coordinateExtension rw [dif_pos hjS] change (Equiv.piFinsetUnion X hIZC) (q.1, eZC q.2) ⟨j, hjS⟩ = q.1 j exact Equiv.piFinsetUnion_left X hIZC j.property hjS have ext_Z (q : (∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j))) (j : Z) : ext q j = q.2.1 j := by have hjZC : (j : V) ∈ Z ∪ C := Finset.mem_union_left _ j.property have hjS : (j : V) ∈ S := Finset.mem_union_right _ hjZC unfold ext coordinateExtension rw [dif_pos hjS] change (Equiv.piFinsetUnion X hIZC) (q.1, eZC q.2) ⟨j, hjS⟩ = q.2.1 j rw [Equiv.piFinsetUnion_right X hIZC hjZC hjS] change (Equiv.piFinsetUnion X hZC) q.2 ⟨j, hjZC⟩ = q.2.1 j exact Equiv.piFinsetUnion_left X hZC j.property hjZC have ext_C (q : (∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j))) (j : C) : ext q j = q.2.2 j := by have hjZC : (j : V) ∈ Z ∪ C := Finset.mem_union_right _ j.property have hjS : (j : V) ∈ S := Finset.mem_union_right _ hjZC unfold ext coordinateExtension rw [dif_pos hjS] change (Equiv.piFinsetUnion X hIZC) (q.1, eZC q.2) ⟨j, hjS⟩ = q.2.2 j rw [Equiv.piFinsetUnion_right X hIZC hjZC hjS] change (Equiv.piFinsetUnion X hZC) q.2 ⟨j, hjZC⟩ = q.2.2 j exact Equiv.piFinsetUnion_right X hZC j.property hjZC let d := fun q : (∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j)) ↦ B.partialDensity S (ext q) have hd : Measurable d := by unfold d ext fun_prop let y₀ : ∀ j : I, X j := fun j ↦ x₀ j let z₀ : ∀ j : Z, X j := fun j ↦ x₀ j let a := fun q : (∀ j : I, X j) × (∀ j : C, X j) ↦ B.factor i (ext (q.1, (z₀, q.2))) let b := fun q : (∀ j : Z, X j) × (∀ j : C, X j) ↦ B.partialDensity (S.erase i) (ext (y₀, q)) have ha : Measurable a := by unfold a ext exact (B.measurable_factor i).comp ((measurable_coordinateExtension S x₀).comp (e.measurable.comp (measurable_fst.prodMk (measurable_const.prodMk measurable_snd)))) have hb : Measurable b := by unfold b ext exact (B.measurable_partialDensity (S.erase i)).comp ((measurable_coordinateExtension S x₀).comp (e.measurable.comp (measurable_const.prodMk measurable_id))) have hfactor : d = fun q ↦ a (q.1, q.2.2) * b (q.2.1, q.2.2) := by funext q have hiI : i ∈ I := by simp [I] have hiS : i ∈ S := Finset.mem_union_left _ hiI have hfirst : B.factor i (ext q) = B.factor i (ext (q.1, (z₀, q.2.2))) := by apply B.local_factor i intro k hk rcases Finset.mem_insert.mp hk with hki | hkC · subst k exact ext_I q ⟨i, hiI⟩ |>.trans (ext_I (q.1, (z₀, q.2.2)) ⟨i, hiI⟩).symm · exact ext_C q ⟨k, by simpa [C] using hkC⟩ |>.trans (ext_C (q.1, (z₀, q.2.2)) ⟨k, by simpa [C] using hkC⟩).symm have hrest : B.partialDensity (S.erase i) (ext q) = B.partialDensity (S.erase i) (ext (y₀, (q.2.1, q.2.2))) := by unfold Factorization.partialDensity apply Finset.prod_congr rfl intro j hj apply B.local_factor j have hj' := Finset.mem_erase.mp hj have hjS : j ∈ S := hj'.2 have hji : j ≠ i := hj'.1 have hjR : j ∈ R := hSR ▸ hjS have hij : i ∉ G.parents j := hnochild j hjR hji intro k hk have hkS : k ∈ S := by rcases Finset.mem_insert.mp hk with rfl | hkj · exact hjS · exact hSclosed hjS hkj have hki : k ≠ i := by rcases Finset.mem_insert.mp hk with hkj | hkp · exact hkj.trans_ne hji · exact fun h ↦ hij (h ▸ hkp) rcases Finset.mem_union.mp hkS with hkI | hkZC · have hki' : k = i := by simpa [I] using hkI exact (hki hki').elim · rcases Finset.mem_union.mp hkZC with hkZ | hkC · exact ext_Z q ⟨k, hkZ⟩ |>.trans (ext_Z (y₀, (q.2.1, q.2.2)) ⟨k, hkZ⟩).symm · exact ext_C q ⟨k, hkC⟩ |>.trans (ext_C (y₀, (q.2.1, q.2.2)) ⟨k, hkC⟩).symm unfold d a b calc B.partialDensity S (ext q) = B.factor i (ext q) * B.partialDensity (S.erase i) (ext q) := by unfold Factorization.partialDensity exact (Finset.mul_prod_erase S (fun j ↦ B.factor j (ext q)) hiS).symm _ = B.factor i (ext (q.1, (z₀, q.2.2))) * B.partialDensity (S.erase i) (ext (y₀, (q.2.1, q.2.2))) := by rw [hfirst, hrest] let φ : (∀ j, X j) → ((∀ j : I, X j) × ((∀ j : Z, X j) × (∀ j : C, X j))) := e.symm ∘ coordinateProjection S have hφ : Measurable φ := e.symm.measurable.comp (measurable_coordinateProjection S) have hlaw : Measure.map φ B.observationalMeasure = (refI.prod (refZ.prod refC)).withDensity d := by let dS : (∀ j : S, X j) → ℝ≥0∞ := fun z ↦ B.partialDensity S (coordinateExtension S x₀ z) have hdS : Measurable dS := by unfold dS exact (B.measurable_partialDensity S).comp (measurable_coordinateExtension S x₀) have hproj := map_coordinateProjection_withDensity_eq_marginal (X := X) (μ := μ) S B.observationalDensity B.measurable_observationalDensity x₀ rw [B.lmarginal_compl_observationalDensity_eq hSclosed] at hproj change Measure.map (coordinateProjection (X := X) S) B.observationalMeasure = refS.withDensity dS at hproj calc Measure.map φ B.observationalMeasure = Measure.map e.symm (Measure.map (coordinateProjection (X := X) S) B.observationalMeasure) := by symm simpa [φ, Function.comp_def] using Measure.map_map e.symm.measurable (measurable_coordinateProjection S) (μ := B.observationalMeasure) _ = Measure.map e.symm (refS.withDensity dS) := by rw [hproj] _ = (refI.prod (refZ.prod refC)).withDensity d := by have heSymm : MeasurePreserving e.symm refS (refI.prod (refZ.prod refC)) := MeasurePreserving.symm e he simpa [dS, d, ext, Function.comp_def] using map_withDensity_equiv_of_measurePreserving e.symm heSymm dS hdS have hfinite : IsFiniteMeasure -- … truncated; follow the source link for the rest …
Causalean.Graph.FiniteDensity.Factorization.localMarkovParents_of_parentClosed · Causalean/Graph/FiniteDensity/OrderedLocalMarkov/Local.lean:164 · uses DAG , parents , Factorization , instIsFiniteMeasureObservationalMeasure , observationalMeasure , ParentClosed , coordinateConditioning_comap_le , coordinateProjection
Main 1 core · 4 supporting This module derives the arbitrary-conditioning-superset form of the local Markov property and specializes it to predecessor sets from arbitrary and canonical topological rankings. ★ orderedLocalMarkov

Ordered local Markov property for finite DAG density factorizations

This module derives the arbitrary-conditioning-superset form of the local Markov property and specializes it to predecessor sets from arbitrary and canonical topological rankings. It also exports the unit-cube version using the existing unit-cube reference measure.

theorem orderedLocalMarkov reviewed
Causalean.Graph.FiniteDensity.Factorization

For a finite DAG density factorization, an arbitrary topological ranking, a vertex, a conditioning predecessor set, and proof that it lies among the predecessors and contains every parent, the vertex coordinate is conditionally independent of all other predecessors given that set.

Formal statement
hypotheses
V :
Type u_1
V → Type u_2
(i : V) → MeasurableSpace (X i)
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
τ :
TopologicalRanking G
i :
V
A :
Finset V
hA :
A ⊆ predecessors τ i
hpa :
G.parents i ⊆ A
conclusion
CondIndepFun (comap (coordinateProjection (X := X) A) inferInstance) (coordinateConditioning_comap_le (X := X) A) (fun x : ∀ j, X j ↦ x i) (coordinateProjection (X := X) (predecessors τ i \ A)) B.observationalMeasure
Proof (Lean source)
theorem Factorization.orderedLocalMarkov (B : Factorization G X μ) (τ : TopologicalRanking G) (i : V) (A : Finset V) (hA : A ⊆ predecessors τ i) (hpa : G.parents i ⊆ A) : CondIndepFun (comap (coordinateProjection (X := X) A) inferInstance) (coordinateConditioning_comap_le (X := X) A) (fun x : ∀ j, X j ↦ x i) (coordinateProjection (X := X) (predecessors τ i \ A)) B.observationalMeasure := by exact B.localMarkovSuperset_of_parentClosed (parentClosed_predecessors τ i) (not_mem_predecessors τ i) hA hpa
Causalean.Graph.FiniteDensity.Factorization.orderedLocalMarkov · Causalean/Graph/FiniteDensity/OrderedLocalMarkov/Main.lean:179 · uses DAG , parents , Factorization , instIsFiniteMeasureObservationalMeasure , observationalMeasure , TopologicalRanking , coordinateConditioning_comap_le , predecessors , coordinateProjection
4 supporting declarations (lemmas, instances)