Bayesian networks
TheoremSplitting a sum over \(\alpha^{n+1}\) at the last coordinate#✓fully proved
Let \(\alpha\) be a finite type, \(M\) an additive commutative monoid, \(n\) a natural number and \(f : \alpha^{n+1} \to M\). Then \(\sum_{x \in \alpha^{n+1}} f(x) = \sum_{y \in \alpha^n} \sum_{a \in \alpha} f(y_0, \dots, y_{n-1}, a)\), where \(y = (y_0, \dots, y_{n-1})\).
theorem sum_snoc [Fintype α] {M : Type*} [AddCommMonoid M] {n : ℕ} (f : (Fin (n + 1) → α) → M) :
∑ x, f x = ∑ y : Fin n → α, ∑ a, f (Fin.snoc y a)Used by 8
StructureChain of conditional distributions#✓fully proved
A chain of conditional distributions with values in a type \(\alpha\) assigns to every \(k \in \mathbb{N}\) and every assignment \((x_0, \dots, x_{k-1})\) of values in \(\alpha\) to the variables \(0, \dots, k - 1\) a finitely supported probability distribution \(p_k(\cdot \mid x_0, \dots, x_{k-1})\) on \(\alpha\), the conditional distribution of variable \(k\) given the earlier ones.
structure Chain (α : Type*) where
/-- The distribution of variable `k` given the values of variables `0, …, k - 1`. -/
cond : (k : ℕ) → (Fin k → α) → StdSimplex ℝ αUsed by 17
DefinitionJoint distribution of a chain#✓fully proved
For a chain of conditional distributions with values in a type \(\alpha\), write \(p_k(\cdot \mid x_0, \dots, x_{k-1})\) for the conditional distribution of variable \(k\) given the earlier ones. The joint distribution \(P_n : \alpha^n \to \mathbb{R}\) of the first \(n\) variables is defined by the chain rule: \(P_0 = 1\) and \(P_{n+1}(x_0, \dots, x_n) = P_n(x_0, \dots, x_{n-1}) \, p_n(x_n \mid x_0, \dots, x_{n-1})\).
noncomputable def joint : (n : ℕ) → (Fin n → α) → ℝ
| 0, _ => 1
| n + 1, x => joint n (Fin.init x) * (c.cond n (Fin.init x)).weights (x (Fin.last n))Uses 1 · Used by 15
TheoremMarginalizing the last variable of a chain#✓fully proved
Let \(c\) be a chain of conditional distributions with values in a finite type \(\alpha\), and write \(P_k\) for its joint distribution of the first \(k\) variables. For every \(n\) and every \(y = (y_0, \dots, y_{n-1}) \in \alpha^n\), \(\sum_{a \in \alpha} P_{n+1}(y_0, \dots, y_{n-1}, a) = P_n(y)\).
theorem sum_joint_snoc [Fintype α] (n : ℕ) (y : Fin n → α) :
∑ a, c.joint (n + 1) (Fin.snoc y a) = c.joint n yUses 2 · Used by 1
TheoremThe joint distribution of a chain sums to one#✓fully proved
Let \(c\) be a chain of conditional distributions with values in a finite type \(\alpha\), and write \(P_n\) for its joint distribution of the first \(n\) variables. For every \(n\), \(\sum_{x \in \alpha^n} P_n(x) = 1\).
theorem sum_joint [Fintype α] : ∀ n : ℕ, ∑ x, c.joint n x = 1Uses 4 · Used by 1
TheoremConditionals of the joint of a chain#✓fully proved
Let \(c\) be a chain of conditional distributions with values in a type \(\alpha\), let \(P_m\) be its joint distribution of the first \(m\) variables, and let \(p_n(\cdot \mid y)\) be its conditional distribution of variable \(n\) given values \(y \in \alpha^n\) of the earlier ones. For every \(n\), every \(y \in \alpha^n\) with \(P_n(y) \ne 0\) and every \(a \in \alpha\), we have \(P_{n+1}(y, a) / P_n(y) = p_n(a \mid y)\), where \((y, a) \in \alpha^{n+1}\) extends \(y\) by the value \(a\).
theorem cond_eq_div {n : ℕ} {y : Fin n → α} (hy : c.joint n y ≠ 0) (a : α) :
c.joint (n + 1) (Fin.snoc y a) / c.joint n y = (c.cond n y).weights aUses 2 · Used by 1
TheoremFactorization of the joint of a chain#✓fully proved
For a chain of conditional distributions with values in a type \(\alpha\), write \(p_k(\cdot \mid x_0, \dots, x_{k-1})\) for the conditional distribution of variable \(k\) given the earlier ones and \(P_n\) for the joint distribution of the first \(n\) variables. Then for every \(n\) and every \(x \in \alpha^n\) we have \(P_n(x) = \prod_{k < n} p_k(x_k \mid x_0, \dots, x_{k-1})\).
theorem joint_eq_prod : ∀ (n : ℕ) (x : Fin n → α),
c.joint n x = ∏ k : Fin n, (c.cond k fun j => x (Fin.castLE k.2.le j)).weights (x k)Uses 2 · Used by 1
TheoremJoint distribution determined by the first conditionals#✓fully proved
Let \(n \in \mathbb{N}\). If two chains of conditional distributions \(c\) and \(c'\) with values in a type \(\alpha\) have the same conditional distribution of variable \(k\) given the earlier variables for every \(k < n\), then they have the same joint distribution of the first \(n\) variables.
theorem joint_congr {c' : Chain α} : ∀ {n : ℕ}, (∀ k < n, c.cond k = c'.cond k) →
c.joint n = c'.joint nstructure Chain (α : Type*) where
/-- The distribution of variable `k` given the values of variables `0, …, k - 1`. -/
cond : (k : ℕ) → (Fin k → α) → StdSimplex ℝ αCSLibExt/MachineLearning/GraphicalModels/BayesianNetwork.lean:61
Uses 2 · Used by 4
DefinitionReplacing one conditional of a chain#✓fully proved
Given a chain \(c\) of conditional distributions with values in \(\alpha\), an index \(n\) and a family \(f\) assigning to each \(y \in \alpha^n\) a probability distribution \(f(y)\) on \(\alpha\), the updated chain has conditional distribution \(f\) for variable \(n\) and the same conditional distribution as \(c\) for every other variable.
def update (n : ℕ) (f : (Fin n → α) → StdSimplex ℝ α) : Chain α where
cond k := if h : k = n then h ▸ f else c.cond kstructure Chain (α : Type*) where
/-- The distribution of variable `k` given the values of variables `0, …, k - 1`. -/
cond : (k : ℕ) → (Fin k → α) → StdSimplex ℝ αCSLibExt/MachineLearning/GraphicalModels/BayesianNetwork.lean:61
cond : (k : ℕ) → (Fin k → α) → StdSimplex ℝ αCSLibExt/MachineLearning/GraphicalModels/BayesianNetwork.lean:63
Uses 1 · Used by 1
TheoremThe chain rule#✓fully proved
Let \(\alpha\) be a finite nonempty type and \(n \in \mathbb{N}\). For every function \(P : \alpha^n \to \mathbb{R}\) with \(P(x) \ge 0\) for all \(x\) and \(\sum_x P(x) = 1\), there is a chain of conditional distributions with values in \(\alpha\) whose joint distribution of the first \(n\) variables equals \(P\).
theorem exists_chain [Fintype α] [Nonempty α] : ∀ (n : ℕ) (P : (Fin n → α) → ℝ),
(∀ x, 0 ≤ P x) → ∑ x, P x = 1 → ∃ c : Chain α, ∀ x, P x = c.joint n xstructure Chain (α : Type*) where
/-- The distribution of variable `k` given the values of variables `0, …, k - 1`. -/
cond : (k : ℕ) → (Fin k → α) → StdSimplex ℝ αCSLibExt/MachineLearning/GraphicalModels/BayesianNetwork.lean:61
StructureBayesian network#✓fully proved
A Bayesian network with values in a type \(\alpha\) on the nodes \(0, \dots, n - 1\), listed in a topological order, assigns to each node \(k\) a finite set of parents among the earlier nodes \(0, \dots, k - 1\), and a conditional probability table: for each assignment of values in \(\alpha\) to the parents of \(k\), a finitely supported probability distribution on \(\alpha\) for the value of node \(k\).
structure BayesNet (α : Type*) (n : ℕ) where
/-- The parents of node `k`, among the nodes `0, …, k - 1`. -/
pa : (k : Fin n) → Finset (Fin k)
/-- The distribution of node `k` given the values of its parents. -/
cpt : (k : Fin n) → (pa k → α) → StdSimplex ℝ α pa : (k : Fin n) → Finset (Fin k)CSLibExt/MachineLearning/GraphicalModels/BayesianNetwork.lean:172
Used by 44
do(X_k = a) · Intervention leaves the parents of other nodes unchanged · Intervention deletes the parents of the intervened node · Descendant relation in a Bayesian network · Path in the skeleton of a Bayesian network · The reverse of a path is a path · 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 · Mutilated network of a set intervention · Descendants in the mutilated network are descendants in the original · Parent values of a node · Blocked path · Reversal preserves blocked paths · 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 · Symmetry of d-separationDefinitionThe chain of a Bayesian network#✓fully proved
A Bayesian network \(b\) on nodes \(0, \dots, n - 1\) with values in a nonempty type \(\alpha\) defines a chain of conditional distributions. For \(k < n\), the conditional distribution of variable \(k\) given values \(y_0, \dots, y_{k-1}\) of the earlier variables is the table of node \(k\) applied to the values \(y_j\) of its parents \(j\). For \(k \ge n\) it is the point mass at a fixed arbitrary element of \(\alpha\).
noncomputable def toChain : Chain α where
cond k y := if hk : k < n then b.cpt ⟨k, hk⟩ fun j => y j else
StdSimplex.single (Classical.arbitrary α)structure Chain (α : Type*) where
/-- The distribution of variable `k` given the values of variables `0, …, k - 1`. -/
cond : (k : ℕ) → (Fin k → α) → StdSimplex ℝ αCSLibExt/MachineLearning/GraphicalModels/BayesianNetwork.lean:61
cond : (k : ℕ) → (Fin k → α) → StdSimplex ℝ αCSLibExt/MachineLearning/GraphicalModels/BayesianNetwork.lean:63
Uses 2 · Used by 10
DefinitionJoint distribution of a Bayesian network#✓fully proved
Let \(B\) be a Bayesian network on the nodes \(0, \dots, n - 1\) with values in a nonempty type \(\alpha\). The joint distribution of \(B\) is the function \(P : \alpha^n \to \mathbb{R}\) given by \(P(x) = P_n(x)\) for \(x \in \alpha^n\), where \(P_n\) is the joint distribution of the first \(n\) variables of the chain of conditional distributions of \(B\).
noncomputable def joint (x : Fin n → α) : ℝ :=
b.toChain.joint n xUses 3 · Used by 20
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 parentsTheoremFactorization of a Bayesian network#✓fully proved
The joint is the product over nodes of the probability of the node's value given the values of its parents.
theorem joint_eq_prod (x : Fin n → α) :
b.joint x = ∏ k : Fin n, (b.cpt k fun j => x (Fin.castLE k.2.le j)).weights (x k)Uses 6 · Used by 9
TheoremThe joint distribution of a Bayesian network sums to one#✓fully proved
Let \(B\) be a Bayesian network on the nodes \(0, \dots, n - 1\) with values in a finite nonempty type \(\alpha\), and let \(P\) be its joint distribution. Then \(\sum_{x \in \alpha^n} P(x) = 1\).
theorem sum_joint [Fintype α] : ∑ x, b.joint x = 1Uses 4 · Used by 1
TheoremThe ordered Markov property#✓fully proved
Let \(B\) be a Bayesian network on the nodes \(0, \dots, n - 1\) with values in a nonempty type \(\alpha\), and let \(P_m\) be the joint distribution of the first \(m\) nodes of \(B\) viewed as a chain of conditional distributions. For a node \(k < n\), write \(p_k(\cdot \mid z)\) for its conditional probability table at values \(z\) of its parents. Let \(y = (y_0, \dots, y_{k-1}) \in \alpha^k\) with \(P_k(y) \ne 0\), and write \(y_{\mathrm{pa}(k)}\) for the values of \(y\) at the parents of \(k\). Then for every \(a \in \alpha\),
In particular, the conditional distribution of node \(k\) given all earlier nodes depends only on the values of its parents.
theorem cond_eq_cpt {k : ℕ} (hk : k < n) {y : Fin k → α} (hy : b.toChain.joint k y ≠ 0)
(a : α) :
b.toChain.joint (k + 1) (Fin.snoc y a) / b.toChain.joint k y =
(b.cpt ⟨k, hk⟩ fun j => y j).weights aUses 5
TheoremMarginal on a finite set of nodes as a filtered sum#✓fully proved
FiniteWeight.marginal on a Finset of nodes, as a sum over a decidable filter.
theorem marginal_coe [DecidableEq α] (P : (Fin n → α) → ℝ) (S : Finset (Fin n)) (x' : Fin n → α) :
marginal P ↑S x' = ∑ x with ∀ i ∈ S, x i = x' i, P xnoncomputable def marginal (p : (V → α) → ℝ) (U : Set V) (x : V → α) : ℝ :=
∑ y ∈ univ.filter (fun y : V → α => ∀ v ∈ U, y v = x v), p yMathlibExt/Probability/FiniteWeight.lean:65
Uses 1 · Used by 6
TheoremConditional independence for finite sets of nodes#✓fully proved
FiniteWeight.CondIndep for Finsets of nodes, with the unions taken in Finset.
theorem condIndep_coe_iff {P : (Fin n → α) → ℝ} {X Y Z : Finset (Fin n)} :
CondIndep P ↑X ↑Y ↑Z ↔ ∀ x', marginal P ↑(X ∪ Y ∪ Z) x' * marginal P ↑Z x' =
marginal P ↑(X ∪ Z) x' * marginal P ↑(Y ∪ Z) x'def CondIndep (p : (V → α) → ℝ) (A B S : Set V) : Prop :=
∀ x, marginal p (A ∪ B ∪ S) x * marginal p S x = marginal p (A ∪ S) x * marginal p (B ∪ S) xMathlibExt/Probability/FiniteWeight.lean:84
noncomputable def marginal (p : (V → α) → ℝ) (U : Set V) (x : V → α) : ℝ :=
∑ y ∈ univ.filter (fun y : V → α => ∀ v ∈ U, y v = x v), p yMathlibExt/Probability/FiniteWeight.lean:65
Uses 2 · Used by 6
TheoremA marginal depends only on the fixed variables#✓fully proved
marginal P S x' depends only on the values of x' on S.
theorem marginal_congr_of_eqOn (P : (Fin n → α) → ℝ) (S : Finset (Fin n)) {x y : Fin n → α}
(h : ∀ i ∈ S, x i = y i) : marginal P ↑S x = marginal P ↑S ynoncomputable def marginal (p : (V → α) → ℝ) (U : Set V) (x : V → α) : ℝ :=
∑ y ∈ univ.filter (fun y : V → α => ∀ v ∈ U, y v = x v), p yMathlibExt/Probability/FiniteWeight.lean:65
Uses 2 · Used by 3
TheoremFixing more variables decreases the marginal#✓fully proved
Fixing more variables decreases the probability.
theorem marginal_le_of_subset {P : (Fin n → α) → ℝ} (hP : ∀ x, 0 ≤ P x)
{S T : Finset (Fin n)} (hST : S ⊆ T) (x' : Fin n → α) :
marginal P ↑T x' ≤ marginal P ↑S x'noncomputable def marginal (p : (V → α) → ℝ) (U : Set V) (x : V → α) : ℝ :=
∑ y ∈ univ.filter (fun y : V → α => ∀ v ∈ U, y v = x v), p yMathlibExt/Probability/FiniteWeight.lean:65
Uses 2 · Used by 3
TheoremSumming out one more variable from a marginal#✓fully proved
Summing out one more variable i ∉ S.
theorem marginal_eq_sum_insert (P : (Fin n → α) → ℝ) {S : Finset (Fin n)} {i : Fin n}
(hi : i ∉ S) (x' : Fin n → α) :
marginal P ↑S x' = ∑ a, marginal P ↑(insert i S) (Function.update x' i a)noncomputable def marginal (p : (V → α) → ℝ) (U : Set V) (x : V → α) : ℝ :=
∑ y ∈ univ.filter (fun y : V → α => ∀ v ∈ U, y v = x v), p yMathlibExt/Probability/FiniteWeight.lean:65
Uses 2 · Used by 2
TheoremSymmetry of conditional independence#✓fully proved
Conditional independence is symmetric.
theorem condIndep_symm {P : (Fin n → α) → ℝ} {X Y Z : Finset (Fin n)}
(h : CondIndep P ↑X ↑Y ↑Z) : CondIndep P ↑Y ↑X ↑Zdef CondIndep (p : (V → α) → ℝ) (A B S : Set V) : Prop :=
∀ x, marginal p (A ∪ B ∪ S) x * marginal p S x = marginal p (A ∪ S) x * marginal p (B ∪ S) xMathlibExt/Probability/FiniteWeight.lean:84
Uses 3 · Used by 1
TheoremDecomposition#✓fully proved
If X ⫫ Y | Z then X' ⫫ Y | Z for X' ⊆ X.
theorem condIndep_mono_left {P : (Fin n → α) → ℝ} {X X' Y Z : Finset (Fin n)}
(h : CondIndep P ↑X ↑Y ↑Z) (hX' : X' ⊆ X) (hXY : Disjoint X Y) : CondIndep P ↑X' ↑Y ↑Zdef CondIndep (p : (V → α) → ℝ) (A B S : Set V) : Prop :=
∀ x, marginal p (A ∪ B ∪ S) x * marginal p S x = marginal p (A ∪ S) x * marginal p (B ∪ S) xMathlibExt/Probability/FiniteWeight.lean:84
Uses 5 · Used by 2
TheoremWeak union#✓fully proved
If X ∪ W ⫫ Y | Z then X ⫫ Y | Z ∪ W (for a nonnegative law).
theorem condIndep_weak_union {P : (Fin n → α) → ℝ} (hP : ∀ x, 0 ≤ P x)
{X W Y Z : Finset (Fin n)} (h : CondIndep P ↑(X ∪ W) ↑Y ↑Z) (hXY : Disjoint (X ∪ W) Y) :
CondIndep P ↑X ↑Y ↑(Z ∪ W)def CondIndep (p : (V → α) → ℝ) (A B S : Set V) : Prop :=
∀ x, marginal p (A ∪ B ∪ S) x * marginal p S x = marginal p (A ∪ S) x * marginal p (B ∪ S) xMathlibExt/Probability/FiniteWeight.lean:84
Uses 5 · Used by 1
DefinitionAncestral set of nodes#✓fully proved
A set of nodes is ancestral if it contains the parents of each of its nodes.
Uses 2 · Used by 4
DefinitionProduct of the tables of an ancestral set#✓fully proved
The product of the tables of the nodes in A, with the uniform distribution on the other
nodes. For an ancestral A it has the same marginals on A as the joint
(marginal_joint_eq_ancProd).
noncomputable def ancProd [Fintype α] (A : Finset (Fin n)) (x : Fin n → α) : ℝ :=
∏ j, if j ∈ A then (b.cpt j (b.paVal j x)).weights (x j) else (Fintype.card α : ℝ)⁻¹Uses 2 · Used by 5
TheoremThe ancestral product on all nodes is the joint#✓fully proved
On all nodes, ancProd is the joint.
Uses 5 · Used by 2
TheoremThe law of an ancestral set depends only on its tables#✓fully proved
For an ancestral set A and
S ⊆ A, the marginals of the joint on S are those of ancProd A.
theorem marginal_joint_eq_ancProd [Fintype α] {A : Finset (Fin n)}
(hA : b.IsAncestral A) {S : Finset (Fin n)} (hS : S ⊆ A) (x' : Fin n → α) :
marginal b.joint ↑S x' = marginal (b.ancProd A) ↑S x'noncomputable def marginal (p : (V → α) → ℝ) (U : Set V) (x : V → α) : ℝ :=
∑ y ∈ univ.filter (fun y : V → α => ∀ v ∈ U, y v = x v), p yMathlibExt/Probability/FiniteWeight.lean:65
Uses 9 · Used by 2
TheoremGlobal Markov property for finite sets of nodes#✓fully proved
The global Markov property for Finsets of nodes; condIndep_of_dSeparated is the
statement for arbitrary sets of nodes.
theorem condIndep_of_dSeparated_finset [Fintype α] {X Y Z : Finset (Fin n)}
(h : b.DSeparated (X : Set (Fin n)) (Y : Set (Fin n)) (Z : Set (Fin n))) :
CondIndep b.joint ↑X ↑Y ↑Zdef CondIndep (p : (V → α) → ℝ) (A B S : Set V) : Prop :=
∀ x, marginal p (A ∪ B ∪ S) x * marginal p S x = marginal p (A ∪ S) x * marginal p (B ∪ S) xMathlibExt/Probability/FiniteWeight.lean:84
Uses 21 · Used by 3
TheoremThe global Markov property#✓fully proved
The global Markov property (soundness of d-separation: Geiger, Verma & Pearl 1990;
Lauritzen, Dawid, Larsen & Leimer 1990): if Z d-separates X from Y in the graph of a
Bayesian network, then X and Y are conditionally independent given Z under its joint
law. No disjointness of X, Y, Z is needed.
theorem condIndep_of_dSeparated [Fintype α] {X Y Z : Set (Fin n)} (h : b.DSeparated X Y Z) :
CondIndep b.joint X Y Zdef CondIndep (p : (V → α) → ℝ) (A B S : Set V) : Prop :=
∀ x, marginal p (A ∪ B ∪ S) x * marginal p S x = marginal p (A ∪ S) x * marginal p (B ∪ S) xMathlibExt/Probability/FiniteWeight.lean:84
Uses 5
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.