Conditional independence on finite configuration spaces

DefinitionMarginal of a weight#✓fully proved

Let \(V\) and \(\alpha\) be finite types, a configuration being a map \(x : V \to \alpha\), and let \(p\) be a real-valued weight on configurations. The (unnormalized) marginal of \(p\) on a set of variables \(U \subseteq V\) at a configuration \(x\) is

\[\sum_{y \,:\, y(v) = x(v) \text{ for all } v \in U} p(y),\]

the total weight of the configurations that agree with \(x\) on \(U\).

noncomputable def marginal (p : (V → α) → ℝ) (U : Set V) (x : V → α) : ℝ :=
  ∑ y ∈ univ.filter (fun y : V → α => ∀ v ∈ U, y v = x v), p y

Used by 21

Used byConditional independence for finite sets of nodes · Decomposition · Global Markov property for finite sets of nodes · Symmetry of conditional independence · Weak union · 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 · The law of an ancestral set depends only on its tables · Fixing more variables decreases the marginal · The back-door adjustment · The front-door adjustment · The intervention do(X_k = a) does not change the law of the non-descendants of k · Conditional independence in ratio form · Conditional independence for a finite weight · Conditional independence can be read off a marginal · The factorization criterion for conditional independence · Conditional independence from the variables outside the conditioning set · Monotonicity of marginals in the fixed variables · Marginalizing in two steps · Marginals of a product

TheoremMonotonicity of marginals in the fixed variables#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(p\) be a real-valued weight on the configurations \(x : V \to \alpha\) with \(p(x) \ge 0\) for every \(x\), and let \(U \subseteq U' \subseteq V\). Then for every configuration \(x\), the marginal of \(p\) on \(U'\) at \(x\) is at most the marginal of \(p\) on \(U\) at \(x\).

theorem marginal_anti {p : (V → α) → ℝ} (hp : ∀ x, 0 ≤ p x) {U U' : Set V} (h : U ⊆ U')
    (x : V → α) : marginal p U' x ≤ marginal p U x

Uses 1 · Used by 1

Statement usesMarginal of a weight

Used byFixing more variables decreases the marginal

DefinitionConditional independence for a finite weight#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(p\) be a real-valued weight on the configurations \(x : V \to \alpha\), and for \(U \subseteq V\) write \(p(x_U)\) for the marginal of \(p\) on \(U\) at \(x\), the total weight of the configurations that agree with \(x\) on \(U\). For \(A, B, S \subseteq V\), the variables in \(A\) and in \(B\) are conditionally independent given those in \(S\) under \(p\) when

\[p(x_{A \cup B \cup S})\, p(x_S) = p(x_{A \cup S})\, p(x_{B \cup S})\]

for every configuration \(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) x

Uses 1 · Used by 12

Statement usesMarginal of a weight

Used byConditional independence for finite sets of nodes · Decomposition · The global Markov property · Global Markov property for finite sets of nodes · Symmetry of conditional independence · Weak union · The back-door adjustment · The front-door adjustment · Conditional independence in ratio form · Conditional independence can be read off a marginal · The factorization criterion for conditional independence · Conditional independence from the variables outside the conditioning set

TheoremConditional independence in ratio form#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(p\) be a real-valued weight on the configurations \(x : V \to \alpha\), and for \(U \subseteq V\) write \(p(x_U)\) for the marginal of \(p\) on \(U\) at \(x\). If, for \(A, B, S \subseteq V\), the variables in \(A\) and in \(B\) are conditionally independent given those in \(S\) under \(p\), then every configuration \(x\) with \(p(x_S) \ne 0\) satisfies

\[\frac{p(x_{A\cup B\cup S})}{p(x_S)} = \frac{p(x_{A\cup S})}{p(x_S)}\frac{p(x_{B\cup S})}{p(x_S)}\]

For a nonnegative weight of positive total mass these ratios are the conditional probabilities of the normalized distribution, so this is \(P(x_A, x_B \mid x_S) = P(x_A \mid x_S)\, P(x_B \mid x_S)\).

theorem CondIndep.cond_eq_mul {p : (V → α) → ℝ} {A B S : Set V} (h : CondIndep p A B S)
    {x : V → α} (hx : marginal p S x ≠ 0) :
    marginal p (A ∪ B ∪ S) x / marginal p S x =
      (marginal p (A ∪ S) x / marginal p S x) * (marginal p (B ∪ S) x / marginal p S x)

Uses 2

Statement usesConditional independence for a finite weight · Marginal of a weight

TheoremMarginals of a product#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(f\) and \(g\) be real-valued weights on the configurations \(x : V \to \alpha\), and let \(P, Q, U \subseteq V\) with \(P \cup Q = V\) and \(P \cap Q \subseteq U\), such that \(f(x)\) depends only on the values of \(x\) on \(P\) and \(g(x)\) only on its values on \(Q\). Write \(fg\) for the pointwise product, \(P^c\) and \(Q^c\) for the complements in \(V\), and, for a weight \(h\), a set \(T \subseteq V\) and a configuration \(x\), \(m_h(T, x)\) for the marginal of \(h\) on \(T\) at \(x\), the total weight of the configurations that agree with \(x\) on \(T\). Then for every configuration \(x\),

\[m_{fg}(U, x) = m_f(U \cup P^c, x)\, m_g(U \cup Q^c, x).\]

Here the free variables of \(f\) are those of \(P\) outside \(U\), and those of \(g\) are those of \(Q\) outside \(U\).

theorem marginal_mul {f g : (V → α) → ℝ} {P Q U : Set V} (hf : DependsOn f P) (hg : DependsOn g Q)
    (hPQ : ∀ v, v ∈ P ∨ v ∈ Q) (hU : P ∩ Q ⊆ U) (x : V → α) :
    marginal (f * g) U x = marginal f (U ∪ Pᶜ) x * marginal g (U ∪ Qᶜ) x

Uses 1 · Used by 1

Statement usesMarginal of a weight

Used byThe factorization criterion for conditional independence

TheoremThe factorization criterion for conditional independence#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(f\) and \(g\) be real-valued weights on the configurations \(x : V \to \alpha\), and let \(P, Q \subseteq V\) with \(P \cup Q = V\) such that \(f(x)\) depends only on the values of \(x\) on \(P\) and \(g(x)\) only on its values on \(Q\). If \(A \subseteq V\) is disjoint from \(Q\) and \(B \subseteq V\) is disjoint from \(P\), then the variables in \(A\) and in \(B\) are conditionally independent given those in \(P \cap Q\) under the pointwise product \(fg\).

theorem condIndep_of_dependsOn {f g : (V → α) → ℝ} {P Q : Set V} (hf : DependsOn f P)
    (hg : DependsOn g Q) (hPQ : ∀ v, v ∈ P ∨ v ∈ Q) {A B : Set V} (hA : ∀ v ∈ A, v ∉ Q)
    (hB : ∀ v ∈ B, v ∉ P) : CondIndep (f * g) A B (P ∩ Q)

Uses 3

Statement usesConditional independence for a finite weight

Proof usesMarginal of a weight · Marginals of a product

TheoremConditional independence from the variables outside the conditioning set#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(p\) be a real-valued weight on the configurations \(x : V \to \alpha\), and let \(A, B, S \subseteq V\). If the variables in \(A \setminus S\) and in \(B \setminus S\) are conditionally independent given those in \(S\) under \(p\), then the variables in \(A\) and in \(B\) are conditionally independent given those in \(S\) under \(p\).

theorem condIndep_of_sdiff {p : (V → α) → ℝ} {A B S : Set V}
    (h : CondIndep p (A \ S) (B \ S) S) : CondIndep p A B S

Uses 2

Statement usesConditional independence for a finite weight

Proof usesMarginal of a weight

TheoremAgreement classes of configurations have equal size#✓fully proved

Let \(V\) and \(\alpha\) be finite types and \(W \subseteq V\). For any two configurations \(x, z : V \to \alpha\), the number of configurations \(y : V \to \alpha\) with \(y(v) = z(v)\) for all \(v \in W\) equals the number of configurations \(y\) with \(y(v) = x(v)\) for all \(v \in W\).

theorem card_filter_agree (W : Set V) (x z : V → α) :
    (univ.filter fun y : V → α => ∀ v ∈ W, y v = z v).card =
      (univ.filter fun y : V → α => ∀ v ∈ W, y v = x v).card

Used by 1

Used byMarginalizing in two steps

TheoremMarginalizing in two steps#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(p\) be a real-valued weight on the configurations \(x : V \to \alpha\), let \(U \subseteq W \subseteq V\), and let \(p_W\) be the \(W\)-marginal of \(p\), the weight sending \(x\) to the total weight of the configurations that agree with \(x\) on \(W\). Then for every configuration \(x\), the \(U\)-marginal of \(p_W\) at \(x\) equals \(N\) times the \(U\)-marginal of \(p\) at \(x\), where \(N\) is the number of configurations that agree with \(x\) on \(W\) (the number of assignments of values to the variables outside \(W\)).

theorem marginal_marginal (p : (V → α) → ℝ) {U W : Set V} (h : U ⊆ W) (x : V → α) :
    marginal (marginal p W) U x =
      (univ.filter fun y : V → α => ∀ v ∈ W, y v = x v).card * marginal p U x

Uses 2 · Used by 1

Statement usesMarginal of a weight

Proof usesAgreement classes of configurations have equal size

Used byConditional independence can be read off a marginal

TheoremConditional independence can be read off a marginal#✓fully proved

Let \(V\) and \(\alpha\) be finite types, let \(p\) be a real-valued weight on the configurations \(x : V \to \alpha\), let \(W \subseteq V\), and let \(p_W\) be the \(W\)-marginal of \(p\), the weight sending \(x\) to the total weight of the configurations that agree with \(x\) on \(W\). For all \(A, B, S \subseteq W\), the variables in \(A\) and in \(B\) are conditionally independent given those in \(S\) under \(p_W\) if and only if they are conditionally independent given those in \(S\) under \(p\).

theorem condIndep_marginal_iff {p : (V → α) → ℝ} {A B S W : Set V} (hA : A ⊆ W) (hB : B ⊆ W)
    (hS : S ⊆ W) : CondIndep (marginal p W) A B S ↔ CondIndep p A B S

Uses 3

Statement usesConditional independence for a finite weight · Marginal of a weight

Proof usesMarginalizing in two steps

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.