← Copula mathematical handbook

Regular-vine copula construction

Each path attachment preserves the entire previous copula. At every new edge the supplied family couples the two conditional coordinate laws over their shared marginal. Measurability is explicit; the family can depend on all of the conditioning coordinates. Singular conditional laws are allowed.

@[reducible, inline]

abbrev ProbabilityTheory.Copula.Vine.PairFamilies (d : ℕ) : Type

A pair-copula family for each oriented pair and conditioning set. Only the entries belonging to the chosen vine are used. Each family is evaluated on the conditioning vector padded by zero outside its conditioning set.

Equations

• ProbabilityTheory.Copula.Vine.PairFamilies d = (Fin d → Fin d → Finset (Fin d) → ProbabilityTheory.Copula.Family (Fin d → ↑unitInterval) 2)

inductive ProbabilityTheory.Copula.Vine.Realization {d : ℕ} (t : Tree d) : Marginal t.vars → Type

A realization records the marginal law at every ancestral cluster and proves that each cluster projects to its two immediate parents.

• empty {d : ℕ} : Realization Tree.empty Marginal.empty
• leaf {d : ℕ} (i : Fin d) : Realization (Tree.leaf i) (Marginal.singleton i)
• join {d : ℕ} {a b : Fin d} {s : Finset (Fin d)} {l r : Tree d} {L : Marginal l.vars} {R : Marginal r.vars} (left : Realization l L) (right : Realization r R) (M : Marginal (insert a (insert b s))) (left_map : MeasureTheory.Measure.map (project l.vars) M.toMeasure = L.toMeasure) (right_map : MeasureTheory.Measure.map (project r.vars) M.toMeasure = R.toMeasure) : Realization (Tree.join a b s l r) M

structure ProbabilityTheory.Copula.Vine.Extension {d : ℕ} {t : Tree d} (M : Marginal t.vars) (a : Fin d) (path : List Bool) : Type

The result of adding one variable: its law, its ancestral marginals, and the proof that the previous law is preserved.

• law : Marginal (t.graft a path).vars
• realization : Realization (t.graft a path) self.law
• marginal : MeasureTheory.Measure.map (project t.vars) self.law.toMeasure = M.toMeasure

noncomputable def ProbabilityTheory.Copula.Vine.Realization.graft {d : ℕ} {t : Tree d} {M : Marginal t.vars} (model : Realization t M) (ht : t.Valid) (a : Fin d) (ha : a ∉ t.vars) (path : List Bool) (families : PairFamilies d) : Extension M a path

Build a path attachment, using a conditional copula at each newly introduced edge.

Equations

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

structure ProbabilityTheory.Copula.Vine.Model {d : ℕ} (t : Tree d) : Type

A law together with its ancestral marginal identities.

• law : Marginal t.vars
• realization : Realization t self.law

noncomputable def ProbabilityTheory.Copula.Vine.modelOfList {d : ℕ} (paths : Fin d → List Bool) (families : PairFamilies d) (xs : List (Fin d)) : xs.Nodup → Model (Tree.ofList paths xs)

Construct the probability laws for an ordered list of distinct variables.

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.Vine.modelOfList paths families [] x_2 = { law := ProbabilityTheory.Copula.Vine.Marginal.empty, realization := ProbabilityTheory.Copula.Vine.Realization.empty }

theorem ProbabilityTheory.Copula.Vine.modelOfList_cons_marginal {d : ℕ} (paths : Fin d → List Bool) (families : PairFamilies d) (a : Fin d) (xs : List (Fin d)) (h : (a :: xs).Nodup) : MeasureTheory.Measure.map (project (Tree.ofList paths xs).vars) (modelOfList paths families (a :: xs) h).law.toMeasure = (modelOfList paths families xs ⋯).law.toMeasure

Adding a variable preserves the complete joint law of all previously added variables.

noncomputable def ProbabilityTheory.Copula.RVineStructure.model {d : ℕ} (S : RVineStructure d) (families : Vine.PairFamilies d) : Vine.Model S.toTree

The compatible probability law at every ancestral node of this vine.

Equations

• S.model families = ProbabilityTheory.Copula.Vine.modelOfList S.paths families S.eliminationOrder ⋯

noncomputable def ProbabilityTheory.Copula.RVineStructure.toCopula {d : ℕ} (S : RVineStructure d) (families : Vine.PairFamilies d) : Copula d

Construct a regular-vine copula from measurable, possibly conditioning-dependent pair-copula families. Uniform marginals follow from conditional gluing.

Equations

• S.toCopula families = ((S.model families).law.cast ⋯).toCopula

theorem ProbabilityTheory.Copula.RVineStructure.toMeasure_toCopula {d : ℕ} (S : RVineStructure d) (families : Vine.PairFamilies d) : (S.toCopula families).toMeasure = (S.model families).law.toMeasure

The full copula law is the law at the top of the vine.

noncomputable def ProbabilityTheory.Copula.RVineStructure.simplified {d : ℕ} (S : RVineStructure d) (pairs : Fin d → Fin d → Finset (Fin d) → Copula 2) : Copula d

A simplified regular vine, with a fixed copula at each edge.

Equations

• S.simplified pairs = S.toCopula fun (a b : Fin d) (s : Finset (Fin d)) => ProbabilityTheory.Copula.Family.const (pairs a b s)

noncomputable def ProbabilityTheory.Copula.cVine {d : ℕ} (order : Equiv.Perm (Fin d)) (families : Vine.PairFamilies d) : Copula d

A possibly non-simplified C-vine with a prescribed variable order.

Equations

• ProbabilityTheory.Copula.cVine order families = (ProbabilityTheory.Copula.RVineStructure.cVine order).toCopula families

noncomputable def ProbabilityTheory.Copula.dVine {d : ℕ} (order : Equiv.Perm (Fin d)) (families : Vine.PairFamilies d) : Copula d

A possibly non-simplified D-vine with a prescribed variable order.

Equations

• ProbabilityTheory.Copula.dVine order families = (ProbabilityTheory.Copula.RVineStructure.dVine order).toCopula families