← Copula mathematical handbook

Regular-vine structures by nested path attachment

A new variable is attached along a path through the existing vine's nested coordinate clusters. Each new higher-tree edge shares an immediate parent with its two endpoints: the proximity condition is built into the construction. Always taking the left child gives a C-vine; always taking the right child gives a D-vine. Mixed paths give other regular vines.

inductive ProbabilityTheory.Copula.Vine.Tree (d : ℕ) : Type

A labelled ancestral representation of the top edge of a regular vine. Repeated subtrees represent the same lower-tree cluster.

• empty {d : ℕ} : Tree d
• leaf {d : ℕ} (i : Fin d) : Tree d
• join {d : ℕ} (a b : Fin d) (conditioning : Finset (Fin d)) (left right : Tree d) : Tree d

@[instance_reducible]

instance ProbabilityTheory.Copula.Vine.instDecidableEqTree {d✝ : ℕ} : DecidableEq (Tree d✝)

Equations

• ProbabilityTheory.Copula.Vine.instDecidableEqTree = ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq

def ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq {d✝ : ℕ} (x✝ x✝¹ : Tree d✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq ProbabilityTheory.Copula.Vine.Tree.empty ProbabilityTheory.Copula.Vine.Tree.empty = isTrue ⋯
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq ProbabilityTheory.Copula.Vine.Tree.empty (ProbabilityTheory.Copula.Vine.Tree.leaf i) = isFalse ⋯
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq ProbabilityTheory.Copula.Vine.Tree.empty (ProbabilityTheory.Copula.Vine.Tree.join a b conditioning left right) = isFalse ⋯
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq (ProbabilityTheory.Copula.Vine.Tree.leaf i) ProbabilityTheory.Copula.Vine.Tree.empty = isFalse ⋯
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq (ProbabilityTheory.Copula.Vine.Tree.leaf a) (ProbabilityTheory.Copula.Vine.Tree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq (ProbabilityTheory.Copula.Vine.Tree.leaf i) (ProbabilityTheory.Copula.Vine.Tree.join a b conditioning left right) = isFalse ⋯
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq (ProbabilityTheory.Copula.Vine.Tree.join a b conditioning left right) ProbabilityTheory.Copula.Vine.Tree.empty = isFalse ⋯
• ProbabilityTheory.Copula.Vine.instDecidableEqTree.decEq (ProbabilityTheory.Copula.Vine.Tree.join a b conditioning left right) (ProbabilityTheory.Copula.Vine.Tree.leaf i) = isFalse ⋯

def ProbabilityTheory.Copula.Vine.Tree.vars {d : ℕ} : Tree d → Finset (Fin d)

Coordinates of a cluster.

Equations

• ProbabilityTheory.Copula.Vine.Tree.empty.vars = ∅
• (ProbabilityTheory.Copula.Vine.Tree.leaf i).vars = {i}
• (ProbabilityTheory.Copula.Vine.Tree.join a b s left right).vars = insert a (insert b s)

def ProbabilityTheory.Copula.Vine.Tree.Child {d : ℕ} (q : Tree d) : Tree d → Prop

An immediate parent in the preceding tree.

Equations

• q.Child (ProbabilityTheory.Copula.Vine.Tree.join a b conditioning l r) = (q = l ∨ q = r)
• q.Child x✝ = False

def ProbabilityTheory.Copula.Vine.Tree.Proximity {d : ℕ} (l r : Tree d) (s : Finset (Fin d)) : Prop

The usual shared-parent proximity condition, with the first tree as base case.

Equations

• One or more equations did not get rendered due to their size.

inductive ProbabilityTheory.Copula.Vine.Tree.Valid {d : ℕ} : Tree d → Prop

Well-formed recursive regular-vine clusters.

• empty {d : ℕ} : Tree.empty.Valid
• leaf {d : ℕ} (i : Fin d) : (Tree.leaf i).Valid
• join {d : ℕ} {a b : Fin d} {s : Finset (Fin d)} {l r : Tree d} (left : l.Valid) (right : r.Valid) (left_vars : l.vars = insert a s) (right_vars : r.vars = insert b s) (left_notMem : a ∉ s) (right_notMem : b ∉ s) (distinct : a ≠ b) (proximity : l.Proximity r s) : (Tree.join a b s l r).Valid

theorem ProbabilityTheory.Copula.Vine.Tree.valid_join_iff {d : ℕ} {a b : Fin d} {s : Finset (Fin d)} {l r : Tree d} : (join a b s l r).Valid ↔ l.Valid ∧ r.Valid ∧ l.vars = insert a s ∧ r.vars = insert b s ∧ a ∉ s ∧ b ∉ s ∧ a ≠ b ∧ l.Proximity r s

def ProbabilityTheory.Copula.Vine.Tree.graft {d : ℕ} : Tree d → Fin d → List Bool → Tree d

Attach a fresh variable along a path (false = left, true = right). Missing choices default to left; choices after reaching a leaf are unused.

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.Vine.Tree.empty.graft x✝¹ x✝ = ProbabilityTheory.Copula.Vine.Tree.leaf x✝¹

theorem ProbabilityTheory.Copula.Vine.Tree.vars_graft {d : ℕ} {t : Tree d} (ht : t.Valid) (a : Fin d) (path : List Bool) : (t.graft a path).vars = insert a t.vars

theorem ProbabilityTheory.Copula.Vine.Tree.child_graft {d : ℕ} {t : Tree d} (ht : t ≠ empty) (a : Fin d) (path : List Bool) : t.Child (t.graft a path)

theorem ProbabilityTheory.Copula.Vine.Tree.Valid.graft {d : ℕ} {t : Tree d} (ht : t.Valid) (a : Fin d) (ha : a ∉ t.vars) (path : List Bool) : (t.graft a path).Valid

Path attachment preserves regularity and the proximity condition.

def ProbabilityTheory.Copula.Vine.Tree.ofList {d : ℕ} (paths : Fin d → List Bool) : List (Fin d) → Tree d

Build a vine by adding a list of distinct variables from right to left.

Equations

• ProbabilityTheory.Copula.Vine.Tree.ofList paths [] = ProbabilityTheory.Copula.Vine.Tree.empty
• ProbabilityTheory.Copula.Vine.Tree.ofList paths (a :: xs) = (ProbabilityTheory.Copula.Vine.Tree.ofList paths xs).graft a (paths a)

theorem ProbabilityTheory.Copula.Vine.Tree.valid_ofList {d : ℕ} (paths : Fin d → List Bool) (xs : List (Fin d)) : xs.Nodup → (ofList paths xs).Valid ∧ (ofList paths xs).vars = xs.toFinset

def ProbabilityTheory.Copula.Vine.Tree.edges {d : ℕ} : Tree d → Finset (Fin d × Fin d × Finset (Fin d))

All labelled pair-copula edges; duplicate ancestral references are removed.

Equations

• ProbabilityTheory.Copula.Vine.Tree.empty.edges = ∅
• (ProbabilityTheory.Copula.Vine.Tree.leaf i).edges = ∅
• (ProbabilityTheory.Copula.Vine.Tree.join a b s left right).edges = insert (a, b, s) (left.edges ∪ right.edges)

structure ProbabilityTheory.Copula.RVineStructure (d : ℕ) : Type

A regular-vine structure in path-attachment form. The list is an elimination order: construction adds its variables from right to left.

• eliminationOrder : List (Fin d)

  Each coordinate occurs exactly once.

• nodup : self.eliminationOrder.Nodup
• complete : self.eliminationOrder.toFinset = Finset.univ
• paths : Fin d → List Bool

  Left/right choices for attaching a variable to the earlier clusters.

def ProbabilityTheory.Copula.RVineStructure.ofOrder {d : ℕ} (order : Equiv.Perm (Fin d)) (paths : Fin d → List Bool) : RVineStructure d

Specify the order in which variables are added, together with their attachment paths.

Equations

• ProbabilityTheory.Copula.RVineStructure.ofOrder order paths = { eliminationOrder := (List.ofFn ⇑order).reverse, nodup := ⋯, complete := ⋯, paths := paths }

def ProbabilityTheory.Copula.RVineStructure.cVine {d : ℕ} (order : Equiv.Perm (Fin d)) : RVineStructure d

The C-vine with the given root order.

Equations

• ProbabilityTheory.Copula.RVineStructure.cVine order = ProbabilityTheory.Copula.RVineStructure.ofOrder order fun (x : Fin d) => []

def ProbabilityTheory.Copula.RVineStructure.dVine {d : ℕ} (order : Equiv.Perm (Fin d)) : RVineStructure d

The D-vine with the given chain order.

Equations

• ProbabilityTheory.Copula.RVineStructure.dVine order = ProbabilityTheory.Copula.RVineStructure.ofOrder order fun (x : Fin d) => List.replicate d true

def ProbabilityTheory.Copula.RVineStructure.toTree {d : ℕ} (S : RVineStructure d) : Vine.Tree d

The labelled ancestral tree, including all conditioned and conditioning sets.

Equations

• S.toTree = ProbabilityTheory.Copula.Vine.Tree.ofList S.paths S.eliminationOrder

theorem ProbabilityTheory.Copula.RVineStructure.valid {d : ℕ} (S : RVineStructure d) : S.toTree.Valid

Every structure produced by the API satisfies the recursive proximity condition.

@[simp]

theorem ProbabilityTheory.Copula.RVineStructure.vars_toTree {d : ℕ} (S : RVineStructure d) : S.toTree.vars = Finset.univ

def ProbabilityTheory.Copula.RVineStructure.edges {d : ℕ} (S : RVineStructure d) : Finset (Fin d × Fin d × Finset (Fin d))

The distinct pair-copula edges (a, b, conditioningSet).

Equations

• S.edges = S.toTree.edges

def ProbabilityTheory.Copula.RVineStructure.firstTree {d : ℕ} (S : RVineStructure d) : Finset (Fin d × Fin d)

First-tree edges, with empty conditioning sets.

Equations

• S.firstTree = Finset.image (fun (e : Fin d × Fin d × Finset (Fin d)) => (e.1, e.2.1)) ({e ∈ S.edges | e.2.2 = ∅})