← Copula mathematical handbook

Copula laws on coordinate subsets

Coordinates outside the active subset are padded by zero. This gives all intermediate vine marginals the same ambient measurable space.

def ProbabilityTheory.Copula.Vine.project {d : ℕ} (s : Finset (Fin d)) (x : Fin d → ↑unitInterval) (i : Fin d) : ↑unitInterval

Retain the coordinates in s and set the others to zero.

Equations

• ProbabilityTheory.Copula.Vine.project s x i = if i ∈ s then x i else 0

theorem ProbabilityTheory.Copula.Vine.measurable_project {d : ℕ} (s : Finset (Fin d)) : Measurable (project s)

theorem ProbabilityTheory.Copula.Vine.project_project {d : ℕ} {s t : Finset (Fin d)} (h : s ⊆ t) (x : Fin d → ↑unitInterval) : project s (project t x) = project s x

structure ProbabilityTheory.Copula.Vine.Marginal {d : ℕ} (s : Finset (Fin d)) : Type

A copula on an active coordinate subset, padded by zeros elsewhere.

• measure : MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval)

  The ambient probability law.

• uniform (i : Fin d) (hi : i ∈ s) : MeasureTheory.Measure.map (fun (x : Fin d → ↑unitInterval) => x i) ↑self.measure = MeasureTheory.volume

  Active coordinate laws are uniform.

• supported : ∀ᵐ (x : Fin d → ↑unitInterval) ∂↑self.measure, project s x = x

  Inactive coordinates are zero almost surely.

def ProbabilityTheory.Copula.Vine.Marginal.toMeasure {d : ℕ} {s : Finset (Fin d)} (M : Marginal s) : MeasureTheory.Measure (Fin d → ↑unitInterval)

The underlying probability measure.

Equations

• M.toMeasure = ↑M.measure

instance ProbabilityTheory.Copula.Vine.Marginal.instIsProbabilityMeasureForallFinElemRealUnitIntervalToMeasure {d : ℕ} {s : Finset (Fin d)} (M : Marginal s) : MeasureTheory.IsProbabilityMeasure M.toMeasure

theorem ProbabilityTheory.Copula.Vine.Marginal.ext {d : ℕ} {s : Finset (Fin d)} {L R : Marginal s} (h : L.toMeasure = R.toMeasure) : L = R

theorem ProbabilityTheory.Copula.Vine.Marginal.ext_iff {d : ℕ} {s : Finset (Fin d)} {L R : Marginal s} : L = R ↔ L.toMeasure = R.toMeasure

@[simp]

theorem ProbabilityTheory.Copula.Vine.Marginal.map_project_self {d : ℕ} {s : Finset (Fin d)} (M : Marginal s) : MeasureTheory.Measure.map (project s) M.toMeasure = M.toMeasure

noncomputable def ProbabilityTheory.Copula.Vine.Marginal.restrict {d : ℕ} {s t : Finset (Fin d)} (M : Marginal t) (h : s ⊆ t) : Marginal s

Restrict a marginal to a smaller coordinate subset.

Equations

• M.restrict h = { measure := M.measure.map (ProbabilityTheory.Copula.Vine.project s), uniform := ⋯, supported := ⋯ }

noncomputable def ProbabilityTheory.Copula.Vine.Marginal.empty {d : ℕ} : Marginal ∅

The empty marginal is a point mass at the zero vector.

Equations

• ProbabilityTheory.Copula.Vine.Marginal.empty = { measure := ⟨MeasureTheory.Measure.dirac fun (x : Fin d) => 0, ⋯⟩, uniform := ⋯, supported := ⋯ }

def ProbabilityTheory.Copula.Vine.Marginal.ofCopula {d : ℕ} (C : Copula d) : Marginal Finset.univ

Regard an ordinary copula as a marginal on all coordinates.

Equations

• ProbabilityTheory.Copula.Vine.Marginal.ofCopula C = { measure := C.measure, uniform := ⋯, supported := ⋯ }

noncomputable def ProbabilityTheory.Copula.Vine.Marginal.singleton {d : ℕ} (i : Fin d) : Marginal {i}

A uniform single coordinate, padded by zeros.

Equations

• ProbabilityTheory.Copula.Vine.Marginal.singleton i = (ProbabilityTheory.Copula.Vine.Marginal.ofCopula (ProbabilityTheory.Copula.independence d)).restrict ⋯

def ProbabilityTheory.Copula.Vine.Marginal.toCopula {d : ℕ} (M : Marginal Finset.univ) : Copula d

Convert a full-coordinate marginal to the library's copula type.

Equations

• M.toCopula = { measure := M.measure, marginal_eq := ⋯ }

def ProbabilityTheory.Copula.Vine.Marginal.cast {d : ℕ} {s t : Finset (Fin d)} (M : Marginal s) (h : s = t) : Marginal t

Transport a marginal along equality of its active sets.

Equations

• M.cast h = h ▸ M

@[simp]

theorem ProbabilityTheory.Copula.Vine.Marginal.toMeasure_cast {d : ℕ} {s t : Finset (Fin d)} (M : Marginal s) (h : s = t) : (M.cast h).toMeasure = M.toMeasure

theorem ProbabilityTheory.Copula.Vine.Marginal.map_empty {d : ℕ} {s : Finset (Fin d)} (M : Marginal s) : MeasureTheory.Measure.map (project ∅) M.toMeasure = empty.toMeasure

theorem ProbabilityTheory.Copula.Vine.Marginal.toMeasure_eq_uniform_singleton {d : ℕ} (i : Fin d) (M : Marginal {i}) : M.toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => project {i} fun (x : Fin d) => u) MeasureTheory.volume

instance ProbabilityTheory.Copula.Vine.Marginal.instSubsingletonSingletonFinFinset {d : ℕ} (i : Fin d) : Subsingleton (Marginal {i})

def ProbabilityTheory.Copula.Vine.insertCoordinate {d : ℕ} (s : Finset (Fin d)) (a : Fin d) (p : (Fin d → ↑unitInterval) × ↑unitInterval) (i : Fin d) : ↑unitInterval

Reinsert one conditioned coordinate into a padded conditioning vector.

Equations

• ProbabilityTheory.Copula.Vine.insertCoordinate s a p i = if i = a then p.2 else ProbabilityTheory.Copula.Vine.project s p.1 i

theorem ProbabilityTheory.Copula.Vine.measurable_insertCoordinate {d : ℕ} (s : Finset (Fin d)) (a : Fin d) : Measurable (insertCoordinate s a)

noncomputable def ProbabilityTheory.Copula.Vine.coordinateKernel {d : ℕ} {t : Finset (Fin d)} (M : Marginal t) (s : Finset (Fin d)) (a : Fin d) : Kernel (Fin d → ↑unitInterval) ↑unitInterval

The conditional distribution of a coordinate given a retained subset.

Equations

• ProbabilityTheory.Copula.Vine.coordinateKernel M s a = ProbabilityTheory.condDistrib (fun (x : Fin d → ↑unitInterval) => x a) (ProbabilityTheory.Copula.Vine.project s) M.toMeasure

instance ProbabilityTheory.Copula.Vine.instIsMarkovKernelForallFinElemRealUnitIntervalCoordinateKernel {d : ℕ} {t : Finset (Fin d)} (M : Marginal t) (s : Finset (Fin d)) (a : Fin d) : IsMarkovKernel (coordinateKernel M s a)

theorem ProbabilityTheory.Copula.Vine.coordinateKernel_empty {d : ℕ} {t : Finset (Fin d)} (M : Marginal t) (a : Fin d) (ha : a ∈ t) : ((coordinateKernel M ∅ a) fun (x : Fin d) => 0) = MeasureTheory.volume

Conditioning on the empty coordinate set leaves an active coordinate uniform.

@[simp]

theorem ProbabilityTheory.Copula.Vine.unitQuantile_volume (u : ↑unitInterval) : unitQuantile MeasureTheory.volume u = u

theorem ProbabilityTheory.Copula.Vine.map_insertCoordinate_disintegration {d : ℕ} {t s : Finset (Fin d)} (M : Marginal t) (a : Fin d) (ht : t = insert a s) : MeasureTheory.Measure.map (insertCoordinate s a) ((MeasureTheory.Measure.map (project s) M.toMeasure).compProd (coordinateKernel M s a)) = M.toMeasure

Disintegrating and reinserting a coordinate recovers its entire marginal law.