From 6cedbb703a9aa71ecd1816df98eb64e869a1a218 Mon Sep 17 00:00:00 2001 From: zixiaowang17 Date: Wed, 14 Oct 2026 17:14:47 -0400 Subject: [PATCH] feat: add abstract graphical Markov properties --- Statlib.lean | 1 + .../Combinatorics/SimpleGraph/Markov.lean | 127 ++++++++++++++++++ 2 files changed, 128 insertions(+) create mode 100644 Statlib/ForMathlib/Combinatorics/SimpleGraph/Markov.lean diff --git a/Statlib.lean b/Statlib.lean index 12c1108..7617b0d 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -5,6 +5,7 @@ import Statlib.EValues.EVariable import Statlib.EValues.Utility.Basic import Statlib.EValues.Utility.Log import Statlib.ForMathlib.Algebra.Order.Group.PosPart +import Statlib.ForMathlib.Combinatorics.SimpleGraph.Markov import Statlib.ForMathlib.Convex import Statlib.ForMathlib.ENNReal import Statlib.ForMathlib.EReal diff --git a/Statlib/ForMathlib/Combinatorics/SimpleGraph/Markov.lean b/Statlib/ForMathlib/Combinatorics/SimpleGraph/Markov.lean new file mode 100644 index 0000000..60d93c8 --- /dev/null +++ b/Statlib/ForMathlib/Combinatorics/SimpleGraph/Markov.lean @@ -0,0 +1,127 @@ +/- +Copyright (c) 2026 Zixiao Wang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zixiao Wang +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Walk.Basic + +/-! +# The global, local, and pairwise Markov properties + +An independence relation is a ternary relation on sets. A semigraphoid satisfies symmetry, +decomposition, weak union, and contraction. This module connects such relations to separation +in an undirected graph. + +## Main definitions and results + +* `IndependenceRelation` and `IndependenceRelation.IsSemigraphoid`: abstract independence. +* `SimpleGraph.Separates`: every walk between the two sets meets the separating set. +* `IndependenceRelation.IsGlobalMarkov`, `IndependenceRelation.IsLocalMarkov`, and + `IndependenceRelation.IsPairwiseMarkov`: the three graphical Markov properties. +* `IndependenceRelation.IsGlobalMarkov.isLocalMarkov`: global implies local, with no axioms + on the independence relation. +* `IndependenceRelation.IsLocalMarkov.isPairwiseMarkov`: local implies pairwise for a semigraphoid. + +## Implementation notes + +The vertex type is arbitrary. Semigraphoid axioms apply to all subsets, including overlapping +sets. Global Markov requires pairwise disjoint sets and allows empty sets. The conditioning +set in local Markov is the entire neighborhood, which may be infinite. + +## References + +* David Montague and Bala Rajaratnam, *Graphical Markov models for infinitely many variables*, + Transactions of the American Mathematical Society **370** (2018), no. 11, 7557–7603, + Section 4. [doi:10.1090/tran/7048](https://doi.org/10.1090/tran/7048). + +## Tags + +conditional independence, semigraphoid, graphical model, Markov property, graph separation +-/ + +@[expose] public section + +open Set + +universe u + +/-- An abstract independence relation on subsets of a type. +`R A B S` expresses that `A` and `B` are independent given `S`. -/ +abbrev IndependenceRelation (V : Type*) := Set V → Set V → Set V → Prop + +namespace IndependenceRelation + +variable {V : Type u} + +/-- An independence relation satisfying symmetry, decomposition, weak union, and contraction. +The axioms apply to arbitrary subsets, including infinite and overlapping sets. -/ +structure IsSemigraphoid (R : IndependenceRelation V) : Prop where + /-- Symmetry in the two independent sets. -/ + symm : ∀ {A B S}, R A B S → R B A S + /-- Independence from a union implies independence from each set. -/ + decomp : ∀ {A B C S}, R A (B ∪ C) S → R A B S ∧ R A C S + /-- Part of the second set can be moved into the conditioning set. -/ + weak_union : ∀ {A B C S}, R A (B ∪ C) S → R A B (S ∪ C) + /-- Combine independence statements with nested conditioning sets. -/ + contraction : ∀ {A B C S}, R A B (S ∪ C) → R A C S → R A (B ∪ C) S + +end IndependenceRelation + +namespace SimpleGraph + +variable {V : Type*} + +/-- `G.Separates A B S` means that every walk in `G` from `A` to `B` contains a vertex of `S`, +possibly at an endpoint. -/ +def Separates (G : SimpleGraph V) (A B S : Set V) : Prop := + ∀ ⦃a b : V⦄, a ∈ A → b ∈ B → ∀ p : G.Walk a b, ∃ v ∈ p.support, v ∈ S + +/-- The neighborhood of a vertex separates it from the vertices outside its closed neighborhood. -/ +theorem neighborSet_separates_singleton (G : SimpleGraph V) (i : V) : + G.Separates {i} (({i} ∪ G.neighborSet i)ᶜ) (G.neighborSet i) := by + rintro a b rfl hb p + cases p with + | nil => exact (hb (Or.inl rfl)).elim + | cons hij q => exact ⟨_, by simp, hij⟩ + +end SimpleGraph + +namespace IndependenceRelation + +open SimpleGraph + +variable {V : Type u} + +/-- Any two distinct nonadjacent vertices are independent given all remaining vertices. -/ +def IsPairwiseMarkov (R : IndependenceRelation V) (G : SimpleGraph V) : Prop := + ∀ ⦃i j : V⦄, i ≠ j → ¬ G.Adj i j → R {i} {j} ({i, j}ᶜ) + +/-- Each vertex is independent of the vertices outside its closed neighborhood, +given its neighborhood. -/ +def IsLocalMarkov (R : IndependenceRelation V) (G : SimpleGraph V) : Prop := + ∀ i, R {i} (({i} ∪ G.neighborSet i)ᶜ) (G.neighborSet i) + +/-- For pairwise disjoint sets `A`, `B`, and `S`, separation of `A` and `B` by `S` +implies their independence given `S`. -/ +def IsGlobalMarkov (R : IndependenceRelation V) (G : SimpleGraph V) : Prop := + ∀ ⦃A B S : Set V⦄, Disjoint A B → Disjoint A S → Disjoint B S → + G.Separates A B S → R A B S + +/-- The global Markov property implies the local Markov property for any independence relation. -/ +theorem IsGlobalMarkov.isLocalMarkov {R : IndependenceRelation V} {G : SimpleGraph V} + (h : IsGlobalMarkov R G) : IsLocalMarkov R G := fun i ↦ + h (by simp) (by simp) (by simp [disjoint_compl_left_iff]) + (G.neighborSet_separates_singleton i) + +/-- The local Markov property implies the pairwise Markov property for a semigraphoid. -/ +theorem IsLocalMarkov.isPairwiseMarkov {R : IndependenceRelation V} {G : SimpleGraph V} + (hR : IsSemigraphoid R) (h : IsLocalMarkov R G) : IsPairwiseMarkov R G := by + intro i j hij hadj + convert hR.weak_union (B := {j}) (C := (({i} ∪ G.neighborSet i)ᶜ \ {j})) + (by simpa [hij.symm, hadj] using h i) using 1 + apply compl_injective + simp [compl_sdiff, inter_insert_of_mem, hadj] + +end IndependenceRelation