← Copula mathematical handbook

Copulas as probability measures

A copula is a probability measure on a finite power of the unit interval with uniform coordinate marginals. Dimension zero is allowed. The usual copula distribution function is derived in Copula.CDF.

structure ProbabilityTheory.Copula (d : ℕ) : Type

A d-dimensional copula, represented by a probability measure on [0, 1]^d whose coordinate marginals are the canonical uniform probability measure.

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

  The probability measure underlying the copula.

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

  Every coordinate has the uniform distribution on the unit interval.

def ProbabilityTheory.Copula.toMeasure {d : ℕ} (C : Copula d) : MeasureTheory.Measure (Fin d → ↑unitInterval)

The underlying measure, for use with mathlib's measure-theoretic API.

Equations

• C.toMeasure = ↑C.measure

instance ProbabilityTheory.Copula.instIsProbabilityMeasureForallFinElemRealUnitIntervalToMeasure {d : ℕ} (C : Copula d) : MeasureTheory.IsProbabilityMeasure C.toMeasure

theorem ProbabilityTheory.Copula.ext {d : ℕ} {C D : Copula d} (h : C.toMeasure = D.toMeasure) : C = D

theorem ProbabilityTheory.Copula.ext_iff {d : ℕ} {C D : Copula d} : C = D ↔ C.toMeasure = D.toMeasure

theorem ProbabilityTheory.Copula.toMeasure_injective {d : ℕ} : Function.Injective toMeasure

@[simp]

theorem ProbabilityTheory.Copula.map_eval {d : ℕ} (C : Copula d) (i : Fin d) : MeasureTheory.Measure.map (fun (x : Fin d → ↑unitInterval) => x i) C.toMeasure = MeasureTheory.volume

theorem ProbabilityTheory.Copula.measurePreserving_eval {d : ℕ} (C : Copula d) (i : Fin d) : MeasureTheory.MeasurePreserving (fun (x : Fin d → ↑unitInterval) => x i) C.toMeasure MeasureTheory.volume

Coordinate projections preserve the uniform measure.

theorem ProbabilityTheory.Copula.measure_preimage_eval {d : ℕ} (C : Copula d) (i : Fin d) {s : Set ↑unitInterval} (hs : MeasurableSet s) : C.toMeasure ((fun (x : Fin d → ↑unitInterval) => x i) ⁻¹' s) = MeasureTheory.volume s

The probability of a measurable coordinate event is its uniform volume.

@[simp]

theorem ProbabilityTheory.Copula.measure_eval_le {d : ℕ} (C : Copula d) (i : Fin d) (u : ↑unitInterval) : C.toMeasure {x : Fin d → ↑unitInterval | x i ≤ u} = ENNReal.ofReal ↑u

@[simp]

theorem ProbabilityTheory.Copula.measureReal_eval_le {d : ℕ} (C : Copula d) (i : Fin d) (u : ↑unitInterval) : C.toMeasure.real {x : Fin d → ↑unitInterval | x i ≤ u} = ↑u

noncomputable def ProbabilityTheory.Copula.ofMap {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (X : Ω → Fin d → ↑unitInterval) (hX : Measurable X) (hmarg : ∀ (i : Fin d), MeasureTheory.Measure.map (fun (ω : Ω) => X ω i) ↑μ = MeasureTheory.volume) : Copula d

Construct a copula from a random vector with uniform coordinate laws.

Equations

• ProbabilityTheory.Copula.ofMap μ X hX hmarg = { measure := μ.map X, marginal_eq := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_ofMap {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (X : Ω → Fin d → ↑unitInterval) (hX : Measurable X) (hmarg : ∀ (i : Fin d), MeasureTheory.Measure.map (fun (ω : Ω) => X ω i) ↑μ = MeasureTheory.volume) : (ofMap μ X hX hmarg).toMeasure = MeasureTheory.Measure.map X ↑μ