← Copula mathematical handbook

CDF recursion and independence for simplified C-vines

theorem ProbabilityTheory.Copula.measure_vineStep_Iic {d : ℕ} (pairs : Fin d → Copula 2) (D : Copula d) (u : Fin (d + 1) → ↑unitInterval) : (vineStep pairs D).toMeasure (Set.Iic u) = ∫⁻ (r : ↑unitInterval) in Set.Iic (u 0), D.toMeasure (Set.Iic fun (i : Fin d) => (pairs i).conditionalCDFUnit r (u i.succ))

The lower-orthant probability of a C-vine step.

theorem ProbabilityTheory.Copula.cdf_vineStep {d : ℕ} (pairs : Fin d → Copula 2) (D : Copula d) (u : Fin (d + 1) → ↑unitInterval) : (vineStep pairs D).cdf u = ∫ (r : ↑unitInterval) in Set.Iic (u 0), D.cdf fun (i : Fin d) => (pairs i).conditionalCDFUnit r (u i.succ)

The usual recursive C-vine CDF formula, valid also for singular pair copulas.

theorem ProbabilityTheory.Copula.cdf_vineStep_independence {d : ℕ} (D : Copula d) (u : Fin (d + 1) → ↑unitInterval) : (vineStep (fun (x : Fin d) => independence 2) D).cdf u = ↑(u 0) * D.cdf fun (i : Fin d) => u i.succ

With independent root-pair copulas, the root is independent of the residual copula.

@[simp]

theorem ProbabilityTheory.Copula.vineStep_independence (d : ℕ) : vineStep (fun (x : Fin d) => independence 2) (independence d) = independence (d + 1)

noncomputable def ProbabilityTheory.Copula.CVine.independent (d : ℕ) : CVine d

The vine whose pair copulas are all independent.

Equations

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

@[simp]

theorem ProbabilityTheory.Copula.CVine.toCopula_independent (d : ℕ) : (independent d).toCopula = independence d

theorem ProbabilityTheory.Copula.CVine.cdf_triple (A B D : Copula 2) (u v w : ↑unitInterval) : (triple A B D).toCopula.cdf ![u, v, w] = ∫ (r : ↑unitInterval) in Set.Iic u, D.cdf ![A.conditionalCDFUnit r v, B.conditionalCDFUnit r w]

Explicit three-variable pair-copula CDF formula.