← Copula mathematical handbook

Conditional pair-copula gluing

Glue the laws of (a, S) and (b, S) over their common S marginal using a measurable family of pair copulas. Both input laws are preserved, without assuming densities or continuous conditional distributions.

structure ProbabilityTheory.Copula.Vine.Overlap {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) : Prop

The compatibility conditions for two marginals sharing a conditioning set.

• left_set : l = insert a s
• right_set : r = insert b s
• left_notMem : a ∉ s
• right_notMem : b ∉ s
• distinct : a ≠ b
• left_map : MeasureTheory.Measure.map (project s) L.toMeasure = D.toMeasure
• right_map : MeasureTheory.Measure.map (project s) R.toMeasure = D.toMeasure

noncomputable def ProbabilityTheory.Copula.Vine.glueMap {d : ℕ} {l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (s : Finset (Fin d)) (a b : Fin d) (p : (Fin d → ↑unitInterval) × (Fin 2 → ↑unitInterval)) (i : Fin d) : ↑unitInterval

Insert the two conditional quantiles into their shared conditioning vector.

Equations

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

theorem ProbabilityTheory.Copula.Vine.measurable_glueMap {d : ℕ} {l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (s : Finset (Fin d)) (a b : Fin d) : Measurable (glueMap L R s a b)

noncomputable def ProbabilityTheory.Copula.Vine.glueProbability {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) : MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval)

The probability law obtained by conditional pair-copula gluing.

Equations

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

theorem ProbabilityTheory.Copula.Vine.toMeasure_glueProbability {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) : ↑(glueProbability L R D a b F) = MeasureTheory.Measure.map (glueMap L R s a b) (D.toMeasure.compProd (F.comap (project s) ⋯).kernel)

theorem ProbabilityTheory.Copula.Vine.glueProbability_apply {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) {A : Set (Fin d → ↑unitInterval)} (hA : MeasurableSet A) : ↑(glueProbability L R D a b F) A = ∫⁻ (x : Fin d → ↑unitInterval), (F.kernel (project s x)) {z : Fin 2 → ↑unitInterval | glueMap L R s a b (x, z) ∈ A} ∂D.toMeasure

Event probabilities for a non-simplified pair-copula join. The pair family is evaluated at the actual shared coordinates, not averaged in advance.

theorem ProbabilityTheory.Copula.Vine.glueProbability_empty {d : ℕ} {l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (a b : Fin d) (ha : a ∈ l) (hb : b ∈ r) (F : Family (Fin d → ↑unitInterval) 2) : ↑(glueProbability L R Marginal.empty a b F) = MeasureTheory.Measure.map (fun (z : Fin 2 → ↑unitInterval) (i : Fin d) => if i = a then z 0 else if i = b then z 1 else 0) (F.copula fun (x : Fin d) => 0).toMeasure

With no conditioning coordinates, gluing inserts the supplied pair law directly into the two active coordinates.

theorem ProbabilityTheory.Copula.Vine.map_glueProbability_empty_pair {d : ℕ} {l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (a b : Fin d) (ha : a ∈ l) (hb : b ∈ r) (hab : a ≠ b) (F : Family (Fin d → ↑unitInterval) 2) : MeasureTheory.Measure.map (fun (x : Fin d → ↑unitInterval) => ![x a, x b]) ↑(glueProbability L R Marginal.empty a b F) = (F.copula fun (x : Fin d) => 0).toMeasure

Projecting an unconditional join onto its ordered endpoints recovers the input pair copula, including singular copulas.

theorem ProbabilityTheory.Copula.Vine.map_glue_left {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) (h : Overlap L R D a b) : MeasureTheory.Measure.map (project l) ↑(glueProbability L R D a b F) = L.toMeasure

theorem ProbabilityTheory.Copula.Vine.map_glue_right {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) (h : Overlap L R D a b) : MeasureTheory.Measure.map (project r) ↑(glueProbability L R D a b F) = R.toMeasure

noncomputable def ProbabilityTheory.Copula.Vine.glue {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) (h : Overlap L R D a b) : Marginal (insert a (insert b s))

Join compatible marginal copulas through a possibly non-simplified pair family.

Equations

• ProbabilityTheory.Copula.Vine.glue L R D a b F h = { measure := ProbabilityTheory.Copula.Vine.glueProbability L R D a b F, uniform := ⋯, supported := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.Vine.map_glue_project_left {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) (h : Overlap L R D a b) : MeasureTheory.Measure.map (project l) (glue L R D a b F h).toMeasure = L.toMeasure

@[simp]

theorem ProbabilityTheory.Copula.Vine.map_glue_project_right {d : ℕ} {s l r : Finset (Fin d)} (L : Marginal l) (R : Marginal r) (D : Marginal s) (a b : Fin d) (F : Family (Fin d → ↑unitInterval) 2) (h : Overlap L R D a b) : MeasureTheory.Measure.map (project r) (glue L R D a b F h).toMeasure = R.toMeasure