Causal Bayesian networks

DefinitionParent values of a node#✓fully proved

The values of the parents of node k in a full assignment x.

def paVal (k : Fin n) (x : Fin n → α) : b.pa k → α :=
  fun j => x (Fin.castLE k.2.le j)

Uses 1 · Used by 17

Statement usesBayesian network

Used byProduct of the tables of an ancestral set · The ancestral product on all nodes is the joint · Global Markov property for finite sets of nodes · The law of an ancestral set depends only on its tables · The back-door adjustment · The front-door adjustment · Joint law as interventional law times the node's table · The truncated factorization · Assignments contradicting an intervention have probability zero · The truncated factorization for a set of nodes · The intervention do(X_k = a) does not change the law of the non-descendants of k · A node's table is its conditional law given its parents · A node's table is its conditional law given a predecessor set · Adjustment for the direct causes · Adjustment for the direct causes under table positivity · Back-door adjustment for a set of predecessors containing the parents · Intervention preserves the law of the parents

DefinitionThe intervention do(X_k = a)#✓fully proved

The mechanism of node k is replaced by the point mass at a, and all incoming arrows to k are deleted (its parent set becomes ∅); every other node keeps its parents and its table. (The new table of k is the point mass on the empty parent set; the tables of the other nodes are transported along the equality of their parent sets.)

noncomputable def intervene (k : Fin n) (a : α) : BayesNet α n where
  pa j := if j = k then ∅ else b.pa j
  cpt j z := if h : j = k then StdSimplex.single a
    else b.cpt j fun i => z ⟨i.1, by rw [if_neg h]; exact i.2⟩

Uses 1 · Used by 15

Statement usesBayesian network

Used byThe back-door adjustment · The front-door adjustment · Intervention leaves the parents of other nodes unchanged · Intervention deletes the parents of the intervened node · Joint law as interventional law times the node's table · The truncated factorization · Assignments contradicting an intervention have probability zero · The intervention do(X_k = a) does not change the law of the non-descendants of k · A node's table is its conditional law given its parents · A node's table is its conditional law given a predecessor set · Adjustment for the direct causes · Adjustment for the direct causes under table positivity · Back-door adjustment for a set of predecessors containing the parents · Back-door adjustment for a set of predecessors · Intervention preserves the law of the parents

TheoremIntervention deletes the parents of the intervened node#✓fully proved

The parents of the intervened node are deleted.

theorem intervene_pa_self (k : Fin n) (a : α) : (b.intervene k a).pa k = ∅

Uses 2 · Used by 1

Statement usesBayesian network · The intervention do(X_k = a)

Used byThe intervention do(X_k = a) does not change the law of the non-descendants of k

TheoremIntervention leaves the parents of other nodes unchanged#✓fully proved

The parents of every other node are unchanged by the intervention.

theorem intervene_pa_of_ne {j k : Fin n} (hj : j ≠ k) (a : α) :
    (b.intervene k a).pa j = b.pa j

Uses 2 · Used by 1

Statement usesBayesian network · The intervention do(X_k = a)

Used byThe intervention do(X_k = a) does not change the law of the non-descendants of k

TheoremThe truncated factorization#✓fully proved

The truncated factorization (Pearl 2009, eq. (3.10)): after do(X_k = a) the joint is the product of the tables of all nodes other than k on assignments with x_k = a, and 0 elsewhere.

theorem joint_intervene [DecidableEq α] (k : Fin n) (a : α) (x : Fin n → α) :
    (b.intervene k a).joint x =
      if x k = a then ∏ j ∈ univ.erase k, (b.cpt j (b.paVal j x)).weights (x j) else 0

Uses 5 · Used by 8

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network · Parent values of a node

Proof usesFactorization of a Bayesian network

Used byThe back-door adjustment · The front-door adjustment · Joint law as interventional law times the node's table · Assignments contradicting an intervention have probability zero · A node's table is its conditional law given its parents · A node's table is its conditional law given a predecessor set · Adjustment for the direct causes · Back-door adjustment for a set of predecessors containing the parents

TheoremIntervention preserves the law of the parents#✓fully proved

The intervention do(X_k = a) does not change the law of the parents of node k.

theorem sum_paVal_intervene [Fintype α] [DecidableEq α] (k : Fin n) (a : α)
    (z : b.pa k → α) :
    ∑ x with b.paVal k x = z, (b.intervene k a).joint x = ∑ x with b.paVal k x = z, b.joint x

Uses 9 · Used by 2

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network · Parent values of a node

Proof usesThe chain of a Bayesian network · Chain of conditional distributions · Joint distribution of a chain · Joint distribution determined by the first conditionals · Splitting a sum over \(\alpha^{n+1}\) at the last coordinate

Used byA node's table is its conditional law given its parents · Adjustment for the direct causes

TheoremAdjustment for the direct causes#✓fully proved

Adjustment for the direct causes (Pearl 2009, Theorem 3.2.2; the case Z = pa(X) of the back-door adjustment): for every function f of the variables, E[f | do(X_k = a)] = ∑_z P(pa_k = z) E[f | X_k = a, pa_k = z], assuming P(X_k = a, pa_k = z) > 0 whenever P(pa_k = z) > 0.

theorem sum_intervene_joint_mul [Fintype α] [DecidableEq α] (k : Fin n) (a : α)
    (f : (Fin n → α) → ℝ)
    (hpos : ∀ z : b.pa k → α, ∑ x with b.paVal k x = z, b.joint x ≠ 0 →
      ∑ x with x k = a ∧ b.paVal k x = z, b.joint x ≠ 0) :
    ∑ x, (b.intervene k a).joint x * f x =
      ∑ z : b.pa k → α, (∑ x with b.paVal k x = z, b.joint x) *
        ((∑ x with x k = a ∧ b.paVal k x = z, b.joint x * f x) /
          ∑ x with x k = a ∧ b.paVal k x = z, b.joint x)

Uses 10 · Used by 1

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network · Parent values of a node

Proof usesFactorization of a Bayesian network · The truncated factorization · Intervention preserves the law of the parents · The chain of a Bayesian network · Chain of conditional distributions · Joint distribution of a chain

Used byAdjustment for the direct causes under table positivity

TheoremA node's table is its conditional law given its parents#✓fully proved

The table of node k is the conditional law of X_k given its parents: P(X_k = a, pa_k = z) = p_k (a | z) P(pa_k = z).

theorem sum_filter_joint_eq_cpt_mul [Fintype α] [DecidableEq α] (k : Fin n) (a : α)
    (z : b.pa k → α) :
    ∑ x with x k = a ∧ b.paVal k x = z, b.joint x =
      (b.cpt k z).weights a * ∑ x with b.paVal k x = z, b.joint x

Uses 7 · Used by 1

Statement usesBayesian network · Joint distribution of a Bayesian network · Parent values of a node

Proof usesThe intervention do(X_k = a) · Factorization of a Bayesian network · The truncated factorization · Intervention preserves the law of the parents

Used byAdjustment for the direct causes under table positivity

TheoremAdjustment for the direct causes under table positivity#✓fully proved

Adjustment for the direct causes when the table of node k gives the value a positive probability at every value of the parents.

theorem sum_intervene_joint_mul_of_cpt_ne_zero [Fintype α] [DecidableEq α] (k : Fin n) (a : α)
    (f : (Fin n → α) → ℝ) (hpos : ∀ z, (b.cpt k z).weights a ≠ 0) :
    ∑ x, (b.intervene k a).joint x * f x =
      ∑ z : b.pa k → α, (∑ x with b.paVal k x = z, b.joint x) *
        ((∑ x with x k = a ∧ b.paVal k x = z, b.joint x * f x) /
          ∑ x with x k = a ∧ b.paVal k x = z, b.joint x)

Uses 6

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network · Parent values of a node

Proof usesA node's table is its conditional law given its parents · Adjustment for the direct causes

TheoremBack-door adjustment for a set of predecessors containing the parents#✓fully proved

Let Z be a set of nodes preceding k in the topological order (so Z contains no descendant of k) that contains the parents of k. Then Z meets the back-door criterion for every outcome node y ∉ Z (a path from k to y that starts with an arrow into k starts k ← p with p ∈ pa(k) ⊆ Z, an interior non-collider, so it is blocked), and for every function f of the variables E[f | do(X_k = a)] = ∑_z P(Z = z) E[f | X_k = a, Z = z], assuming P(X_k = a, Z = z) > 0 whenever P(Z = z) > 0 (Pearl 2009, Theorem 3.3.2, in this case).

theorem sum_intervene_joint_mul_of_pred [Fintype α] [DecidableEq α] (k : Fin n) (a : α)
    (Z : Finset (Fin n)) (hZk : ∀ i ∈ Z, i < k)
    (hpaZ : ∀ j ∈ b.pa k, Fin.castLE k.2.le j ∈ Z) (f : (Fin n → α) → ℝ)
    (hpos : ∀ z : Z → α, ∑ x with (fun i : Z => x i) = z, b.joint x ≠ 0 →
      ∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x ≠ 0) :
    ∑ x, (b.intervene k a).joint x * f x =
      ∑ z : Z → α, (∑ x with (fun i : Z => x i) = z, b.joint x) *
        ((∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x * f x) /
          ∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x)

Uses 11 · Used by 1

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network

Proof usesFactorization of a Bayesian network · The truncated factorization · Parent values of a node · The chain of a Bayesian network · Chain of conditional distributions · Joint distribution of a chain · Joint distribution determined by the first conditionals · Splitting a sum over \(\alpha^{n+1}\) at the last coordinate

Used byBack-door adjustment for a set of predecessors

TheoremA node's table is its conditional law given a predecessor set#✓fully proved

For a set Z of predecessors of k containing its parents, the table of k is its conditional law given Z: P(X_k = a, Z = z) = p_k (a | z_{pa k}) P(Z = z).

theorem sum_filter_restrict_joint_eq_cpt_mul [Fintype α] [DecidableEq α] (k : Fin n) (a : α)
    (Z : Finset (Fin n)) (hZk : ∀ i ∈ Z, i < k) (hpaZ : ∀ j ∈ b.pa k, Fin.castLE k.2.le j ∈ Z)
    (z : Z → α) :
    ∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x =
      (b.cpt k fun j => z ⟨Fin.castLE k.2.le j, hpaZ j j.2⟩).weights a *
        ∑ x with (fun i : Z => x i) = z, b.joint x

Uses 11 · Used by 1

Statement usesBayesian network · Joint distribution of a Bayesian network

Proof usesThe intervention do(X_k = a) · Factorization of a Bayesian network · The truncated factorization · Parent values of a node · The chain of a Bayesian network · Chain of conditional distributions · Joint distribution of a chain · Joint distribution determined by the first conditionals · Splitting a sum over \(\alpha^{n+1}\) at the last coordinate

Used byBack-door adjustment for a set of predecessors

TheoremBack-door adjustment for a set of predecessors#✓fully proved

Back-door adjustment for a set of predecessors containing the parents, when the table of node k gives the value a positive probability at every value of the parents.

theorem sum_intervene_joint_mul_of_pred_of_cpt_ne_zero [Fintype α] [DecidableEq α] (k : Fin n)
    (a : α) (Z : Finset (Fin n)) (hZk : ∀ i ∈ Z, i < k)
    (hpaZ : ∀ j ∈ b.pa k, Fin.castLE k.2.le j ∈ Z) (f : (Fin n → α) → ℝ)
    (hcpt : ∀ u, (b.cpt k u).weights a ≠ 0) :
    ∑ x, (b.intervene k a).joint x * f x =
      ∑ z : Z → α, (∑ x with (fun i : Z => x i) = z, b.joint x) *
        ((∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x * f x) /
          ∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x)

Uses 5

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network

Proof usesA node's table is its conditional law given a predecessor set · Back-door adjustment for a set of predecessors containing the parents

DefinitionEdge of a Bayesian network#✓fully proved

The edge i → j of the network's graph: i is a parent of j.

def Edge (i j : Fin n) : Prop :=
  ∃ h : i.val < j.val, (⟨i.val, h⟩ : Fin j) ∈ b.pa j

Uses 1 · Used by 14

Statement usesBayesian network

Used byGlobal Markov property for finite sets of nodes · Ancestral set of nodes · The law of an ancestral set depends only on its tables · Adjacency in the skeleton of a Bayesian network · The back-door adjustment · Blocking at a node of a path · Blocking at a node is independent of path direction · Arrows of the mutilated network · Intervened nodes descend only from themselves · The front-door adjustment · Descendant relation in a Bayesian network · The reverse of a path is a path · The intervention do(X_k = a) does not change the law of the non-descendants of k · Descendants in the mutilated network are descendants in the original

DefinitionDescendant relation in a Bayesian network#✓fully proved

j is a descendant of i (every node is its own descendant).

def IsDescendant (i j : Fin n) : Prop :=
  Relation.ReflTransGen b.Edge i j

Uses 2 · Used by 8

Statement usesBayesian network · Edge of a Bayesian network

Used byGlobal Markov property for finite sets of nodes · The back-door adjustment · Blocking at a node of a path · Blocking at a node is independent of path direction · Intervened nodes descend only from themselves · The front-door adjustment · The intervention do(X_k = a) does not change the law of the non-descendants of k · Descendants in the mutilated network are descendants in the original

DefinitionAdjacency in the skeleton of a Bayesian network#✓fully proved

i and j are adjacent in the skeleton of the graph.

def Adj (i j : Fin n) : Prop :=
  b.Edge i j ∨ b.Edge j i

Uses 2 · Used by 5

Statement usesBayesian network · Edge of a Bayesian network

Used byGlobal Markov property for finite sets of nodes · The back-door adjustment · The front-door adjustment · Path in the skeleton of a Bayesian network · The reverse of a path is a path

DefinitionPath in the skeleton of a Bayesian network#✓fully proved

A path of the skeleton from x to y: a list of distinct nodes, consecutive ones adjacent, starting at x and ending at y.

def IsPath (x y : Fin n) (p : List (Fin n)) : Prop :=
  p.Nodup ∧ p.IsChain b.Adj ∧ p.head? = some x ∧ p.getLast? = some y

Uses 2 · Used by 6

Statement usesBayesian network · Adjacency in the skeleton of a Bayesian network

Used byGlobal Markov property for finite sets of nodes · The back-door adjustment · d-separation · The front-door adjustment · The reverse of a path is a path · Symmetry of d-separation

DefinitionBlocking at a node of a path#✓fully proved

The consecutive nodes u, m, w of a path are blocked by Z (Pearl 2009, Definition 1.2.3): either m is a collider u → m ← w none of whose descendants is in Z, or m is not a collider (a chain or a fork) and m ∈ Z.

def BlockedAt (Z : Set (Fin n)) (u m w : Fin n) : Prop :=
  (b.Edge u m ∧ b.Edge w m ∧ ∀ d, b.IsDescendant m d → d ∉ Z) ∨
    (¬(b.Edge u m ∧ b.Edge w m) ∧ m ∈ Z)

Uses 3 · Used by 6

Statement usesBayesian network · Edge of a Bayesian network · Descendant relation in a Bayesian network

Used byGlobal Markov property for finite sets of nodes · The back-door adjustment · Blocking at a node is independent of path direction · The front-door adjustment · Blocked path · Reversal preserves blocked paths

DefinitionBlocked path#✓fully proved

A path is blocked by Z if some three consecutive nodes of it are.

def PathBlocked (Z : Set (Fin n)) (p : List (Fin n)) : Prop :=
  ∃ (i : ℕ) (h : i + 2 < p.length), b.BlockedAt Z p[i] p[i + 1] p[i + 2]

Uses 2 · Used by 6

Statement usesBayesian network · Blocking at a node of a path

Used byGlobal Markov property for finite sets of nodes · The back-door adjustment · d-separation · The front-door adjustment · Reversal preserves blocked paths · Symmetry of d-separation

Definitiond-separation#✓fully proved

d-separation (Pearl 1988; Pearl 2009, Definition 1.2.3): Z d-separates X from Y if every path between a node of X and a node of Y is blocked by Z.

def DSeparated (X Y Z : Set (Fin n)) : Prop :=
  ∀ x ∈ X, ∀ y ∈ Y, ∀ p, b.IsPath x y p → b.PathBlocked Z p

Uses 3 · Used by 5

Statement usesBayesian network · Path in the skeleton of a Bayesian network · Blocked path

Used byThe global Markov property · Global Markov property for finite sets of nodes · The back-door adjustment · The front-door adjustment · Symmetry of d-separation

TheoremBlocking at a node is independent of path direction#✓fully proved

Blocking at a node does not depend on the direction in which the path is read.

theorem blockedAt_comm {Z : Set (Fin n)} {u m w : Fin n} :
    b.BlockedAt Z u m w ↔ b.BlockedAt Z w m u

Uses 4 · Used by 1

Statement usesBayesian network · Blocking at a node of a path

Proof usesEdge of a Bayesian network · Descendant relation in a Bayesian network

Used byReversal preserves blocked paths

TheoremThe reverse of a path is a path#✓fully proved

The reverse of a path from x to y is a path from y to x.

theorem isPath_reverse {x y : Fin n} {p : List (Fin n)} (h : b.IsPath x y p) :
    b.IsPath y x p.reverse

Uses 4 · Used by 2

Statement usesBayesian network · Path in the skeleton of a Bayesian network

Proof usesAdjacency in the skeleton of a Bayesian network · Edge of a Bayesian network

Used byGlobal Markov property for finite sets of nodes · Symmetry of d-separation

TheoremReversal preserves blocked paths#✓fully proved

If a path is blocked by Z, so is its reverse.

theorem pathBlocked_reverse {Z : Set (Fin n)} {p : List (Fin n)} (h : b.PathBlocked Z p) :
    b.PathBlocked Z p.reverse

Uses 4 · Used by 1

Statement usesBayesian network · Blocked path

Proof usesBlocking at a node of a path · Blocking at a node is independent of path direction

Used bySymmetry of d-separation

TheoremSymmetry of d-separation#✓fully proved

Symmetry of d-separation. d-separation is symmetric.

theorem DSeparated.symm {X Y Z : Set (Fin n)} (h : b.DSeparated X Y Z) : b.DSeparated Y X Z

Uses 6

Statement usesBayesian network · d-separation

Proof usesPath in the skeleton of a Bayesian network · Blocked path · The reverse of a path is a path · Reversal preserves blocked paths

DefinitionMutilated network of a set intervention#✓fully proved

The network of the intervention do(X_W = w) with the arrows into W removed: every node j ∈ W has no parents and the point mass at w j as its table.

noncomputable def mutilateSet (W : Finset (Fin n)) (w : Fin n → α) : BayesNet α n where
  pa j := if j ∈ W then ∅ else b.pa j
  cpt j z := if h : j ∈ W then StdSimplex.single (w j) else
    b.cpt j fun i => z ⟨i, by simp [h]⟩

Uses 1 · Used by 6

Statement usesBayesian network

Used byThe back-door adjustment · Arrows of the mutilated network · Intervened nodes descend only from themselves · The front-door adjustment · The truncated factorization for a set of nodes · Descendants in the mutilated network are descendants in the original

TheoremThe truncated factorization for a set of nodes#✓fully proved

After do(X_W = w), the joint is the product of the tables of the nodes outside W on assignments agreeing with w on W.

theorem joint_mutilateSet [DecidableEq α] (W : Finset (Fin n)) (w x : Fin n → α) :
    (b.mutilateSet W w).joint x = ∏ j, if j ∈ W then (if x j = w j then 1 else 0)
      else (b.cpt j (b.paVal j x)).weights (x j)

Uses 5 · Used by 2

Statement usesBayesian network · Joint distribution of a Bayesian network · Mutilated network of a set intervention · Parent values of a node

Proof usesFactorization of a Bayesian network

Used byThe back-door adjustment · The front-door adjustment

TheoremArrows of the mutilated network#✓fully proved

The arrows of b.mutilateSet W w are those of b not pointing into W.

theorem edge_mutilateSet_iff (W : Finset (Fin n)) (w : Fin n → α) {i j : Fin n} :
    (b.mutilateSet W w).Edge i j ↔ b.Edge i j ∧ j ∉ W

Uses 3 · Used by 4

Statement usesBayesian network · Edge of a Bayesian network · Mutilated network of a set intervention

Used byThe back-door adjustment · Intervened nodes descend only from themselves · The front-door adjustment · Descendants in the mutilated network are descendants in the original

TheoremDescendants in the mutilated network are descendants in the original#✓fully proved

A descendant after removing the arrows into W is a descendant in b.

theorem IsDescendant.of_mutilateSet {W : Finset (Fin n)} {w : Fin n → α} {i j : Fin n}
    (h : (b.mutilateSet W w).IsDescendant i j) : b.IsDescendant i j

Uses 5 · Used by 2

Statement usesBayesian network · Descendant relation in a Bayesian network · Mutilated network of a set intervention

Proof usesEdge of a Bayesian network · Arrows of the mutilated network

Used byThe back-door adjustment · The front-door adjustment

TheoremIntervened nodes descend only from themselves#✓fully proved

After removing the arrows into W, a node of W is a descendant only of itself.

theorem eq_of_isDescendant_mutilateSet {W : Finset (Fin n)} {w : Fin n → α} {i j : Fin n}
    (h : (b.mutilateSet W w).IsDescendant i j) (hj : j ∈ W) : i = j

Uses 5 · Used by 2

Statement usesBayesian network · Descendant relation in a Bayesian network · Mutilated network of a set intervention

Proof usesEdge of a Bayesian network · Arrows of the mutilated network

Used byThe back-door adjustment · The front-door adjustment

TheoremAssignments contradicting an intervention have probability zero#✓fully proved

After do(X_k = a), assignments with x k ≠ a have probability 0.

theorem joint_intervene_eq_zero {k : Fin n} {a : α} {x : Fin n → α}
    (hx : x k ≠ a) : (b.intervene k a).joint x = 0

Uses 5

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network

Proof usesThe truncated factorization · Parent values of a node

TheoremJoint law as interventional law times the node's table#✓fully proved

For x k = a, P(x) = P(x | do(X_k = a)) · p_k(a | x_{pa k}).

theorem joint_eq_intervene_mul_cpt {k : Fin n} {a : α} {x : Fin n → α}
    (hx : x k = a) :
    b.joint x = (b.intervene k a).joint x * (b.cpt k (b.paVal k x)).weights a

Uses 6 · Used by 2

Statement usesBayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network · Parent values of a node

Proof usesFactorization of a Bayesian network · The truncated factorization

Used byThe back-door adjustment · The front-door adjustment

TheoremThe intervention do(X_k = a) does not change the law of the non-descendants of k#✓fully proved

The intervention do(X_k = a) does not change the law of the non-descendants of k.

theorem marginal_intervene_of_not_isDescendant [Fintype α] (k : Fin n) (a : α)
    {S : Finset (Fin n)} (hS : ∀ i ∈ S, ¬b.IsDescendant k i) (x' : Fin n → α) :
    marginal (b.intervene k a).joint ↑S x' = marginal b.joint ↑S x'

Uses 12 · Used by 1

Statement usesBayesian network · Descendant relation in a Bayesian network · The intervention do(X_k = a) · Joint distribution of a Bayesian network · Marginal of a weight

Proof usesEdge of a Bayesian network · Ancestral set of nodes · Product of the tables of an ancestral set · Intervention leaves the parents of other nodes unchanged · Intervention deletes the parents of the intervened node · The law of an ancestral set depends only on its tables · Parent values of a node

Used byThe back-door adjustment

TheoremThe back-door adjustment#✓fully proved

The back-door adjustment (Pearl 1995; Pearl 2009, Theorem 3.3.2): if the set Z contains no descendant of the treatment node k and blocks every path between k and the outcome node y that begins with an arrow into k, then P(X_y = v | do(X_k = a)) = ∑_z P(Z = z) P(X_y = v | X_k = a, Z = z), assuming P(X_k = a, Z = z) > 0 whenever P(Z = z) > 0.

theorem backdoor_adjustment [Fintype α] [DecidableEq α] (k y : Fin n) (Z : Finset (Fin n))
    (a v : α) (hky : k ≠ y) (hyZ : y ∉ Z) (hdesc : ∀ z ∈ Z, ¬b.IsDescendant k z)
    (hblock : ∀ p, b.IsPath k y p → (∃ h : 1 < p.length, b.Edge p[1] k) →
      b.PathBlocked (Z : Set (Fin n)) p)
    (hpos : ∀ z : Z → α, ∑ x with (fun i : Z => x i) = z, b.joint x ≠ 0 →
      ∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x ≠ 0) :
    ∑ x with x y = v, (b.intervene k a).joint x =
      ∑ z : Z → α, (∑ x with (fun i : Z => x i) = z, b.joint x) *
        ((∑ x with x k = a ∧ x y = v ∧ (fun i : Z => x i) = z, b.joint x) /
          ∑ x with x k = a ∧ (fun i : Z => x i) = z, b.joint x)

Uses 29

Statement usesBayesian network · Edge of a Bayesian network · Descendant relation in a Bayesian network · Path in the skeleton of a Bayesian network · Blocked path · The intervention do(X_k = a) · Joint distribution of a Bayesian network

Proof usesAdjacency in the skeleton of a Bayesian network · Blocking at a node of a path · d-separation · Descendants in the mutilated network are descendants in the original · Global Markov property for finite sets of nodes · Arrows of the mutilated network · Intervened nodes descend only from themselves · Joint law as interventional law times the node's table · The truncated factorization · The truncated factorization for a set of nodes · The intervention do(X_k = a) does not change the law of the non-descendants of k · Mutilated network of a set intervention · Parent values of a node · The chain of a Bayesian network · Chain of conditional distributions · Joint distribution of a chain · Conditional independence for finite sets of nodes · Marginal on a finite set of nodes as a filtered sum · A marginal depends only on the fixed variables · Fixing more variables decreases the marginal · Conditional independence for a finite weight · Marginal of a weight

TheoremThe front-door adjustment#✓fully proved

The front-door adjustment (Pearl 1995; Pearl 2009, Theorem 3.3.4): if the set M intercepts every directed path from the treatment node k to the outcome node y, no path from k to a node of M that begins with an arrow into k is open (blocked by ∅), and every path from a node of M to y that begins with an arrow into that node is blocked by {k}, then P(X_y = v | do(X_k = a)) = ∑_m P(M = m | X_k = a) ∑_{a'} P(X_y = v | X_k = a', M = m) P(X_k = a'), assuming P(X_k = a', M = m) > 0 for all a' and m.

Cslib.MachineLearning.GraphicalModels.BayesNet.frontdoor_adjustment · 17 lines

theorem frontdoor_adjustment [Fintype α] [DecidableEq α] (k y : Fin n) (M : Finset (Fin n))
    (a v : α) (hky : k ≠ y) (hkM : k ∉ M) (hyM : y ∉ M)
    (hdir : ∀ p : List (Fin n), p.IsChain b.Edge → p.head? = some k → p.getLast? = some y →
      ∃ m ∈ M, m ∈ p)
    (hkm : ∀ m ∈ M, ∀ p, b.IsPath k m p → (∃ h : 1 < p.length, b.Edge p[1] k) →
      b.PathBlocked ∅ p)
    (hmy : ∀ m ∈ M, ∀ p, b.IsPath m y p → (∃ h : 1 < p.length, b.Edge p[1] m) →
      b.PathBlocked {k} p)
    (hpos : ∀ (a' : α) (m : M → α), ∑ x with x k = a' ∧ (fun i : M => x i) = m, b.joint x ≠ 0) :
    ∑ x with x y = v, (b.intervene k a).joint x =
      ∑ m : M → α,
        ((∑ x with x k = a ∧ (fun i : M => x i) = m, b.joint x) /
            ∑ x with x k = a, b.joint x) *
          ∑ a' : α,
            ((∑ x with x k = a' ∧ x y = v ∧ (fun i : M => x i) = m, b.joint x) /
                ∑ x with x k = a' ∧ (fun i : M => x i) = m, b.joint x) *
              ∑ x with x k = a', b.joint x

Uses 34

Statement usesBayesian network · Edge of a Bayesian network · Path in the skeleton of a Bayesian network · Blocked path · The intervention do(X_k = a) · Joint distribution of a Bayesian network

Proof usesAdjacency in the skeleton of a Bayesian network · Blocking at a node of a path · d-separation · Ancestral set of nodes · Descendant relation in a Bayesian network · Descendants in the mutilated network are descendants in the original · Product of the tables of an ancestral set · Global Markov property for finite sets of nodes · Arrows of the mutilated network · Intervened nodes descend only from themselves · Joint law as interventional law times the node's table · Factorization of a Bayesian network · The truncated factorization · The truncated factorization for a set of nodes · The law of an ancestral set depends only on its tables · Mutilated network of a set intervention · Parent values of a node · The joint distribution of a Bayesian network sums to one · The chain of a Bayesian network · Chain of conditional distributions · Joint distribution of a chain · Conditional independence for finite sets of nodes · Marginal on a finite set of nodes as a filtered sum · A marginal depends only on the fixed variables · Summing out one more variable from a marginal · Fixing more variables decreases the marginal · Conditional independence for a finite weight · Marginal of a weight

33 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.