Stat.FinitePositiveTable.DAG
This roll-up module exports positive finite DAG table factorizations, coordinate-fixing expansions, reverse-topological normalization, finite-atom conditional-independence bridges, and global Markov theorems for the resu
Basic 5 core · 4 supporting This module packages a strictly positive finite table together with normalized parent-local DAG factors. ★ parentFixingSteps_valid
Positive finite DAG tables and arrowhead removal
This module packages a strictly positive finite table together with normalized parent-local DAG factors. It also defines the graph and algebraic objects used by coordinate fixing: the product of the factors not yet fixed, parent-conditioned fixing steps, and the DAG obtained by removing every arrowhead into a fixed vertex.
The package deliberately reuses FinitePositiveTable for profiles, fibre sums, marginals, and
fixing, and PositiveFiniteDAGMechanism for normalized local factors.
structure PositiveDAGTableFactorization reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG
A DAG and strictly positive finite table have a normalized parent-local factorization when every coordinate has at least one state, each vertex carries a strictly positive local factor that depends only on the vertex and its parents and sums to one over the vertex's own value, and the table mass of every complete profile is the product of all the local factors at that profile.
Definition (Lean source)
parameters
fields
Every coordinate alphabet contains at least one state.
cardinalitiesPositive :
The normalized, strictly positive, parent-local factors.
mechanism :
PositiveFiniteDAGMechanism G (fun v ↦ Fin (r v))
The table mass is the product of the local factors.
mass_eq_jointMass :
∀ x, p.mass x = mechanism.jointMass x
def remainingFactorKernel reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
A factorized table and fixed vertex set determine the truncated product kernel by multiplying, at each complete profile, exactly the local factors of the vertices outside the fixed set.
def parentFixingSteps reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
A DAG and vertex list determine the parent-conditioned fixing steps by pairing each listed vertex, in order, with its DAG parent set as the conditioning set.
Definition (Lean source)
parameters
def
given by
vertices.map fun v ↦ ⟨v, G.parents v⟩
theorem parentFixingSteps_valid reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
A DAG, vertex list, and proof that the vertices are distinct give a valid parent-conditioned fixing sequence: the fixed coordinates are distinct and no step conditions on its own coordinate.
Formal statement
hypotheses
conclusion
FixingSequenceValid (parentFixingSteps G vertices)
Proof (Lean source)
theorem parentFixingSteps_valid (G : DAG V) (vertices : List V)
(hvertices : vertices.Nodup) :
FixingSequenceValid (parentFixingSteps G vertices) := by
/-
Unfold both definitions. Mapping `FixingStep.coordinate` over the constructed list is
definitionally `vertices`; the second conjunct is `v ∉ G.parents v`, which follows from
`DAG.irrefl` through `DAG.mem_parents`.
-/
constructor
· simpa [parentFixingSteps, List.map_map, Function.comp_def] using hvertices
· intro s hs
simp only [parentFixingSteps, List.mem_map] at hs
obtain ⟨v, hv, rfl⟩ := hs
exact fun h ↦ G.irrefl v (G.mem_parents.mp h)
def arrowheadRemovedDAG reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
A DAG and fixed vertex set determine the DAG with incoming arrows to fixed vertices removed: an edge remains exactly when its target is unfixed, edge decidability is inherited, and acyclicity is preserved.
Definition (Lean source)
parameters
def
given by
clause 1
edge u v := G.edge u v ∧ v ∉ fixed
clause 2
decEdge := inferInstance
clause 3
acyclic := by intro v hcycle exact G.acyclic v ((Relation.TransGen.mono (r := fun u v ↦ G.edge u v ∧ v ∉ fixed) (p := G.edge) (fun _ _ h ↦ h.1)) v v hcycle)
4 supporting declarations (lemmas, instances)
-
arrowheadRemovedDAG_edge_ifftheorem — A DAG, fixed vertex set, and ordered vertex pair satisfy the exact edge-survival criterion after arrowhead removal.hypothesesconclusion(arrowheadRemovedDAG G fixed).edge u v ↔ G.edge u v ∧ v ∉ fixedProof (Lean source)
@[simp] theorem arrowheadRemovedDAG_edge_iff (G : DAG V) (fixed : Finset V) (u v : V) : (arrowheadRemovedDAG G fixed).edge u v ↔ G.edge u v ∧ v ∉ fixed := by rfl -
arrowheadRemovedDAG_fixed_parents_emptytheorem — A DAG, fixed vertex set, and proof that a vertex is fixed give an empty parent set for that vertex after arrowhead removal.hypothesesconclusion(arrowheadRemovedDAG G fixed).parents v = ∅Proof (Lean source)
theorem arrowheadRemovedDAG_fixed_parents_empty (G : DAG V) (fixed : Finset V) {v : V} (hv : v ∈ fixed) : (arrowheadRemovedDAG G fixed).parents v = ∅ := by ext u simp [DAG.mem_parents, hv] -
arrowheadRemovedDAG_random_parentstheorem — A DAG, fixed vertex set, and proof that a vertex remains random give the original parent set for that vertex after arrowhead removal.hypothesesconclusion(arrowheadRemovedDAG G fixed).parents v = G.parents vProof (Lean source)
theorem arrowheadRemovedDAG_random_parents (G : DAG V) (fixed : Finset V) {v : V} (hv : v ∉ fixed) : (arrowheadRemovedDAG G fixed).parents v = G.parents v := by ext u simp [DAG.mem_parents, hv] -
fixed_disjoint_remainingtheorem — A fixed vertex set has no vertex in common with its remaining complement.Proof (Lean source)
theorem fixed_disjoint_remaining (fixed : Finset V) : Disjoint fixed (univ \ fixed) := by rw [Finset.disjoint_left] intro v hvFixed hvRemaining exact (Finset.mem_sdiff.mp hvRemaining).2 hvFixed
KernelCI 4 core · 1 supporting This module isolates the graph-independent part of the substrate. ★ condIndepFun_finiteAtom_crossProduct
Finite-kernel conditional independence bridges
This module isolates the graph-independent part of the substrate. It defines set-valued
conditional independence for a finite kernel, converts Causalean's measure-theoretic
CondIndepFun into the corresponding finite-atom cross-product equality, and relates the
set-valued predicate to the existing two-coordinate KernelCondIndep API.
def fixedKernelMarginal reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG
A kernel, fixed and requested random coordinate sets, and profile determine the corresponding fixed-row kernel marginal as the sum of the kernel over all complete profiles that agree with the given profile on every fixed and every requested coordinate.
Definition (Lean source)
def FixedKernelCondIndepAt reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG
A kernel, fixed, two random, and conditioning coordinate sets, and profile determine the fixed-row atomwise conditional-independence identity: the fixed-row marginal over the two random sets and the conditioning set, times the fixed-row marginal over the conditioning set, equals the product of the fixed-row marginals over each random set joined with the conditioning set.
Definition (Lean source)
parameters
def
FixedKernelCondIndepAt q fixed X Y Z x :
Prop
given by
fixedKernelMarginal q fixed (X ∪ Y ∪ Z) x * fixedKernelMarginal q fixed Z x
= fixedKernelMarginal q fixed (X ∪ Z) x * fixedKernelMarginal q fixed (Y ∪ Z) x
def FixedKernelCondIndep reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG
A kernel and fixed, two random, and conditioning coordinate sets determine fixed-row conditional independence by requiring the atomwise identity at every profile.
Definition (Lean source)
parameters
def
FixedKernelCondIndep q fixed X Y Z :
Prop
given by
FixedKernelCondIndepAt q fixed X Y Z x
theorem condIndepFun_finiteAtom_crossProduct reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG
On a standard Borel space with a finite measure, let three random elements with finite value sets be measurable, with the first two conditionally independent given the third. Then for any three values, the measure of the event that all three elements take these values, times the measure of the event that the third takes its value, equals the measure of the event that the first and third take their values times the measure of the event that the second and third take theirs.
Formal statement
hypotheses
Ω :
Type uΩ
A :
Type uA
B :
Type uB
C :
Type uC
Fintype A
Fintype B
Fintype C
mu :
f :
Ω → A
g :
Ω → B
c :
Ω → C
hf :
hg :
hc :
hci :
a :
A
b :
B
c₀ :
C
conclusion
mu.real (((f ⁻¹' {a}) ∩ (g ⁻¹' {b})) ∩ (c ⁻¹' {c₀})) * mu.real (c ⁻¹' {c₀})
= mu.real ((f ⁻¹' {a}) ∩ (c ⁻¹' {c₀})) * mu.real ((g ⁻¹' {b}) ∩ (c ⁻¹' {c₀}))
Proof (Lean source)
theorem condIndepFun_finiteAtom_crossProduct
{Ω : Type uΩ} {A : Type uA} {B : Type uB} {C : Type uC}
[MeasurableSpace Ω] [StandardBorelSpace Ω]
[Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
[Fintype B] [MeasurableSpace B] [MeasurableSingletonClass B]
[Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C]
(mu : Measure Ω) [IsFiniteMeasure mu]
(f : Ω → A) (g : Ω → B) (c : Ω → C)
(hf : Measurable f) (hg : Measurable g) (hc : Measurable c)
(hci : CondIndepFun (comap c inferInstance)
hc.comap_le f g mu)
(a : A) (b : B) (c₀ : C) :
mu.real (((f ⁻¹' {a}) ∩ (g ⁻¹' {b})) ∩ (c ⁻¹' {c₀})) *
mu.real (c ⁻¹' {c₀}) =
mu.real ((f ⁻¹' {a}) ∩ (c ⁻¹' {c₀})) *
mu.real ((g ⁻¹' {b}) ∩ (c ⁻¹' {c₀})) := by
classical
let F := c ⁻¹' {c₀}
by_cases hzero : mu.real F = 0
· have hjoint : mu.real (((f ⁻¹' {a}) ∩ (g ⁻¹' {b})) ∩ F) = 0 :=
le_antisymm (hzero ▸ measureReal_mono Set.inter_subset_right) measureReal_nonneg
have hfiber : mu.real ((f ⁻¹' {a}) ∩ F) = 0 :=
le_antisymm (hzero ▸ measureReal_mono Set.inter_subset_right) measureReal_nonneg
have hgiber : mu.real ((g ⁻¹' {b}) ∩ F) = 0 :=
le_antisymm (hzero ▸ measureReal_mono Set.inter_subset_right) measureReal_nonneg
simpa [F, hzero, hjoint, hfiber, hgiber]
· have hci_atoms :=
(condIndepFun_iff_condExp_inter_preimage_eq_mul hf hg).mp hci
{a} {b} (measurableSet_singleton a) (measurableSet_singleton b)
have hjoint := condExp_indicator_finite_comap_local mu c hc
((f ⁻¹' {a}) ∩ (g ⁻¹' {b}))
((hf (measurableSet_singleton a)).inter (hg (measurableSet_singleton b)))
have hfiber := condExp_indicator_finite_comap_local mu c hc
(f ⁻¹' {a}) (hf (measurableSet_singleton a))
have hgiber := condExp_indicator_finite_comap_local mu c hc
(g ⁻¹' {b}) (hg (measurableSet_singleton b))
have hratio : ∀ᵐ omega ∂mu,
finiteComapCondProb mu c ((f ⁻¹' {a}) ∩ (g ⁻¹' {b})) (c omega) =
finiteComapCondProb mu c (f ⁻¹' {a}) (c omega) *
finiteComapCondProb mu c (g ⁻¹' {b}) (c omega) := by
filter_upwards [hci_atoms, hjoint, hfiber, hgiber] with omega hciω hjω hfω hgω
exact hjω.symm.trans (hciω.trans (congrArg₂ (· * ·) hfω hgω))
have hmuF : mu F ≠ 0 := by
intro hF
apply hzero
simp only [Measure.real, hF, ENNReal.toReal_zero]
have hnebot : (ae (mu.restrict F)).NeBot := ae_restrict_neBot.mpr hmuF
have hratioF : ∀ᵐ omega ∂mu.restrict F,
finiteComapCondProb mu c ((f ⁻¹' {a}) ∩ (g ⁻¹' {b})) (c omega) =
finiteComapCondProb mu c (f ⁻¹' {a}) (c omega) *
finiteComapCondProb mu c (g ⁻¹' {b}) (c omega) :=
hratio.filter_mono (@ae_restrict_le Ω _ mu F)
have hmemF : ∀ᵐ omega ∂mu.restrict F, omega ∈ F :=
ae_restrict_mem (hc (measurableSet_singleton c₀))
letI : (ae (mu.restrict F)).NeBot := hnebot
obtain ⟨omega, hωratio, hωF⟩ := (hratioF.and hmemF).exists
have hcω : c omega = c₀ := by simpa [F] using hωF
unfold finiteComapCondProb at hωratio
simp only [hcω] at hωratio
change (mu.real F)⁻¹ *
mu.real (F ∩ ((f ⁻¹' {a}) ∩ (g ⁻¹' {b}))) =
((mu.real F)⁻¹ * mu.real (F ∩ (f ⁻¹' {a}))) *
((mu.real F)⁻¹ * mu.real (F ∩ (g ⁻¹' {b}))) at hωratio
field_simp at hωratio
simpa [F, Set.inter_comm, Set.inter_left_comm, Set.inter_assoc, mul_comm] using hωratio
1 supporting declaration (lemmas, instances)
-
fixedKernelCondIndep_complement_iff_kernelCondIndeptheorem — A kernel, fixed vertex set, two vertices, proofs that they are unfixed, and proof that they are distinct give the equivalence between set-valued fixed-row independence and the existing singleton kernel identity.hypothesesV :sharedType uV → ℕq :Kernel rfixed :Finset Va b :Vha :a ∉ fixedhb :b ∉ fixedhab :a ≠ bconclusion↔ KernelCondIndep q a bProof (Lean source)
theorem fixedKernelCondIndep_complement_iff_kernelCondIndep (q : Kernel r) (fixed : Finset V) (a b : V) (ha : a ∉ fixed) (hb : b ∉ fixed) (hab : a ≠ b) : FixedKernelCondIndep q fixed {a} {b} (((univ \ fixed).erase a).erase b) ↔ KernelCondIndep q a b := by classical let Z := ((univ \ fixed).erase a).erase b have hfull : fixed ∪ ({a} ∪ {b} ∪ Z) = univ := by ext v by_cases hva : v = a <;> by_cases hvb : v = b <;> by_cases hvf : v ∈ fixed <;> simp_all [Z] have hcond : fixed ∪ Z = (Finset.univ.erase a).erase b := by ext v by_cases hva : v = a <;> by_cases hvb : v = b <;> by_cases hvf : v ∈ fixed <;> simp_all [Z] have hrow : fixed ∪ ({a} ∪ Z) = Finset.univ.erase b := by ext v by_cases hva : v = a <;> by_cases hvb : v = b <;> by_cases hvf : v ∈ fixed <;> simp_all [Z] have hcolumn : fixed ∪ ({b} ∪ Z) = Finset.univ.erase a := by ext v by_cases hva : v = a <;> by_cases hvb : v = b <;> by_cases hvf : v ∈ fixed <;> simp_all [Z] have hmass_full (x : ProfileSpace r) : kernelMarginalMass q (fixed ∪ ({a} ∪ {b} ∪ Z)) x = q x := by rw [hfull, kernelMarginalMass, fiberSum_univ] have hmass_row (x : ProfileSpace r) : kernelMarginalMass q (fixed ∪ ({a} ∪ Z)) x = coordinateRowMass q b x := by rw [hrow] unfold coordinateRowMass unfold kernelMarginalMass rw [← sum_fiberSum_insert_update q (S := Finset.univ.erase b) (v := b) (by simp) x] simp only [mem_univ, insert_erase, fiberSum_univ] have hmass_column (x : ProfileSpace r) : kernelMarginalMass q (fixed ∪ ({b} ∪ Z)) x = coordinateColumnMass q a x := by rw [hcolumn] unfold coordinateColumnMass unfold kernelMarginalMass rw [← sum_fiberSum_insert_update q (S := Finset.univ.erase a) (v := a) (by simp) x] simp only [mem_univ, insert_erase, fiberSum_univ] have hmass_rectangle (x : ProfileSpace r) : kernelMarginalMass q (fixed ∪ Z) x = coordinateRectangleMass q a b x := by rw [hcond] unfold kernelMarginalMass rw [← sum_fiberSum_insert_update q (S := (Finset.univ.erase a).erase b) (v := b) (by simp) x] have hinsert : insert b ((Finset.univ.erase a).erase b) = Finset.univ.erase a := by ext v by_cases hva : v = a <;> by_cases hvb : v = b <;> simp_all rw [hinsert] simp_rw [← sum_fiberSum_insert_update q (S := Finset.univ.erase a) (v := a) (by simp) (update x b _)] simp only [mem_univ, insert_erase, fiberSum_univ] unfold coordinateRectangleMass rw [Finset.sum_comm] apply Finset.sum_congr rfl intro zb hzb apply Finset.sum_congr rfl intro za hza rw [Function.update_comm hab.symm] unfold FixedKernelCondIndep KernelCondIndep constructor <;> intro h x · have hx := h x unfold FixedKernelCondIndepAt fixedKernelMarginal at hx change kernelMarginalMass q (fixed ∪ ({a} ∪ {b} ∪ Z)) x * kernelMarginalMass q (fixed ∪ Z) x = kernelMarginalMass q (fixed ∪ ({a} ∪ Z)) x * kernelMarginalMass q (fixed ∪ ({b} ∪ Z)) x at hx unfold KernelCondIndepAt rw [hmass_full, hmass_rectangle, hmass_row, hmass_column] at hx exact hx · unfold KernelCondIndepAt at h unfold FixedKernelCondIndepAt fixedKernelMarginal rw [hmass_full, hmass_rectangle, hmass_row, hmass_column] exact h x
Elimination 1 core · 7 supporting This module isolates the finite-sum algebra behind DAG fixing. ★ remainingFactorKernel_row_normalized
Reverse-topological elimination for truncated finite DAG products
This module isolates the finite-sum algebra behind DAG fixing. A maximal remaining vertex can be summed out because no other remaining local factor depends on it and its own local row is normalized. Iterating this reverse-topological step normalizes every row of a truncated product and identifies the conditional mass used by graph-independent fixing with the vertex's local factor.
theorem remainingFactorKernel_row_normalized reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
A factorized table, fixed vertex set, and profile give unit total mass for the truncated product in that fixed-coordinate row: the product of the local factors of the unfixed vertices, summed over all complete profiles that agree with the given profile on the fixed set, equals one.
Formal statement
hypotheses
conclusion
kernelMarginalMass (fac.remainingFactorKernel fixed) fixed x = 1
Proof (Lean source)
theorem remainingFactorKernel_row_normalized
(fac : PositiveDAGTableFactorization G p) (fixed : Finset V)
(x : ProfileSpace r) :
kernelMarginalMass (fac.remainingFactorKernel fixed) fixed x = 1 := by
/-
Induct on `card (univ \ fixed)`. The empty case reduces the fibre to `x` and the empty
product to one. Otherwise select `exists_remaining_sink`, partition the fibre with
`kernelMarginalMass_decompose`, rewrite each summand by `sum_remainingFactorKernel_sink`,
and apply the induction hypothesis to `insert v fixed`.
-/
classical
induction hcard : (univ \ fixed).card using Nat.strong_induction_on generalizing fixed x with
| h n ih =>
by_cases hne : (univ \ fixed).Nonempty
· obtain ⟨v, hv, hsink⟩ := exists_remaining_sink G fixed hne
have hlt : (univ \ insert v fixed).card < n := by
rw [← hcard]
simpa [Finset.sdiff_insert] using
Finset.card_erase_lt_of_mem (Finset.mem_sdiff.mpr ⟨Finset.mem_univ v, hv⟩)
rw [kernelMarginalMass_eliminate_coordinate
(fac.remainingFactorKernel fixed)
(fac.remainingFactorKernel (insert v fixed)) (S := fixed) (v := v) hv
(fac.sum_remainingFactorKernel_sink fixed hv hsink) x]
exact ih _ hlt (insert v fixed) x rfl
· have hempty : univ \ fixed = ∅ := Finset.not_nonempty_iff_eq_empty.mp hne
have hfixed : fixed = univ := by
ext w
simpa using congrArg (w ∈ ·) hempty
subst fixed
rw [kernelMarginalMass, fiberSum_univ, remainingFactorKernel]
simp
7 supporting declarations (lemmas, instances)
-
remainingFactorKernel_postheorem — A factorized table and fixed vertex set give strictly positive mass at every profile for the truncated product kernel.Proof (Lean source)
theorem remainingFactorKernel_pos (fac : PositiveDAGTableFactorization G p) (fixed : Finset V) : (fac.remainingFactorKernel fixed).IsStrictlyPositive := by intro x exact Finset.prod_pos fun v _ ↦ fac.mechanism.factor_pos v x -
kernelMarginalMass_decomposetheorem — A kernel, coordinate outside the marginal set, and reference profile give the finite decomposition of its marginal across that coordinate's states.hypothesesconclusion= kernelMarginalMass q S xProof (Lean source)
theorem kernelMarginalMass_decompose (q : Kernel r) {S : Finset V} {v : V} (hv : v ∉ S) (x : ProfileSpace r) : (∑ z : Fin (r v), kernelMarginalMass q (insert v S) (update x v z)) = kernelMarginalMass q S x := by simpa [kernelMarginalMass] using sum_fiberSum_insert_update q hv x -
kernelMarginalMass_eliminate_coordinatetheorem — Two kernels, a coordinate outside the marginal set, a pointwise coordinate-summation identity, and reference profile give the corresponding elimination identity for kernel marginals.Proof (Lean source)
theorem kernelMarginalMass_eliminate_coordinate (q qNext : Kernel r) {S : Finset V} {v : V} (hv : v ∉ S) (hsum : ∀ y, (∑ z : Fin (r v), q (update y v z)) = qNext y) (x : ProfileSpace r) : kernelMarginalMass q S x = kernelMarginalMass qNext (insert v S) x := by classical let e := Equiv.piSplitAt v (fun i ↦ Fin (r i)) let base (t : ∀ j : {j // j ≠ v}, Fin (r j)) : ProfileSpace r := e.symm (x v, t) have hbase_v (t : ∀ j : {j // j ≠ v}, Fin (r j)) : base t v = x v := by simp [base, e, Equiv.piSplitAt] have hupdate (t : ∀ j : {j // j ≠ v}, Fin (r j)) (z : Fin (r v)) : update (base t) v z = e.symm (z, t) := by funext i by_cases hiv : i = v · subst i simp [base, e, Equiv.piSplitAt] · simp [base, e, Equiv.piSplitAt, hiv] have hagree (t : ∀ j : {j // j ≠ v}, Fin (r j)) (z : Fin (r v)) : AgreeOn S (e.symm (z, t)) x ↔ AgreeOn S (base t) x := by constructor <;> intro h w hw · simpa only [← hupdate t z, Function.update_of_ne (ne_of_mem_of_not_mem hw hv)] using h w hw · have hwv : w ≠ v := ne_of_mem_of_not_mem hw hv simpa only [← hupdate t z, Function.update_of_ne hwv] using h w hw have hagree_insert (t : ∀ j : {j // j ≠ v}, Fin (r j)) (z : Fin (r v)) : AgreeOn (insert v S) (e.symm (z, t)) x ↔ z = x v ∧ AgreeOn S (base t) x := by rw [← hupdate t z] constructor · intro h constructor · simpa using h v (mem_insert_self v S) · intro w hw have hwv : w ≠ v := ne_of_mem_of_not_mem hw hv simpa only [Function.update_of_ne hwv] using h w (mem_insert_of_mem hw) · rintro ⟨rfl, h⟩ w hw rcases mem_insert.mp hw with rfl | hw · simp · have hwv : w ≠ v := ne_of_mem_of_not_mem hw hv simpa only [Function.update_of_ne hwv] using h w hw unfold kernelMarginalMass fiberSum calc (∑ y : ProfileSpace r, if AgreeOn S y x then q y else 0) = ∑ a : Fin (r v) × (∀ j : {j // j ≠ v}, Fin (r j)), if AgreeOn S (e.symm a) x then q (e.symm a) else 0 := by exact Fintype.sum_equiv e _ _ (fun y ↦ by simp) _ = ∑ t : (∀ j : {j // j ≠ v}, Fin (r j)), ∑ z : Fin (r v), if AgreeOn S (e.symm (z, t)) x then q (e.symm (z, t)) else 0 := by rw [Fintype.sum_prod_type, Finset.sum_comm] _ = ∑ t : (∀ j : {j // j ≠ v}, Fin (r j)), if AgreeOn S (base t) x then qNext (base t) else 0 := by apply Finset.sum_congr rfl intro t ht simp_rw [hagree t] split_ifs with h · simp_rw [← hupdate t] exact hsum (base t) · simp _ = ∑ a : Fin (r v) × (∀ j : {j // j ≠ v}, Fin (r j)), if AgreeOn (insert v S) (e.symm a) x then qNext (e.symm a) else 0 := by rw [Fintype.sum_prod_type, Finset.sum_comm] apply Finset.sum_congr rfl intro t ht simp_rw [hagree_insert t] rw [Finset.sum_eq_single (x v)] · simp [base] · intro z hz hne simp [hne] · intro hnot exact (hnot (Finset.mem_univ _)).elim _ = ∑ y : ProfileSpace r, if AgreeOn (insert v S) y x then qNext y else 0 := by symm exact Fintype.sum_equiv e _ _ (fun y ↦ by simp) -
exists_remaining_sinktheorem — A DAG, fixed vertex set, and nonempty set of remaining vertices give a remaining vertex with no remaining child.hypothesesconclusion∃ v,v ∉ fixedconclusion 1w :w ∉ fixed¬ G.edge v wProof (Lean source)
theorem exists_remaining_sink (G : DAG V) (fixed : Finset V) (hne : (univ \ fixed).Nonempty) : ∃ v, v ∉ fixed ∧ ∀ w, w ∉ fixed → ¬ G.edge v w := by /- Choose a vertex maximizing `G.topoOrder` on `univ \ fixed`. An edge to another remaining vertex would strictly increase `topoOrder`, contradicting maximality. `Finset.exists_max_image` is the same selection lemma used by the ordered-local d-separation closure. -/ obtain ⟨v, hv, hmax⟩ := Finset.exists_max_image (univ \ fixed) G.topoOrder hne refine ⟨v, (Finset.mem_sdiff.mp hv).2, ?_⟩ intro w hw hEdge have hwRemaining : w ∈ univ \ fixed := Finset.mem_sdiff.mpr ⟨Finset.mem_univ w, hw⟩ exact (not_lt_of_ge (hmax w hwRemaining)) (G.topoOrder_lt v w hEdge) -
sum_remainingFactorKernel_sinktheorem — A factorized table, fixed vertex set, remaining vertex, proof that it has no remaining child, and profile give the identity obtained by summing out that sink's local factor.hypothesesProof (Lean source)
theorem sum_remainingFactorKernel_sink (fac : PositiveDAGTableFactorization G p) (fixed : Finset V) {v : V} (hv : v ∉ fixed) (hsink : ∀ w, w ∉ fixed → ¬ G.edge v w) (x : ProfileSpace r) : (∑ z : Fin (r v), fac.remainingFactorKernel fixed (update x v z)) = fac.remainingFactorKernel (insert v fixed) x := by /- Split the product into the factor at `v` and the remaining factors. For any remaining `w ≠ v`, locality of factor `w` and `hsink w` show that updating `v` does not change it. Pull this common product outside the sum and apply `factor_normalized v x`. -/ let S : Finset V := univ \ fixed have hvS : v ∈ S := Finset.mem_sdiff.mpr ⟨Finset.mem_univ v, hv⟩ have hrest (z : Fin (r v)) : (∏ w ∈ S.erase v, fac.mechanism.factor w (update x v z)) = ∏ w ∈ S.erase v, fac.mechanism.factor w x := by apply Finset.prod_congr rfl intro w hw apply fac.mechanism.factor_local w intro i hi have hwS : w ∈ S := Finset.mem_of_mem_erase hw have hwFixed : w ∉ fixed := (Finset.mem_sdiff.mp hwS).2 have hwne : w ≠ v := (Finset.mem_erase.mp hw).1 have hvNotLocal : v ∉ insert w (G.parents w) := by simp only [Finset.mem_insert, not_or] exact ⟨Ne.symm hwne, fun hvParent ↦ hsink w hwFixed (G.mem_parents.mp hvParent)⟩ have hine : i ≠ v := fun hiv ↦ hvNotLocal (hiv ▸ hi) exact Function.update_of_ne hine z x rw [remainingFactorKernel] simp only [S] at hvS hrest ⊢ calc (∑ z : Fin (r v), ∏ w ∈ (univ \ fixed), fac.mechanism.factor w (update x v z)) = ∑ z : Fin (r v), fac.mechanism.factor v (update x v z) * ∏ w ∈ (univ \ fixed).erase v, fac.mechanism.factor w (update x v z) := by apply Finset.sum_congr rfl intro z hz exact (Finset.mul_prod_erase (univ \ fixed) (fun w ↦ fac.mechanism.factor w (update x v z)) hvS).symm _ = ∑ z : Fin (r v), fac.mechanism.factor v (update x v z) * ∏ w ∈ (univ \ fixed).erase v, fac.mechanism.factor w x := by apply Finset.sum_congr rfl intro z hz rw [hrest z] _ = (∑ z : Fin (r v), fac.mechanism.factor v (update x v z)) * ∏ w ∈ (univ \ fixed).erase v, fac.mechanism.factor w x := by rw [Finset.sum_mul] _ = ∏ w ∈ (univ \ fixed).erase v, fac.mechanism.factor w x := by rw [fac.mechanism.factor_normalized, one_mul] _ = ∏ w ∈ (univ \ insert v fixed), fac.mechanism.factor w x := by congr 1 ext w simp -
remainingFactorKernel_conditionalMass_eq_factortheorem — A factorized table, fixed vertex set, proof that the vertex remains random, profile, and proposed vertex state give the equality between the truncated kernel's parent-conditional mass and its normalized local factor.hypothesesconclusionkernelConditionalMass (fac.remainingFactorKernel fixed) v (G.parents v) x z= fac.mechanism.factor v (update x v z)Proof (Lean source)
theorem remainingFactorKernel_conditionalMass_eq_factor (fac : PositiveDAGTableFactorization G p) (fixed : Finset V) {v : V} (hv : v ∉ fixed) (x : ProfileSpace r) (z : Fin (r v)) : kernelConditionalMass (fac.remainingFactorKernel fixed) v (G.parents v) x z = fac.mechanism.factor v (update x v z) := by /- Expand numerator and denominator as truncated-product fibre sums. Reverse-topologically eliminate every remaining vertex except `v` and its parents; locality makes the surviving numerator equal the factor at `v` times the denominator. Strict positivity from `remainingFactorKernel_pos` cancels the denominator. This is the finite-table form of the ordered local Markov calculation and should reuse `remainingFactorKernel_row_normalized`. -/ classical let (i : V) : Nonempty (Fin (r i)) := ⟨⟨0, fac.cardinalitiesPositive i⟩⟩ let M : PositiveFiniteDAGMechanism G (fun i ↦ Fin (r i)) := { factor := fun i y ↦ if i ∈ fixed then (r i : ℝ)⁻¹ else fac.mechanism.factor i y factor_pos := by intro i y split_ifs with hi · exact inv_pos.mpr (Nat.cast_pos.mpr (fac.cardinalitiesPositive i)) · exact fac.mechanism.factor_pos i y factor_normalized := by intro i y by_cases hi : i ∈ fixed · simp only [hi, if_pos] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] exact mul_inv_cancel₀ (Nat.cast_ne_zero.mpr (Nat.ne_of_gt (fac.cardinalitiesPositive i))) · simp only [hi] exact fac.mechanism.factor_normalized i y factor_local := by intro i y y' hyy' by_cases hi : i ∈ fixed · simp [hi] · simp only [hi] exact fac.mechanism.factor_local i hyy' } let c : ℝ := ∏ i ∈ fixed, (r i : ℝ)⁻¹ have hcpos : 0 < c := by exact Finset.prod_pos fun i hi ↦ inv_pos.mpr (Nat.cast_pos.mpr (fac.cardinalitiesPositive i)) have hjoint (y : ProfileSpace r) : M.jointMass y = c * fac.remainingFactorKernel fixed y := by unfold PositiveFiniteDAGMechanism.jointMass remainingFactorKernel c M rw [Finset.prod_ite] congr 1 · congr 1 ext i simp · congr 1 ext i simp have hagree_iff_projection (S : Finset V) (a y : ProfileSpace r) : AgreeOn S y a ↔ coordinateProjection (X := fun i ↦ Fin (r i)) S y = coordinateProjection (X := fun i ↦ Fin (r i)) S a := by constructor · intro h funext w exact h w w.property · intro h w hw exact congrFun h ⟨w, hw⟩ have hmarginal (S : Finset V) (a : ProfileSpace r) : M.marginalMass S a = c * kernelMarginalMass (fac.remainingFactorKernel fixed) S a := by unfold PositiveFiniteDAGMechanism.marginalMass kernelMarginalMass fiberSum rw [Finset.mul_sum] apply Finset.sum_congr rfl intro y hy rw [hjoint] by_cases hya : AgreeOn S y a · have hp := (hagree_iff_projection S a y).mp hya simp [hya, hp] · have hp : coordinateProjection (X := fun i ↦ Fin (r i)) S y ≠ coordinateProjection (X := fun i ↦ Fin (r i)) S a := fun hp ↦ hya ((hagree_iff_projection S a y).mpr hp) simp [hya, hp] have hcond := M.conditionalMass_given_parents v x z unfold PositiveFiniteDAGMechanism.conditionalMass at hcond rw [hmarginal, hmarginal] at hcond rw [mul_div_mul_left _ _ hcpos.ne'] at hcond unfold kernelConditionalMass simpa [M, hv] using hcond -
fixKernelCoordinate_remainingFactorKerneltheorem — A factorized table, fixed vertex set, and proof that the vertex is not fixed already give the parent-conditioned fixing identity that removes its local factor.hypothesesconclusionfixKernelCoordinate (fac.remainingFactorKernel fixed) v (G.parents v)= fac.remainingFactorKernel (insert v fixed)Proof (Lean source)
theorem fixKernelCoordinate_remainingFactorKernel (fac : PositiveDAGTableFactorization G p) (fixed : Finset V) {v : V} (hv : v ∉ fixed) : fixKernelCoordinate (fac.remainingFactorKernel fixed) v (G.parents v) = fac.remainingFactorKernel (insert v fixed) := by /- Extensionality, `fixKernelCoordinate_apply`, and `remainingFactorKernel_conditionalMass_eq_factor` reduce the claim to cancelling the positive factor at `v` from the finite product. Use `Finset.prod_erase` (or the corresponding insert/sdiff product lemma) and `factor_pos.ne'`. -/ funext x rw [fixKernelCoordinate_apply, fac.remainingFactorKernel_conditionalMass_eq_factor fixed hv x (x v)] simp only [Function.update_eq_self] unfold remainingFactorKernel have hvRemaining : v ∈ univ \ fixed := Finset.mem_sdiff.mpr ⟨Finset.mem_univ v, hv⟩ have hsets : univ \ insert v fixed = (univ \ fixed).erase v := by ext w simp rw [hsets, ← Finset.mul_prod_erase (univ \ fixed) (fun w ↦ fac.mechanism.factor w x) hvRemaining] exact mul_div_cancel_left₀ _ (fac.mechanism.factor_pos v x).ne'
Fixing 1 core · 2 supporting This module proves the graph-independent fixing expansion requested by downstream consumers: for any list of distinct vertices, sequential FinitePositiveTable fixing conditional on the original DAG parent sets equals the ★ fixSequence_eq_remainingFactorKernel
Sequential fixing removes local DAG factors
This module proves the graph-independent fixing expansion requested by downstream consumers:
for any list of distinct vertices, sequential FinitePositiveTable fixing conditional on the
original DAG parent sets equals the product of precisely the local factors whose vertices have
not been fixed. Hence the result is a normalized kernel over the remaining coordinates with
the fixed coordinates acting as arguments.
theorem fixSequence_eq_remainingFactorKernel reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
A factorized table, vertex list, and proof that its vertices are distinct give the sequential-fixing expansion as the truncated local-factor product: fixing the listed vertices one after another, each time dividing the current kernel by its conditional mass of the vertex given the vertex's DAG parents, yields at every complete profile the product of the local factors of the vertices not in the list.
Formal statement
hypotheses
conclusion
fixSequence p (parentFixingSteps G vertices) = fac.remainingFactorKernel vertices.toFinset
Proof (Lean source)
theorem fixSequence_eq_remainingFactorKernel
(fac : PositiveDAGTableFactorization G p) (vertices : List V)
(hvertices : vertices.Nodup) :
fixSequence p (parentFixingSteps G vertices) =
fac.remainingFactorKernel vertices.toFinset := by
/-
Induct on `vertices`. At the empty list, use `fac.mass_eq_jointMass` and identify the
`univ \ ∅` product with `jointMass`. At `v :: vs`, rewrite the first kernel by the
induction invariant for the already fixed set and apply
`fixKernelCoordinate_remainingFactorKernel`; `Nodup` supplies `v ∉ vs.toFinset`.
The recursion direction of `fixKernelSequence` may make it cleaner to strengthen the
induction statement to start from an arbitrary already-fixed set.
-/
have hstart : p.mass = fac.remainingFactorKernel ∅ := by
funext x
rw [fac.mass_eq_jointMass]
unfold Causalean.Graph.FiniteDensity.PositiveFiniteDAGMechanism.jointMass
remainingFactorKernel
simp
have haux : ∀ (done : Finset V) (vs : List V),
vs.Nodup → Disjoint done vs.toFinset →
fixKernelSequence (fac.remainingFactorKernel done) (parentFixingSteps G vs) =
fac.remainingFactorKernel (done ∪ vs.toFinset) := by
intro done vs hnodup hdisj
induction vs generalizing done with
| nil =>
simp [parentFixingSteps, fixKernelSequence]
| cons v vs ih =>
simp only [List.nodup_cons] at hnodup
simp only [List.toFinset_cons, Finset.disjoint_insert_right] at hdisj
rw [show parentFixingSteps G (v :: vs) =
{ coordinate := v, conditioning := G.parents v } :: parentFixingSteps G vs by rfl]
rw [fixKernelSequence]
rw [fac.fixKernelCoordinate_remainingFactorKernel done hdisj.1]
rw [ih (insert v done) hnodup.2]
· congr 1
ext w
simp
· rw [Finset.disjoint_insert_left]
exact ⟨by simpa using hnodup.1, hdisj.2⟩
unfold fixSequence
rw [hstart]
simpa using haux ∅ vertices hvertices (by simp)
2 supporting declarations (lemmas, instances)
-
fixSequence_row_normalizedtheorem — A factorized table, distinct vertex list, and profile give unit mass for the sequentially fixed kernel in that fixed-coordinate row.Proof (Lean source)
theorem fixSequence_row_normalized (fac : PositiveDAGTableFactorization G p) (vertices : List V) (hvertices : vertices.Nodup) (x : ProfileSpace r) : kernelMarginalMass (fixSequence p (parentFixingSteps G vertices)) vertices.toFinset x = 1 := by rw [fixSequence_eq_remainingFactorKernel fac vertices hvertices] exact fac.remainingFactorKernel_row_normalized vertices.toFinset x -
fixSequence_strictlyPositivetheorem — A factorized table, vertex list, and proof that its vertices are distinct give a pointwise strictly positive sequentially fixed kernel.Proof (Lean source)
theorem fixSequence_strictlyPositive (fac : PositiveDAGTableFactorization G p) (vertices : List V) (hvertices : vertices.Nodup) : (fixSequence p (parentFixingSteps G vertices)).IsStrictlyPositive := by rw [fixSequence_eq_remainingFactorKernel fac vertices hvertices] exact fac.remainingFactorKernel_pos vertices.toFinset
GlobalMarkov 1 core · 2 supporting This module exposes the headline API. ★ fixSequence_globalMarkov
Global Markov theorems for sequentially fixed finite DAG tables
This module exposes the headline API. Sequential graph-independent fixing of distinct DAG vertices is first identified with the truncated local-factor product; d-separation in the DAG with incoming arrows to those fixed vertices removed then yields multiplicative finite-kernel conditional independence. Both a set-valued core and singleton consumer forms are provided.
theorem fixSequence_globalMarkov reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
A factorized table, distinct fixed-vertex list, three remaining coordinate sets, proofs that each is remaining, and d-separation of the first two sets given the third set together with all fixed vertices, in the DAG with incoming arrows to fixed vertices removed, give the atomwise multiplicative conditional-independence identity for the kernel obtained by sequentially fixing the listed vertices given their DAG parents.
Formal statement
Proof (Lean source)
theorem fixSequence_globalMarkov
(fac : PositiveDAGTableFactorization G p) (vertices : List V)
(hvertices : vertices.Nodup) (X Y Z : Finset V)
(hX : X ⊆ univ \ vertices.toFinset)
(hY : Y ⊆ univ \ vertices.toFinset)
(hZ : Z ⊆ univ \ vertices.toFinset)
(hdSep : (arrowheadRemovedDAG G vertices.toFinset).dSep
X Y (Z ∪ vertices.toFinset)) :
FixedKernelCondIndep
(fixSequence p (parentFixingSteps G vertices)) vertices.toFinset X Y Z := by
rw [fixSequence_eq_remainingFactorKernel fac vertices hvertices]
exact fac.remainingFactorKernel_globalMarkov vertices.toFinset X Y Z
hX hY hZ hdSep
2 supporting declarations (lemmas, instances)
-
fixSequence_singleton_globalMarkovtheorem — A factorized table, distinct fixed-vertex list, two vertices and a random conditioning set, proofs that both vertices remain, proof that the conditioning set remains random, and the corresponding d-separation give singleton multiplicative conditional independence after sequential fixing.hypothesesfac :vertices :List Vhvertices :vertices.Nodupa b :VZ :Finset Vha :a ∉ vertices.toFinsethb :b ∉ vertices.toFinsethZ :Z ⊆ univ \ vertices.toFinsethdSep :(arrowheadRemovedDAG G vertices.toFinset).dSep {a} {b} (Z ∪ vertices.toFinset)conclusionProof (Lean source)
theorem fixSequence_singleton_globalMarkov (fac : PositiveDAGTableFactorization G p) (vertices : List V) (hvertices : vertices.Nodup) (a b : V) (Z : Finset V) (ha : a ∉ vertices.toFinset) (hb : b ∉ vertices.toFinset) (hZ : Z ⊆ univ \ vertices.toFinset) (hdSep : (arrowheadRemovedDAG G vertices.toFinset).dSep {a} {b} (Z ∪ vertices.toFinset)) : FixedKernelCondIndep (fixSequence p (parentFixingSteps G vertices)) vertices.toFinset {a} {b} Z := by exact fac.fixSequence_globalMarkov vertices hvertices {a} {b} Z (by intro v hv rw [Finset.mem_singleton] at hv subst v simp [ha]) (by intro v hv rw [Finset.mem_singleton] at hv subst v simp [hb]) hZ hdSep -
fixSequence_kernelCondIndeptheorem — A factorized table, distinct fixed-vertex list, two distinct remaining vertices, and d-separation by all other random and fixed vertices give the existing singleton kernel cross-product identity after sequential fixing.hypothesesfac :vertices :List Vhvertices :vertices.Nodupa b :Vha :a ∉ vertices.toFinsethb :b ∉ vertices.toFinsethab :a ≠ bhdSep :(arrowheadRemovedDAG G vertices.toFinset).dSep {a} {b} ((((univ \ vertices.toFinset).erase a).erase b) ∪ vertices.toFinset)conclusionProof (Lean source)
theorem fixSequence_kernelCondIndep (fac : PositiveDAGTableFactorization G p) (vertices : List V) (hvertices : vertices.Nodup) (a b : V) (ha : a ∉ vertices.toFinset) (hb : b ∉ vertices.toFinset) (hab : a ≠ b) (hdSep : (arrowheadRemovedDAG G vertices.toFinset).dSep {a} {b} ((((univ \ vertices.toFinset).erase a).erase b) ∪ vertices.toFinset)) : KernelCondIndep (fixSequence p (parentFixingSteps G vertices)) a b := by apply (fixedKernelCondIndep_complement_iff_kernelCondIndep (fixSequence p (parentFixingSteps G vertices)) vertices.toFinset a b ha hb hab).mp exact fac.fixSequence_singleton_globalMarkov vertices hvertices a b (((univ \ vertices.toFinset).erase a).erase b) ha hb (by intro v hv; simp only [Finset.mem_erase] at hv ⊢; exact hv.2.2) hdSep
KernelMarkov 1 core · 3 supporting This module interprets the DAG ordered-local closure for truncated products and combines that interpretation with d-separation after arrowhead removal. ★ remainingFactorKernel_globalMarkov
Multiplicative conditional independence and DAG global Markov kernels
This module interprets the DAG ordered-local closure for truncated products and combines that
interpretation with d-separation after arrowhead removal. The graph-independent finite-kernel
conditional-independence definitions and bridges live in KernelCI.
theorem remainingFactorKernel_globalMarkov reviewed
⚑ flagged
Causalean.Stat.FinitePositiveTable.DAG.PositiveDAGTableFactorization
Take a strictly positive finite table that factorizes into normalized parent-local factors along a DAG, and a set of fixed vertices with three further vertex sets, two random sets and a conditioning set, each consisting of unfixed vertices. If the two random sets are d-separated given the conditioning set together with the fixed vertices, in the DAG obtained by deleting every arrow pointing into a fixed vertex, then the truncated product of the unfixed local factors satisfies the multiplicative conditional-independence identity at every profile: with the fixed coordinates held at the profile's values, its marginal over both random sets and the conditioning set, times its marginal over the conditioning set, equals the product of its marginals over each random set joined with the conditioning set.
Formal statement
hypotheses
fac :
fixed X Y Z :
Finset V
hX :
X ⊆ univ \ fixed
hY :
Y ⊆ univ \ fixed
hZ :
Z ⊆ univ \ fixed
hdSep :
(arrowheadRemovedDAG G fixed).dSep X Y (Z ∪ fixed)
conclusion
FixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed X Y Z
Proof (Lean source)
theorem remainingFactorKernel_globalMarkov
(fac : PositiveDAGTableFactorization G p) (fixed X Y Z : Finset V)
(hX : X ⊆ univ \ fixed) (hY : Y ⊆ univ \ fixed)
(hZ : Z ⊆ univ \ fixed)
(hdSep : (arrowheadRemovedDAG G fixed).dSep X Y (Z ∪ fixed)) :
FixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed X Y Z := by
apply fac.remainingFactorKernel_orderedLocalMarkov fixed X Y Z
apply (arrowheadRemovedDAG G fixed).orderedLocalSG_of_dSep_with_fixed
(univ \ fixed) X Y Z fixed
· intro f hf
exact arrowheadRemovedDAG_fixed_parents_empty G fixed hf
· exact fixed_disjoint_remaining fixed
· exact hX
· exact hY
· exact hZ
· exact hdSep
3 supporting declarations (lemmas, instances)
-
remainingFactorKernel_orderedLocalBasistheorem — A factorized table, fixed vertex set, remaining vertex, candidate nondescendant set, proof that it remains random, and proof that it contains only nondescendants give the ordered-local fixed-row conditional-independence basis statement.hypothesesfac :fixed :Finset Vv :Vhv :v ∈ univ \ fixedP :Finset VhP :P ⊆ univ \ fixedhND :P ⊆ (arrowheadRemovedDAG G fixed).nonDescendants vconclusionFixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed {v} (P \ ((arrowheadRemovedDAG G fixed).parents v ∩ (univ \ fixed))) ((arrowheadRemovedDAG G fixed).parents v ∩ (univ \ fixed))Proof (Lean source)
theorem remainingFactorKernel_orderedLocalBasis (fac : PositiveDAGTableFactorization G p) (fixed : Finset V) {v : V} (hv : v ∈ univ \ fixed) (P : Finset V) (hP : P ⊆ univ \ fixed) (hND : P ⊆ (arrowheadRemovedDAG G fixed).nonDescendants v) : FixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed {v} (P \ ((arrowheadRemovedDAG G fixed).parents v ∩ (univ \ fixed))) ((arrowheadRemovedDAG G fixed).parents v ∩ (univ \ fixed)) := by classical let (i : V) : Nonempty (Fin (r i)) := ⟨⟨0, fac.cardinalitiesPositive i⟩⟩ let H := arrowheadRemovedDAG G fixed let M : PositiveFiniteDAGMechanism H (fun i ↦ Fin (r i)) := { factor := fun i y ↦ if i ∈ fixed then (r i : ℝ)⁻¹ else fac.mechanism.factor i y factor_pos := by intro i y split_ifs with hi · exact inv_pos.mpr (Nat.cast_pos.mpr (fac.cardinalitiesPositive i)) · exact fac.mechanism.factor_pos i y factor_normalized := by intro i y by_cases hi : i ∈ fixed · simp only [hi, if_pos] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] exact mul_inv_cancel₀ (Nat.cast_ne_zero.mpr (Nat.ne_of_gt (fac.cardinalitiesPositive i))) · simp only [hi] exact fac.mechanism.factor_normalized i y factor_local := by intro i y y' hyy' by_cases hi : i ∈ fixed · simp [hi] · simp only [hi] apply fac.mechanism.factor_local i rw [← arrowheadRemovedDAG_random_parents G fixed hi] exact hyy' } let c : ℝ := ∏ i ∈ fixed, (r i : ℝ)⁻¹ have hcpos : 0 < c := by exact Finset.prod_pos fun i _ ↦ inv_pos.mpr (Nat.cast_pos.mpr (fac.cardinalitiesPositive i)) have hjoint (y : ProfileSpace r) : M.jointMass y = c * fac.remainingFactorKernel fixed y := by unfold PositiveFiniteDAGMechanism.jointMass remainingFactorKernel c M rw [Finset.prod_ite] congr 1 · congr 1 ext i simp · congr 1 ext i simp have hmarginal (S : Finset V) (a : ProfileSpace r) : M.marginalMass S a = c * kernelMarginalMass (fac.remainingFactorKernel fixed) S a := by unfold PositiveFiniteDAGMechanism.marginalMass kernelMarginalMass fiberSum rw [Finset.mul_sum] apply Finset.sum_congr rfl intro y hy rw [hjoint] by_cases hya : AgreeOn S y a · have hp : coordinateProjection (X := fun i ↦ Fin (r i)) S y = coordinateProjection (X := fun i ↦ Fin (r i)) S a := by funext w exact hya w w.property simp [hya, hp] · have hp : coordinateProjection (X := fun i ↦ Fin (r i)) S y ≠ coordinateProjection (X := fun i ↦ Fin (r i)) S a := by intro hp apply hya intro w hw exact congrFun hp ⟨w, hw⟩ simp [hya, hp] have hci := mechanism_orderedLocalBasis_condIndep H M fixed (univ \ fixed) rfl (fun f hf ↦ arrowheadRemovedDAG_fixed_parents_empty G fixed hf) hv P hP hND exact fixedKernelCondIndep_of_mechanism H M fac.cardinalitiesPositive (fac.remainingFactorKernel fixed) c hcpos hmarginal fixed {v} (P \ (H.parents v ∩ (univ \ fixed))) (H.parents v ∩ (univ \ fixed)) (by simpa only [H, Finset.union_assoc, Finset.union_left_comm, union_comm] using hci) -
remainingFactorKernel_orderedLocalMarkovtheorem — A factorized table, fixed and three coordinate sets, and an ordered-local semi-graphoid derivation in the arrowhead-removed DAG give the corresponding multiplicative fixed-row conditional independence.hypothesesconclusionFixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed X Y ZProof (Lean source)
theorem remainingFactorKernel_orderedLocalMarkov (fac : PositiveDAGTableFactorization G p) (fixed X Y Z : Finset V) (hsg : (arrowheadRemovedDAG G fixed).OrderedLocalSG (univ \ fixed) X Y Z) : FixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed X Y Z := by classical let (i : V) : Nonempty (Fin (r i)) := ⟨⟨0, fac.cardinalitiesPositive i⟩⟩ letI : ∀ i, MeasurableSpace (Fin (r i)) := fun _ ↦ ⊤ let H := arrowheadRemovedDAG G fixed let R := univ \ fixed let M : PositiveFiniteDAGMechanism H (fun i ↦ Fin (r i)) := { factor := fun i y ↦ if i ∈ fixed then (r i : ℝ)⁻¹ else fac.mechanism.factor i y factor_pos := by intro i y split_ifs with hi · exact inv_pos.mpr (Nat.cast_pos.mpr (fac.cardinalitiesPositive i)) · exact fac.mechanism.factor_pos i y factor_normalized := by intro i y by_cases hi : i ∈ fixed · simp only [hi, if_pos] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] exact mul_inv_cancel₀ (Nat.cast_ne_zero.mpr (Nat.ne_of_gt (fac.cardinalitiesPositive i))) · simp only [hi] exact fac.mechanism.factor_normalized i y factor_local := by intro i y y' hyy' by_cases hi : i ∈ fixed · simp [hi] · simp only [hi] apply fac.mechanism.factor_local i rw [← arrowheadRemovedDAG_random_parents G fixed hi] exact hyy' } let c : ℝ := ∏ i ∈ fixed, (r i : ℝ)⁻¹ have hcpos : 0 < c := by exact Finset.prod_pos fun i _ ↦ inv_pos.mpr (Nat.cast_pos.mpr (fac.cardinalitiesPositive i)) have hjoint (y : ProfileSpace r) : M.jointMass y = c * fac.remainingFactorKernel fixed y := by unfold PositiveFiniteDAGMechanism.jointMass remainingFactorKernel c M rw [Finset.prod_ite] congr 1 · congr 1 ext i simp · congr 1 ext i simp have hmarginal (S : Finset V) (a : ProfileSpace r) : M.marginalMass S a = c * kernelMarginalMass (fac.remainingFactorKernel fixed) S a := by unfold PositiveFiniteDAGMechanism.marginalMass kernelMarginalMass fiberSum rw [Finset.mul_sum] apply Finset.sum_congr rfl intro y hy rw [hjoint] by_cases hya : AgreeOn S y a · have hp : coordinateProjection (X := fun i ↦ Fin (r i)) S y = coordinateProjection (X := fun i ↦ Fin (r i)) S a := by funext w exact hya w w.property simp [hya, hp] · have hp : coordinateProjection (X := fun i ↦ Fin (r i)) S y ≠ coordinateProjection (X := fun i ↦ Fin (r i)) S a := by intro hp apply hya intro w hw exact congrFun hp ⟨w, hw⟩ simp [hya, hp] have hmeasure : ∀ {X Y Z : Finset V}, H.OrderedLocalSG R X Y Z → CondIndepFun (comap (coordinateProjection (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) inferInstance) (coordinateConditioning_comap_le (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) (coordinateProjection (X := fun i ↦ Fin (r i)) X) (coordinateProjection (X := fun i ↦ Fin (r i)) Y) M.toCountingFactorization.observationalMeasure := by intro X' Y' Z' h induction h with | nil Y Z hY hZ => let emptyValue : ∀ j : (∅ : Finset V), Fin (r j) := fun j ↦ False.elim ((Finset.notMem_empty j.val : j.val ∉ (∅ : Finset V)) j.property) have hempty : coordinateProjection (X := fun i ↦ Fin (r i)) ∅ = fun _ ↦ emptyValue := by funext x j exact False.elim ((Finset.notMem_empty j.val : j.val ∉ (∅ : Finset V)) j.property) rw [hempty] exact condIndepFun_const_left emptyValue _ | basis v hv P hP hND hPa => exact mechanism_orderedLocalBasis_condIndep H M fixed R rfl (fun f hf ↦ arrowheadRemovedDAG_fixed_parents_empty G fixed hf) hv P hP hND | symm h ih => exact ih.symm | @decomp X Y W Z h ih => let restrictY : (∀ j : ↑(Y ∪ W), Fin (r j)) → (∀ j : Y, Fin (r j)) := fun z j ↦ z ⟨j, Finset.mem_union_left W j.property⟩ have hrestrictY : Measurable restrictY := measurable_of_finite _ have hcomp := ih.comp measurable_id hrestrictY have heq : restrictY ∘ coordinateProjection (X := fun i ↦ Fin (r i)) (Y ∪ W) = coordinateProjection (X := fun i ↦ Fin (r i)) Y := by funext x j rfl simpa only [Function.id_comp, heq] using hcomp | @weakUnion X Y W Z h ih => let split : (∀ j : ↑(Y ∪ W), Fin (r j)) → ((∀ j : Y, Fin (r j)) × (∀ j : W, Fin (r j))) := fun z ↦ (fun j ↦ z ⟨j, Finset.mem_union_left W j.property⟩, fun j ↦ z ⟨j, mem_union_right Y j.property⟩) have hsplit : Measurable split := measurable_of_finite _ have hp := ih.comp measurable_id hsplit have hsplit_eq : split ∘ coordinateProjection (X := fun i ↦ Fin (r i)) (Y ∪ W) = fun x ↦ (coordinateProjection (X := fun i ↦ Fin (r i)) Y x, coordinateProjection (X := fun i ↦ Fin (r i)) W x) := by funext x rfl rw [hsplit_eq] at hp have hw := condIndepFun_weak_union_of_prodMk (coordinateConditioning_comap_le (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) (measurable_coordinateProjection X) (measurable_coordinateProjection Y) (measurable_coordinateProjection W) hp have hσ : comap (coordinateProjection (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) inferInstance ⊔ comap (coordinateProjection (X := fun i ↦ Fin (r i)) W) inferInstance = comap (coordinateProjection (X := fun i ↦ Fin (r i)) (fixed ∪ (Z ∪ W))) inferInstance := by rw [← Finset.union_assoc] exact (comap_coordinateProjection_union_eq_sup (X := fun i ↦ Fin (r i)) (fixed ∪ Z) W).symm simpa only [hσ] using hw | @contract X Y W Z h1 h2 ih1 ih2 => have hσ : comap (coordinateProjection (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) inferInstance ⊔ comap (coordinateProjection (X := fun i ↦ Fin (r i)) W) inferInstance = comap (coordinateProjection (X := fun i ↦ Fin (r i)) (fixed ∪ (Z ∪ W))) inferInstance := by rw [← Finset.union_assoc] exact (comap_coordinateProjection_union_eq_sup (X := fun i ↦ Fin (r i)) (fixed ∪ Z) W).symm have ih1' : CondIndepFun (comap (coordinateProjection (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) inferInstance ⊔ comap (coordinateProjection (X := fun i ↦ Fin (r i)) W) inferInstance) (sup_le (coordinateConditioning_comap_le (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) (measurable_coordinateProjection W).comap_le) (coordinateProjection (X := fun i ↦ Fin (r i)) X) (coordinateProjection (X := fun i ↦ Fin (r i)) Y) M.toCountingFactorization.observationalMeasure := by simpa only [hσ] using ih1 have hp := condIndepFun_contraction_of_prodMk (coordinateConditioning_comap_le (X := fun i ↦ Fin (r i)) (fixed ∪ Z)) (measurable_coordinateProjection X) (measurable_coordinateProjection Y) (measurable_coordinateProjection W) ih1' ih2 let merge : ((∀ j : Y, Fin (r j)) × (∀ j : W, Fin (r j))) → (∀ j : ↑(Y ∪ W), Fin (r j)) := fun z j ↦ if hj : j.val ∈ Y then z.1 ⟨j, hj⟩ else z.2 ⟨j, (Finset.mem_union.mp j.property).resolve_left hj⟩ have hmerge : Measurable merge := measurable_of_finite _ have hcomp := hp.comp measurable_id hmerge have hmerge_eq : merge ∘ (fun x ↦ (coordinateProjection (X := fun i ↦ Fin (r i)) Y x, coordinateProjection (X := fun i ↦ Fin (r i)) W x)) = coordinateProjection (X := fun i ↦ Fin (r i)) (Y ∪ W) := by funext x j by_cases hj : j.val ∈ Y <;> simp [merge, hj, coordinateProjection] simpa only [Function.id_comp, hmerge_eq] using hcomp have hci := hmeasure hsg exact fixedKernelCondIndep_of_mechanism H M fac.cardinalitiesPositive (fac.remainingFactorKernel fixed) c hcpos hmarginal fixed X Y Z hci -
remainingFactorKernel_singleton_globalMarkovtheorem — A factorized table, fixed vertex set and two vertices, random conditioning set, proofs that both vertices remain, proof that the conditioning set remains random, and the d-separation premise give singleton multiplicative fixed-row conditional independence.hypothesesfac :fixed :Finset Va b :VZ :Finset Vha :a ∉ fixedhb :b ∉ fixedhZ :Z ⊆ univ \ fixedhdSep :(arrowheadRemovedDAG G fixed).dSep {a} {b} (Z ∪ fixed)conclusionFixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed {a} {b} ZProof (Lean source)
theorem remainingFactorKernel_singleton_globalMarkov (fac : PositiveDAGTableFactorization G p) (fixed : Finset V) (a b : V) (Z : Finset V) (ha : a ∉ fixed) (hb : b ∉ fixed) (hZ : Z ⊆ univ \ fixed) (hdSep : (arrowheadRemovedDAG G fixed).dSep {a} {b} (Z ∪ fixed)) : FixedKernelCondIndep (fac.remainingFactorKernel fixed) fixed {a} {b} Z := by exact fac.remainingFactorKernel_globalMarkov fixed {a} {b} Z (by simpa) (by simpa) hZ hdSep