← Copula mathematical handbook

Measurable families of copulas

These kernels allow a conditional pair copula to depend on the actual values of the conditioning variables. Constant families recover the simplifying assumption.

structure ProbabilityTheory.Copula.Family (Ω : Type u_1) [MeasurableSpace Ω] (d : ℕ) : Type u_1

A measurable family of copulas, parametrized by a measurable space.

• kernel : Kernel Ω (Fin d → ↑unitInterval)

  The family of probability laws.

• markov : IsMarkovKernel self.kernel

  Each law is a probability measure.

• marginal (ω : Ω) (i : Fin d) : MeasureTheory.Measure.map (fun (x : Fin d → ↑unitInterval) => x i) (self.kernel ω) = MeasureTheory.volume

  Each coordinate is uniform at every parameter value.

def ProbabilityTheory.Copula.Family.copula {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (F : Family Ω d) (ω : Ω) : Copula d

The copula at a given parameter value.

Equations

• F.copula ω = { measure := ⟨F.kernel ω, ⋯⟩, marginal_eq := ⋯ }

noncomputable def ProbabilityTheory.Copula.Family.const {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (C : Copula d) : Family Ω d

A simplified (constant) conditional copula.

Equations

• ProbabilityTheory.Copula.Family.const C = { kernel := ProbabilityTheory.Kernel.const Ω C.toMeasure, markov := ⋯, marginal := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.Family.copula_const {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (C : Copula d) (ω : Ω) : (const C).copula ω = C

def ProbabilityTheory.Copula.Family.comap {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {d : ℕ} (F : Family Ω d) (f : Ω' → Ω) (hf : Measurable f) : Family Ω' d

Pull back a family along a measurable conditioning map.

Equations

• F.comap f hf = { kernel := F.kernel.comap f hf, markov := ⋯, marginal := ⋯ }

def ProbabilityTheory.Copula.Family.ofCopulas {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (C : Ω → Copula d) (hC : Measurable fun (ω : Ω) => (C ω).toMeasure) : Family Ω d

Assemble a family from copulas whose probability laws depend measurably on the parameter.

Equations

• ProbabilityTheory.Copula.Family.ofCopulas C hC = { kernel := { toFun := fun (ω : Ω) => (C ω).toMeasure, measurable' := hC }, markov := ⋯, marginal := ⋯ }

noncomputable def ProbabilityTheory.Copula.Family.piecewise {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (s : Set Ω) (hs : MeasurableSet s) (F G : Family Ω d) : Family Ω d

Choose between two families on a measurable set of conditioning values.

Equations

• ProbabilityTheory.Copula.Family.piecewise s hs F G = ProbabilityTheory.Copula.Family.ofCopulas (s.piecewise F.copula G.copula) ⋯

@[simp]

theorem ProbabilityTheory.Copula.Family.copula_piecewise_of_mem {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (s : Set Ω) (hs : MeasurableSet s) (F G : Family Ω d) (ω : Ω) (hω : ω ∈ s) : (piecewise s hs F G).copula ω = F.copula ω

@[simp]

theorem ProbabilityTheory.Copula.Family.copula_piecewise_of_notMem {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (s : Set Ω) (hs : MeasurableSet s) (F G : Family Ω d) (ω : Ω) (hω : ω ∉ s) : (piecewise s hs F G).copula ω = G.copula ω

theorem ProbabilityTheory.Copula.Family.map_fst_eval_compProd {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (F : Family Ω d) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (i : Fin d) : MeasureTheory.Measure.map (fun (p : Ω × (Fin d → ↑unitInterval)) => (p.1, p.2 i)) (μ.compProd F.kernel) = μ.prod MeasureTheory.volume

A pair coordinate remains independent of the conditioning parameter before the conditional quantile transform, even for a nonconstant family.

theorem ProbabilityTheory.Copula.Vine.measurable_kernelQuantile {Ω : Type u_1} [MeasurableSpace Ω] (κ : Kernel Ω ↑unitInterval) [IsMarkovKernel κ] : Measurable fun (p : Ω × ↑unitInterval) => unitQuantile (κ p.1) p.2

Joint measurability of generalized quantiles of a Markov kernel.

theorem ProbabilityTheory.Copula.Vine.map_kernelQuantile {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (κ : Kernel Ω ↑unitInterval) [IsMarkovKernel κ] : MeasureTheory.Measure.map (fun (p : Ω × ↑unitInterval) => (p.1, unitQuantile (κ p.1) p.2)) (μ.prod MeasureTheory.volume) = μ.compProd κ

A uniform quantile coordinate reconstructs a kernel jointly with its parameter.

theorem ProbabilityTheory.Copula.Vine.map_family_quantile {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (F : Family Ω 2) (κ : Kernel Ω ↑unitInterval) [IsMarkovKernel κ] (i : Fin 2) : MeasureTheory.Measure.map (fun (p : Ω × (Fin 2 → ↑unitInterval)) => (p.1, unitQuantile (κ p.1) (p.2 i))) (μ.compProd F.kernel) = μ.compProd κ

Conditional copula coupling has exactly the requested one-dimensional kernels.