← Copula mathematical handbook

Simplified C-vine copulas

One construction step adjoins an independent uniform root to a residual copula, then applies the conditional quantile of each root-pair copula to its residual coordinate. Iterating this step gives a simplified C-vine in any finite dimension. The recursive residual copula is fixed, independent of the value of the root.

noncomputable def ProbabilityTheory.Copula.Vine.rootTransform {d : ℕ} (pairs : Fin d → Copula 2) (p : ↑unitInterval × (Fin d → ↑unitInterval)) : Fin (d + 1) → ↑unitInterval

The inverse conditional transform for one level of a C-vine.

Equations

• ProbabilityTheory.Copula.Vine.rootTransform pairs p = Fin.cons p.1 fun (i : Fin d) => (pairs i).conditionalQuantile p.1 (p.2 i)

theorem ProbabilityTheory.Copula.Vine.measurable_rootTransform {d : ℕ} (pairs : Fin d → Copula 2) : Measurable (rootTransform pairs)

theorem ProbabilityTheory.Copula.Vine.map_root_coordinate {d : ℕ} (D : Copula d) (i : Fin d) : MeasureTheory.Measure.map (fun (p : ↑unitInterval × (Fin d → ↑unitInterval)) => (p.1, p.2 i)) (MeasureTheory.volume.prod D.toMeasure) = MeasureTheory.volume.prod MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.vineStep {d : ℕ} (pairs : Fin d → Copula 2) (D : Copula d) : Copula (d + 1)

Adjoin a root with the prescribed bivariate copulas to a residual copula. The residual dependence is independent of the root (the simplifying assumption).

Equations

• ProbabilityTheory.Copula.vineStep pairs D = ProbabilityTheory.Copula.ofMap ⟨MeasureTheory.volume.prod D.toMeasure, ⋯⟩ (ProbabilityTheory.Copula.Vine.rootTransform pairs) ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_vineStep {d : ℕ} (pairs : Fin d → Copula 2) (D : Copula d) : (vineStep pairs D).toMeasure = MeasureTheory.Measure.map (Vine.rootTransform pairs) (MeasureTheory.volume.prod D.toMeasure)

@[simp]

theorem ProbabilityTheory.Copula.reindex_vineStep_root_pair {d : ℕ} (pairs : Fin d → Copula 2) (D : Copula d) (i : Fin d) : (vineStep pairs D).reindex ![0, i.succ] = pairs i

Each first-tree pair is exactly the bivariate copula supplied by the caller.

inductive ProbabilityTheory.Copula.CVine : ℕ → Type

A simplified C-vine, with roots ordered 0, 1, …. At each level the pair copulas describe the remaining coordinates conditional on all earlier roots. There are d * (d - 1) / 2 bivariate inputs in dimension d.

• nil : CVine 0

  The empty vine.

• cons {d : ℕ} (pairs : Fin d → Copula 2) (tail : CVine d) : CVine (d + 1)

  Add the next root and its pair copulas.

noncomputable def ProbabilityTheory.Copula.CVine.toCopula {d : ℕ} : CVine d → Copula d

The copula represented by a simplified C-vine.

Equations

• ProbabilityTheory.Copula.CVine.nil.toCopula = ProbabilityTheory.Copula.independence 0
• (ProbabilityTheory.Copula.CVine.cons pairs tail).toCopula = ProbabilityTheory.Copula.vineStep pairs tail.toCopula

@[simp]

theorem ProbabilityTheory.Copula.CVine.toCopula_nil : nil.toCopula = independence 0

@[simp]

theorem ProbabilityTheory.Copula.CVine.toCopula_cons {d : ℕ} (pairs : Fin d → Copula 2) (tail : CVine d) : (cons pairs tail).toCopula = vineStep pairs tail.toCopula

def ProbabilityTheory.Copula.CVine.singleton : CVine 1

A one-dimensional vine has no pair-copula inputs.

Equations

• ProbabilityTheory.Copula.CVine.singleton = ProbabilityTheory.Copula.CVine.cons Fin.elim0 ProbabilityTheory.Copula.CVine.nil

@[simp]

theorem ProbabilityTheory.Copula.CVine.toCopula_singleton : singleton.toCopula = independence 1

def ProbabilityTheory.Copula.CVine.ofPairs (d : ℕ) : ((i j : Fin d) → i < j → Copula 2) → CVine d

Construct a C-vine from its strict upper triangular table of pair copulas. The entry (i, j) is the pair of coordinates i and j conditional on coordinates 0, …, i - 1. Entries below the diagonal are not required.

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.CVine.ofPairs 0 x_2 = ProbabilityTheory.Copula.CVine.nil

@[simp]

theorem ProbabilityTheory.Copula.CVine.reindex_ofPairs_root_pair {d : ℕ} (pairs : (i j : Fin (d + 1)) → i < j → Copula 2) (j : Fin d) : (ofPairs (d + 1) pairs).toCopula.reindex ![0, j.succ] = pairs 0 j.succ ⋯

The first row of the triangular table gives the root's bivariate marginals.

def ProbabilityTheory.Copula.CVine.pair (C : Copula 2) : CVine 2

A bivariate vine consists of its single pair copula.

Equations

• ProbabilityTheory.Copula.CVine.pair C = ProbabilityTheory.Copula.CVine.cons (fun (x : Fin 1) => C) ProbabilityTheory.Copula.CVine.singleton

@[simp]

theorem ProbabilityTheory.Copula.CVine.toCopula_pair (C : Copula 2) : (pair C).toCopula = C

def ProbabilityTheory.Copula.CVine.triple (C₀₁ C₀₂ C₁₂₀ : Copula 2) : CVine 3

A three-variable vine with pairs C₀₁, C₀₂ and conditional pair C₁₂;₀.

Equations

• ProbabilityTheory.Copula.CVine.triple C₀₁ C₀₂ C₁₂₀ = ProbabilityTheory.Copula.CVine.cons ![C₀₁, C₀₂] (ProbabilityTheory.Copula.CVine.pair C₁₂₀)

@[simp]

theorem ProbabilityTheory.Copula.CVine.toCopula_triple (C₀₁ C₀₂ C₁₂₀ : Copula 2) : (triple C₀₁ C₀₂ C₁₂₀).toCopula = vineStep ![C₀₁, C₀₂] C₁₂₀